| 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 30938 | . . . 4 class ℋ | |
| 3 | 1, 2 | wcel 2108 | . . 3 wff 𝐴 ∈ ℋ |
| 4 | cB | . . . 4 class 𝐵 | |
| 5 | 4, 2 | wcel 2108 | . . 3 wff 𝐵 ∈ ℋ |
| 6 | 3, 5 | wa 395 | . 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) |
| 7 | cva 30939 | . . . 4 class +ℎ | |
| 8 | 1, 4, 7 | co 7431 | . . 3 class (𝐴 +ℎ 𝐵) |
| 9 | 4, 1, 7 | co 7431 | . . 3 class (𝐵 +ℎ 𝐴) |
| 10 | 8, 9 | wceq 1540 | . 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴) |
| 11 | 6, 10 | wi 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 |