Metamath Proof Explorer

Axiom ax-hvcom

Description: Vector addition is commutative. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-hvcom 
|- ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) = ( B +h A ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 chba 
 |-  ~H
2 0 1 wcel 
 |-  A e. ~H
3 cB 
 |-  B
4 3 1 wcel 
 |-  B e. ~H
5 2 4 wa 
 |-  ( A e. ~H /\ B e. ~H )
6 cva 
 |-  +h
7 0 3 6 co 
 |-  ( A +h B )
8 3 0 6 co 
 |-  ( B +h A )
9 7 8 wceq 
 |-  ( A +h B ) = ( B +h A )
10 5 9 wi 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) = ( B +h A ) )