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

Axiom ax-hvcom 21894
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 21812 . . . 4  class  ~H
31, 2wcel 1715 . . 3  wff  A  e. 
~H
4 cB . . . 4  class  B
54, 2wcel 1715 . . 3  wff  B  e. 
~H
63, 5wa 358 . 2  wff  ( A  e.  ~H  /\  B  e.  ~H )
7 cva 21813 . . . 4  class  +h
81, 4, 7co 5981 . . 3  class  ( A  +h  B )
94, 1, 7co 5981 . . 3  class  ( B  +h  A )
108, 9wceq 1647 . 2  wff  ( A  +h  B )  =  ( B  +h  A
)
116, 10wi 4 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  21912  hvaddid2  21915  hvadd32  21926  hvadd12  21927  hvpncan2  21932  hvsub32  21937  hvaddcan2  21963  hilablo  22052  hhssabloi  22152  shscom  22211  pjhtheu2  22308  pjpjpre  22311  pjpo  22320  spanunsni  22471  chscllem4  22532  hoaddcomi  22665  pjimai  23069  superpos  23247  sumdmdii  23308  cdj3lem3  23331  cdj3lem3b  23333
  Copyright terms: Public domain W3C validator