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

Axiom ax-hvcom 21506
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 21424 . . . 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 21425 . . . 4  class  +h
81, 4, 7co 5757 . . 3  class  ( A  +h  B )
94, 1, 7co 5757 . . 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  21524  hvaddid2  21527  hvadd32  21538  hvadd12  21539  hvpncan2  21544  hvsub32  21549  hvaddcan2  21575  hilablo  21664  hhssabloi  21764  shscom  21823  pjhtheu2  21920  pjpjpre  21923  pjpo  21932  spanunsni  22083  chscllem4  22162  hoaddcomi  22277  pjimai  22681  superpos  22859  sumdmdii  22920  cdj3lem3  22943  cdj3lem3b  22945
  Copyright terms: Public domain W3C validator