![]() |
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 10270 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 2107 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | 4, 2 | wcel 2107 | . . 3 wff 𝐵 ∈ ℂ |
6 | cC | . . . 4 class 𝐶 | |
7 | chba 28348 | . . . 4 class ℋ | |
8 | 6, 7 | wcel 2107 | . . 3 wff 𝐶 ∈ ℋ |
9 | 3, 5, 8 | w3a 1071 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) |
10 | cmul 10277 | . . . . 5 class · | |
11 | 1, 4, 10 | co 6922 | . . . 4 class (𝐴 · 𝐵) |
12 | csm 28350 | . . . 4 class ·ℎ | |
13 | 11, 6, 12 | co 6922 | . . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶) |
14 | 4, 6, 12 | co 6922 | . . . 4 class (𝐵 ·ℎ 𝐶) |
15 | 1, 14, 12 | co 6922 | . . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) |
16 | 13, 15 | wceq 1601 | . 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) |
17 | 9, 16 | wi 4 | 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmul0 28453 hvmul0or 28454 hvm1neg 28461 hvmulcom 28472 hvmulassi 28475 hvsubdistr2 28479 hilvc 28591 hhssnv 28693 h1de2bi 28985 spansncol 28999 h1datomi 29012 mayete3i 29159 homulass 29233 kbmul 29386 kbass5 29551 strlem1 29681 |
Copyright terms: Public domain | W3C validator |