HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hvcom Unicode version

Axiom ax-hvcom 21411
Description: Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvcom  |-  ( ( A  e.  ~H  /\  B  e.  ~H )  ->  ( A  +h  B
)  =  ( B  +h  A ) )

Detailed syntax breakdown of Axiom ax-hvcom
StepHypRef Expression
1 cA . . . 4  class  A
2 chil 21329 . . . 4  class  ~H
31, 2wcel 1621 . . 3  wff  A  e. 
~H
4 cB . . . 4  class  B
54, 2wcel 1621 . . 3  wff  B  e. 
~H
63, 5wa 360 . 2  wff  ( A  e.  ~H  /\  B  e.  ~H )
7 cva 21330 . . . 4  class  +h
81, 4, 7co 5710 . . 3  class  ( A  +h  B )
94, 1, 7co 5710 . . 3  class  ( B  +h  A )
108, 9wceq 1619 . 2  wff  ( A  +h  B )  =  ( B  +h  A
)
116, 10wi 6 1  wff  ( ( A  e.  ~H  /\  B  e.  ~H )  ->  ( A  +h  B
)  =  ( B  +h  A ) )
Colors of variables: wff set class
This axiom is referenced by:  hvcomi  21429  hvaddid2  21432  hvadd32  21443  hvadd12  21444  hvpncan2  21449  hvsub32  21454  hvaddcan2  21480  hilablo  21569  hhssabloi  21669  shscom  21728  pjhtheu2  21825  pjpjpre  21828  pjpo  21837  spanunsni  21988  chscllem4  22067  hoaddcomi  22182  pjimai  22586  superpos  22764  sumdmdii  22825  cdj3lem3  22848  cdj3lem3b  22850
  Copyright terms: Public domain W3C validator