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

Axiom ax-hvcom 21542
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 21460 . . . 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 21461 . . . 4  class  +h
81, 4, 7co 5792 . . 3  class  ( A  +h  B )
94, 1, 7co 5792 . . 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  21560  hvaddid2  21563  hvadd32  21574  hvadd12  21575  hvpncan2  21580  hvsub32  21585  hvaddcan2  21611  hilablo  21700  hhssabloi  21800  shscom  21859  pjhtheu2  21956  pjpjpre  21959  pjpo  21968  spanunsni  22119  chscllem4  22180  hoaddcomi  22313  pjimai  22717  superpos  22895  sumdmdii  22956  cdj3lem3  22979  cdj3lem3b  22981
  Copyright terms: Public domain W3C validator