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 27986
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 27904 . . . 4 class
31, 2wcel 2030 . . 3 wff 𝐴 ∈ ℋ
4 cB . . . 4 class 𝐵
54, 2wcel 2030 . . 3 wff 𝐵 ∈ ℋ
63, 5wa 383 . 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7 cva 27905 . . . 4 class +
81, 4, 7co 6690 . . 3 class (𝐴 + 𝐵)
94, 1, 7co 6690 . . 3 class (𝐵 + 𝐴)
108, 9wceq 1523 . 2 wff (𝐴 + 𝐵) = (𝐵 + 𝐴)
116, 10wi 4 1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
This axiom is referenced by:  hvcomi  28004  hvaddid2  28008  hvadd32  28019  hvadd12  28020  hvpncan2  28025  hvsub32  28030  hvaddcan2  28056  hilablo  28145  hhssabloi  28247  shscom  28306  pjhtheu2  28403  pjpjpre  28406  pjpo  28415  spanunsni  28566  chscllem4  28627  hoaddcomi  28759  pjimai  29163  superpos  29341  sumdmdii  29402  cdj3lem3  29425  cdj3lem3b  29427
  Copyright terms: Public domain W3C validator