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

Axiom ax-hvcom 27746
Description: Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvcom ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Detailed syntax breakdown of Axiom ax-hvcom
StepHypRef Expression
1 cA . . . 4 class 𝐴
2 chil 27664 . . . 4 class
31, 2wcel 1987 . . 3 wff 𝐴 ∈ ℋ
4 cB . . . 4 class 𝐵
54, 2wcel 1987 . . 3 wff 𝐵 ∈ ℋ
63, 5wa 384 . 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7 cva 27665 . . . 4 class +
81, 4, 7co 6615 . . 3 class (𝐴 + 𝐵)
94, 1, 7co 6615 . . 3 class (𝐵 + 𝐴)
108, 9wceq 1480 . 2 wff (𝐴 + 𝐵) = (𝐵 + 𝐴)
116, 10wi 4 1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
This axiom is referenced by:  hvcomi  27764  hvaddid2  27768  hvadd32  27779  hvadd12  27780  hvpncan2  27785  hvsub32  27790  hvaddcan2  27816  hilablo  27905  hhssabloi  28007  shscom  28066  pjhtheu2  28163  pjpjpre  28166  pjpo  28175  spanunsni  28326  chscllem4  28387  hoaddcomi  28519  pjimai  28923  superpos  29101  sumdmdii  29162  cdj3lem3  29185  cdj3lem3b  29187
  Copyright terms: Public domain W3C validator