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

Axiom ax-hvcom 21583
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 21501 . . . 4  class  ~H
31, 2wcel 1686 . . 3  wff  A  e. 
~H
4 cB . . . 4  class  B
54, 2wcel 1686 . . 3  wff  B  e. 
~H
63, 5wa 358 . 2  wff  ( A  e.  ~H  /\  B  e.  ~H )
7 cva 21502 . . . 4  class  +h
81, 4, 7co 5860 . . 3  class  ( A  +h  B )
94, 1, 7co 5860 . . 3  class  ( B  +h  A )
108, 9wceq 1625 . 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  21601  hvaddid2  21604  hvadd32  21615  hvadd12  21616  hvpncan2  21621  hvsub32  21626  hvaddcan2  21652  hilablo  21741  hhssabloi  21841  shscom  21900  pjhtheu2  21997  pjpjpre  22000  pjpo  22009  spanunsni  22160  chscllem4  22221  hoaddcomi  22354  pjimai  22758  superpos  22936  sumdmdii  22997  cdj3lem3  23020  cdj3lem3b  23022
  Copyright terms: Public domain W3C validator