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 27031
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 26949 . . . 4 class
31, 2wcel 1938 . . 3 wff 𝐴 ∈ ℋ
4 cB . . . 4 class 𝐵
54, 2wcel 1938 . . 3 wff 𝐵 ∈ ℋ
63, 5wa 382 . 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7 cva 26950 . . . 4 class +
81, 4, 7co 6425 . . 3 class (𝐴 + 𝐵)
94, 1, 7co 6425 . . 3 class (𝐵 + 𝐴)
108, 9wceq 1474 . 2 wff (𝐴 + 𝐵) = (𝐵 + 𝐴)
116, 10wi 4 1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
This axiom is referenced by:  hvcomi  27049  hvaddid2  27053  hvadd32  27064  hvadd12  27065  hvpncan2  27070  hvsub32  27075  hvaddcan2  27101  hilablo  27190  hhssabloi  27292  shscom  27351  pjhtheu2  27448  pjpjpre  27451  pjpo  27460  spanunsni  27611  chscllem4  27672  hoaddcomi  27804  pjimai  28208  superpos  28386  sumdmdii  28447  cdj3lem3  28470  cdj3lem3b  28472
  Copyright terms: Public domain W3C validator