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 28782
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 chba 28700 . . . 4 class
31, 2wcel 2114 . . 3 wff 𝐴 ∈ ℋ
4 cB . . . 4 class 𝐵
54, 2wcel 2114 . . 3 wff 𝐵 ∈ ℋ
63, 5wa 399 . 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7 cva 28701 . . . 4 class +
81, 4, 7co 7140 . . 3 class (𝐴 + 𝐵)
94, 1, 7co 7140 . . 3 class (𝐵 + 𝐴)
108, 9wceq 1538 . 2 wff (𝐴 + 𝐵) = (𝐵 + 𝐴)
116, 10wi 4 1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
This axiom is referenced by:  hvcomi  28800  hvaddid2  28804  hvadd32  28815  hvadd12  28816  hvpncan2  28821  hvsub32  28826  hvaddcan2  28852  hilablo  28941  hhssabloi  29043  shscom  29100  pjhtheu2  29197  pjpjpre  29200  pjpo  29209  spanunsni  29360  chscllem4  29421  hoaddcomi  29553  pjimai  29957  superpos  30135  sumdmdii  30196  cdj3lem3  30219  cdj3lem3b  30221
  Copyright terms: Public domain W3C validator