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

Axiom ax-hvcom 22457
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 22375 . . . 4  class  ~H
31, 2wcel 1721 . . 3  wff  A  e. 
~H
4 cB . . . 4  class  B
54, 2wcel 1721 . . 3  wff  B  e. 
~H
63, 5wa 359 . 2  wff  ( A  e.  ~H  /\  B  e.  ~H )
7 cva 22376 . . . 4  class  +h
81, 4, 7co 6040 . . 3  class  ( A  +h  B )
94, 1, 7co 6040 . . 3  class  ( B  +h  A )
108, 9wceq 1649 . 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  22475  hvaddid2  22478  hvadd32  22489  hvadd12  22490  hvpncan2  22495  hvsub32  22500  hvaddcan2  22526  hilablo  22615  hhssabloi  22715  shscom  22774  pjhtheu2  22871  pjpjpre  22874  pjpo  22883  spanunsni  23034  chscllem4  23095  hoaddcomi  23228  pjimai  23632  superpos  23810  sumdmdii  23871  cdj3lem3  23894  cdj3lem3b  23896
  Copyright terms: Public domain W3C validator