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

Axiom ax-hvcom 21597
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 21515 . . . 4  class  ~H
31, 2wcel 1696 . . 3  wff  A  e. 
~H
4 cB . . . 4  class  B
54, 2wcel 1696 . . 3  wff  B  e. 
~H
63, 5wa 358 . 2  wff  ( A  e.  ~H  /\  B  e.  ~H )
7 cva 21516 . . . 4  class  +h
81, 4, 7co 5874 . . 3  class  ( A  +h  B )
94, 1, 7co 5874 . . 3  class  ( B  +h  A )
108, 9wceq 1632 . 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  21615  hvaddid2  21618  hvadd32  21629  hvadd12  21630  hvpncan2  21635  hvsub32  21640  hvaddcan2  21666  hilablo  21755  hhssabloi  21855  shscom  21914  pjhtheu2  22011  pjpjpre  22014  pjpo  22023  spanunsni  22174  chscllem4  22235  hoaddcomi  22368  pjimai  22772  superpos  22950  sumdmdii  23011  cdj3lem3  23034  cdj3lem3b  23036
  Copyright terms: Public domain W3C validator