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

Axiom ax-hvcom 21581
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 21499 . . . 4  class  ~H
31, 2wcel 1684 . . 3  wff  A  e. 
~H
4 cB . . . 4  class  B
54, 2wcel 1684 . . 3  wff  B  e. 
~H
63, 5wa 358 . 2  wff  ( A  e.  ~H  /\  B  e.  ~H )
7 cva 21500 . . . 4  class  +h
81, 4, 7co 5858 . . 3  class  ( A  +h  B )
94, 1, 7co 5858 . . 3  class  ( B  +h  A )
108, 9wceq 1623 . 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  21599  hvaddid2  21602  hvadd32  21613  hvadd12  21614  hvpncan2  21619  hvsub32  21624  hvaddcan2  21650  hilablo  21739  hhssabloi  21839  shscom  21898  pjhtheu2  21995  pjpjpre  21998  pjpo  22007  spanunsni  22158  chscllem4  22219  hoaddcomi  22352  pjimai  22756  superpos  22934  sumdmdii  22995  cdj3lem3  23018  cdj3lem3b  23020
  Copyright terms: Public domain W3C validator