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 31029
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 30947 . . . 4 class
31, 2wcel 2105 . . 3 wff 𝐴 ∈ ℋ
4 cB . . . 4 class 𝐵
54, 2wcel 2105 . . 3 wff 𝐵 ∈ ℋ
63, 5wa 395 . 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7 cva 30948 . . . 4 class +
81, 4, 7co 7430 . . 3 class (𝐴 + 𝐵)
94, 1, 7co 7430 . . 3 class (𝐵 + 𝐴)
108, 9wceq 1536 . 2 wff (𝐴 + 𝐵) = (𝐵 + 𝐴)
116, 10wi 4 1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
This axiom is referenced by:  hvcomi  31047  hvaddlid  31051  hvadd32  31062  hvadd12  31063  hvpncan2  31068  hvsub32  31073  hvaddcan2  31099  hilablo  31188  hhssabloi  31290  shscom  31347  pjhtheu2  31444  pjpjpre  31447  pjpo  31456  spanunsni  31607  chscllem4  31668  hoaddcomi  31800  pjimai  32204  superpos  32382  sumdmdii  32443  cdj3lem3  32466  cdj3lem3b  32468
  Copyright terms: Public domain W3C validator