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

Axiom ax-hvcom 22506
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 22424 . . . 4  class  ~H
31, 2wcel 1726 . . 3  wff  A  e. 
~H
4 cB . . . 4  class  B
54, 2wcel 1726 . . 3  wff  B  e. 
~H
63, 5wa 360 . 2  wff  ( A  e.  ~H  /\  B  e.  ~H )
7 cva 22425 . . . 4  class  +h
81, 4, 7co 6083 . . 3  class  ( A  +h  B )
94, 1, 7co 6083 . . 3  class  ( B  +h  A )
108, 9wceq 1653 . 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  22524  hvaddid2  22527  hvadd32  22538  hvadd12  22539  hvpncan2  22544  hvsub32  22549  hvaddcan2  22575  hilablo  22664  hhssabloi  22764  shscom  22823  pjhtheu2  22920  pjpjpre  22923  pjpo  22932  spanunsni  23083  chscllem4  23144  hoaddcomi  23277  pjimai  23681  superpos  23859  sumdmdii  23920  cdj3lem3  23943  cdj3lem3b  23945
  Copyright terms: Public domain W3C validator