HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Axiom ax-hvcom 9019
Description: Vector addition is commutative.
Assertion
Ref Expression
ax-hvcom |- ((A e. H~ /\ B e. H~) -> (A +h B) = (B +h A))
Detailed syntax breakdown of Axiom ax-hvcom
StepHypRef Expression
1 cA . . . 4 class A
2 chil 8968 . . . 4 class H~
31, 2wcel 1105 . . 3 wff A e. H~
4 cB . . . 4 class B
54, 2wcel 1105 . . 3 wff B e. H~
63, 5wa 223 . 2 wff (A e. H~ /\ B e. H~)
7 cva 8969 . . . 4 class +h
81, 4, 7co 3902 . . 3 class (A +h B)
94, 1, 7co 3902 . . 3 class (B +h A)
108, 9wceq 1099 . 2 wff (A +h B) = (B +h A)
116, 10wi 3 1 wff ((A e. H~ /\ B e. H~) -> (A +h B) = (B +h A))
Colors of variables: wff set class
This axiom is referenced by:  hvcom 9038  hvaddid2t 9041  hvadd23t 9052  hvadd12t 9053  hvpncan2t 9058  hvaddcan2t 9087  hilabl 9176  pjtheu2 9379  pjpj0 9384  pjpot 9390  shscomt 9412  spanunsn 9633  hoaddcom 9829  hhlno 9957  pjima 10229  superpos 10403  sumdmdi 10463  cdj3lem3 10484  cdj3lem3b 10486
Copyright terms: Public domain