Throughout, (a), (b), (c), (d) refer to the conditions of Real Inner Product Space §inner-product, and ∣x∣ is the unique real number r with 0≤r and r2=⟨x,x⟩ provided by Existence and Uniqueness of the Nonnegative Square Root as in Real Inner Product Space §norm. We use freely the field axioms of R and the vector space axioms of Vector Space over a Field.
Claim 1. By (a), (b) and (a) again, ⟨x,y+z⟩=⟨y+z,x⟩=⟨y,x⟩+⟨z,x⟩=⟨x,y⟩+⟨x,z⟩; by (a), (c) and (a), ⟨x,λy⟩=⟨λy,x⟩=λ⟨y,x⟩=λ⟨x,y⟩. By claim 5 of Elementary Identities in a Vector Space, −x=(−1)x, so by (c), ⟨−x,y⟩=(−1)⟨x,y⟩=−⟨x,y⟩, and by symmetry (a) also ⟨x,−y⟩=−⟨x,y⟩. Finally ⟨x−y,z⟩=⟨x+(−y),z⟩=⟨x,z⟩+⟨−y,z⟩=⟨x,z⟩−⟨y,z⟩ by (b) and what was just shown, and likewise ⟨x,y−z⟩=⟨x,y⟩−⟨x,z⟩ by the additivity in the second argument just proved.
Claim 2. By claim 3 of Elementary Identities in a Vector Space, 0E=0x, so by (c), ⟨0E,x⟩=⟨0x,x⟩=0⟨x,x⟩=0, and ⟨x,0E⟩=0 by (a). In particular ⟨0E,0E⟩=0=02 with 0≤0, so ∣0E∣=0 by the uniqueness in Existence and Uniqueness of the Nonnegative Square Root.
Claim 3. If ∣x∣=0 then ⟨x,x⟩=∣x∣2=0, so x=0E by (d). Conversely ∣0E∣=0 by claim 2. If x=0E, then ∣x∣=0 by what was just shown, while 0≤∣x∣; hence 0<∣x∣ by the definition of the strict order.
Claim 4. By (c) and claim 1, ⟨λx,λx⟩=λ⟨x,λx⟩=λ2⟨x,x⟩. By claim 1 of Properties of the Absolute Value in an Ordered Field, ∣λ∣ equals λ or −λ, and (−λ)2=λ2 in the field R, so ∣λ∣2=λ2. Hence (∣λ∣∣x∣)2=∣λ∣2∣x∣2=λ2⟨x,x⟩=⟨λx,λx⟩=∣λx∣2. Both ∣λx∣ and ∣λ∣∣x∣ are nonnegative: the first by Real Inner Product Space §norm, the second because 0≤∣λ∣ (claim 1 of Properties of the Absolute Value in an Ordered Field) and 0≤∣x∣, so that 0=∣λ∣⋅0≤∣λ∣∣x∣ by claim 5 of Elementary Arithmetic in an Ordered Field. Hence they are equal by claim 3 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field. For the last assertion, −x=(−1)x, and ∣−1∣=∣1∣ by claim 2 of Properties of the Absolute Value in an Ordered Field while ∣1∣=1 by Absolute Value in an Ordered Field since 0≤1 (claim 1 of Elementary Arithmetic in an Ordered Field); so ∣−x∣=∣−1∣∣x∣=∣x∣.
Claim 5. By (b) and claim 1,
∣x+y∣2=⟨x+y,x+y⟩=⟨x,x+y⟩+⟨y,x+y⟩=⟨x,x⟩+⟨x,y⟩+⟨y,x⟩+⟨y,y⟩=∣x∣2+2⟨x,y⟩+∣y∣2,
using (a) for ⟨y,x⟩=⟨x,y⟩. Applying this with −y in place of y, and using ⟨x,−y⟩=−⟨x,y⟩ (claim 1) and ∣−y∣=∣y∣ (claim 4), gives ∣x−y∣2=∣x∣2−2⟨x,y⟩+∣y∣2.
Claim 6. Add the two identities of claim 5.
Claim 7. Subtract the second identity of claim 5 from the first: ∣x+y∣2−∣x−y∣2=4⟨x,y⟩.