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

Axiom ax-hvcom 22492
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 22410 . . . 4  class  ~H
31, 2wcel 1725 . . 3  wff  A  e. 
~H
4 cB . . . 4  class  B
54, 2wcel 1725 . . 3  wff  B  e. 
~H
63, 5wa 359 . 2  wff  ( A  e.  ~H  /\  B  e.  ~H )
7 cva 22411 . . . 4  class  +h
81, 4, 7co 6072 . . 3  class  ( A  +h  B )
94, 1, 7co 6072 . . 3  class  ( B  +h  A )
108, 9wceq 1652 . 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  22510  hvaddid2  22513  hvadd32  22524  hvadd12  22525  hvpncan2  22530  hvsub32  22535  hvaddcan2  22561  hilablo  22650  hhssabloi  22750  shscom  22809  pjhtheu2  22906  pjpjpre  22909  pjpo  22918  spanunsni  23069  chscllem4  23130  hoaddcomi  23263  pjimai  23667  superpos  23845  sumdmdii  23906  cdj3lem3  23929  cdj3lem3b  23931
  Copyright terms: Public domain W3C validator