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 31020
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 30938 . . . 4 class
31, 2wcel 2108 . . 3 wff 𝐴 ∈ ℋ
4 cB . . . 4 class 𝐵
54, 2wcel 2108 . . 3 wff 𝐵 ∈ ℋ
63, 5wa 395 . 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7 cva 30939 . . . 4 class +
81, 4, 7co 7431 . . 3 class (𝐴 + 𝐵)
94, 1, 7co 7431 . . 3 class (𝐵 + 𝐴)
108, 9wceq 1540 . 2 wff (𝐴 + 𝐵) = (𝐵 + 𝐴)
116, 10wi 4 1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
This axiom is referenced by:  hvcomi  31038  hvaddlid  31042  hvadd32  31053  hvadd12  31054  hvpncan2  31059  hvsub32  31064  hvaddcan2  31090  hilablo  31179  hhssabloi  31281  shscom  31338  pjhtheu2  31435  pjpjpre  31438  pjpo  31447  spanunsni  31598  chscllem4  31659  hoaddcomi  31791  pjimai  32195  superpos  32373  sumdmdii  32434  cdj3lem3  32457  cdj3lem3b  32459
  Copyright terms: Public domain W3C validator