In the coordinate-free approach to differential geometry, this statement has a rather different ontological status than that which it has in the coordinate approach. While, in the latter, it is a theorem, pure and simple, in the former, it is a combination of definition and theorem. That is to say, one uses the equation to define the exterior derivative of a one-form but, in order for this definition to be valid, one must first show that a. the right-hand side of this identity satisfies the requisite properties of antisymmetry and bilinearity and b. the operator implicitly defined is linear.

Proof of a.

For simplicity, we will break down this demontration into three parts.

Antisymmetry

It is easy enough to see that both sides of the equation change by a sign upon interchanging with as a consequence of antisymmetry of two-forms and of the Lie bracket:

Distributivity over addition

Scaling

Finally, we verify that our expression transforms properly under rescaling. Again, by antisymmetry, it suffices to look at only one argument.

Hence this expression behaves like a two-form should. By the principle "If it looks like a duck and quacks like a duck, it must be a duck", we conclude that the expression indeed specifies a two-form.

Proof of b.

As before, we will break the proof of linearity into two steps. Note that here the term "scalar" simply means a real number, not a function on the manifold.

Distributivity over addition

Scaling