![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > ax-hvcom | Structured version Visualization version GIF version |
Description: Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-hvcom | ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . . 4 class 𝐴 | |
2 | chba 30947 | . . . 4 class ℋ | |
3 | 1, 2 | wcel 2105 | . . 3 wff 𝐴 ∈ ℋ |
4 | cB | . . . 4 class 𝐵 | |
5 | 4, 2 | wcel 2105 | . . 3 wff 𝐵 ∈ ℋ |
6 | 3, 5 | wa 395 | . 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) |
7 | cva 30948 | . . . 4 class +ℎ | |
8 | 1, 4, 7 | co 7430 | . . 3 class (𝐴 +ℎ 𝐵) |
9 | 4, 1, 7 | co 7430 | . . 3 class (𝐵 +ℎ 𝐴) |
10 | 8, 9 | wceq 1536 | . 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴) |
11 | 6, 10 | wi 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 |