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 28197
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 28115 . . . 4 class
31, 2wcel 2145 . . 3 wff 𝐴 ∈ ℋ
4 cB . . . 4 class 𝐵
54, 2wcel 2145 . . 3 wff 𝐵 ∈ ℋ
63, 5wa 382 . 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7 cva 28116 . . . 4 class +
81, 4, 7co 6795 . . 3 class (𝐴 + 𝐵)
94, 1, 7co 6795 . . 3 class (𝐵 + 𝐴)
108, 9wceq 1631 . 2 wff (𝐴 + 𝐵) = (𝐵 + 𝐴)
116, 10wi 4 1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
This axiom is referenced by:  hvcomi  28215  hvaddid2  28219  hvadd32  28230  hvadd12  28231  hvpncan2  28236  hvsub32  28241  hvaddcan2  28267  hilablo  28356  hhssabloi  28458  shscom  28517  pjhtheu2  28614  pjpjpre  28617  pjpo  28626  spanunsni  28777  chscllem4  28838  hoaddcomi  28970  pjimai  29374  superpos  29552  sumdmdii  29613  cdj3lem3  29636  cdj3lem3b  29638
  Copyright terms: Public domain W3C validator