![]() |
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 10136 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 2145 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | 4, 2 | wcel 2145 | . . 3 wff 𝐵 ∈ ℂ |
6 | cC | . . . 4 class 𝐶 | |
7 | chil 28116 | . . . 4 class ℋ | |
8 | 6, 7 | wcel 2145 | . . 3 wff 𝐶 ∈ ℋ |
9 | 3, 5, 8 | w3a 1071 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) |
10 | cmul 10143 | . . . . 5 class · | |
11 | 1, 4, 10 | co 6793 | . . . 4 class (𝐴 · 𝐵) |
12 | csm 28118 | . . . 4 class ·ℎ | |
13 | 11, 6, 12 | co 6793 | . . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶) |
14 | 4, 6, 12 | co 6793 | . . . 4 class (𝐵 ·ℎ 𝐶) |
15 | 1, 14, 12 | co 6793 | . . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) |
16 | 13, 15 | wceq 1631 | . 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) |
17 | 9, 16 | wi 4 | 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmul0 28221 hvmul0or 28222 hvm1neg 28229 hvmulcom 28240 hvmulassi 28243 hvsubdistr2 28247 hilvc 28359 hhssnv 28461 h1de2bi 28753 spansncol 28767 h1datomi 28780 mayete3i 28927 homulass 29001 kbmul 29154 kbass5 29319 strlem1 29449 |
Copyright terms: Public domain | W3C validator |