| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > ax-hvmulass | Structured version Visualization version GIF version | ||
| Description: Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ax-hvmulass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . . 4 class 𝐴 | |
| 2 | cc 11153 | . . . 4 class ℂ | |
| 3 | 1, 2 | wcel 2108 | . . 3 wff 𝐴 ∈ ℂ |
| 4 | cB | . . . 4 class 𝐵 | |
| 5 | 4, 2 | wcel 2108 | . . 3 wff 𝐵 ∈ ℂ |
| 6 | cC | . . . 4 class 𝐶 | |
| 7 | chba 30938 | . . . 4 class ℋ | |
| 8 | 6, 7 | wcel 2108 | . . 3 wff 𝐶 ∈ ℋ |
| 9 | 3, 5, 8 | w3a 1087 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) |
| 10 | cmul 11160 | . . . . 5 class · | |
| 11 | 1, 4, 10 | co 7431 | . . . 4 class (𝐴 · 𝐵) |
| 12 | csm 30940 | . . . 4 class ·ℎ | |
| 13 | 11, 6, 12 | co 7431 | . . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶) |
| 14 | 4, 6, 12 | co 7431 | . . . 4 class (𝐵 ·ℎ 𝐶) |
| 15 | 1, 14, 12 | co 7431 | . . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) |
| 16 | 13, 15 | wceq 1540 | . 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) |
| 17 | 9, 16 | wi 4 | 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) |
| Colors of variables: wff setvar class |
| This axiom is referenced by: hvmul0 31043 hvmul0or 31044 hvm1neg 31051 hvmulcom 31062 hvmulassi 31065 hvsubdistr2 31069 hilvc 31181 hhssnv 31283 h1de2bi 31573 spansncol 31587 h1datomi 31600 mayete3i 31747 homulass 31821 kbmul 31974 kbass5 32139 strlem1 32269 |
| Copyright terms: Public domain | W3C validator |