Metamath Proof Explorer


Theorem axhvcom-zf

Description: Derive Axiom ax-hvcom from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008) (New usage is discouraged.)

Ref Expression
Hypotheses axhil.1 U=+norm
axhil.2 UCHilOLD
Assertion axhvcom-zf ABA+B=B+A

Proof

Step Hyp Ref Expression
1 axhil.1 U=+norm
2 axhil.2 UCHilOLD
3 df-hba =BaseSet+norm
4 1 fveq2i BaseSetU=BaseSet+norm
5 3 4 eqtr4i =BaseSetU
6 2 hlnvi UNrmCVec
7 1 6 h2hva +=+vU
8 5 7 hlcom UCHilOLDABA+B=B+A
9 2 8 mp3an1 ABA+B=B+A