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

Axiom ax-hvcom 21576
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 21494 . . . 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 21495 . . . 4  class  +h
81, 4, 7co 5819 . . 3  class  ( A  +h  B )
94, 1, 7co 5819 . . 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  21594  hvaddid2  21597  hvadd32  21608  hvadd12  21609  hvpncan2  21614  hvsub32  21619  hvaddcan2  21645  hilablo  21734  hhssabloi  21834  shscom  21893  pjhtheu2  21990  pjpjpre  21993  pjpo  22002  spanunsni  22153  chscllem4  22214  hoaddcomi  22347  pjimai  22751  superpos  22929  sumdmdii  22990  cdj3lem3  23013  cdj3lem3b  23015
  Copyright terms: Public domain W3C validator