![]() |
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 11090 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 2106 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | 4, 2 | wcel 2106 | . . 3 wff 𝐵 ∈ ℂ |
6 | cC | . . . 4 class 𝐶 | |
7 | chba 30035 | . . . 4 class ℋ | |
8 | 6, 7 | wcel 2106 | . . 3 wff 𝐶 ∈ ℋ |
9 | 3, 5, 8 | w3a 1087 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) |
10 | cmul 11097 | . . . . 5 class · | |
11 | 1, 4, 10 | co 7393 | . . . 4 class (𝐴 · 𝐵) |
12 | csm 30037 | . . . 4 class ·ℎ | |
13 | 11, 6, 12 | co 7393 | . . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶) |
14 | 4, 6, 12 | co 7393 | . . . 4 class (𝐵 ·ℎ 𝐶) |
15 | 1, 14, 12 | co 7393 | . . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) |
16 | 13, 15 | wceq 1541 | . 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) |
17 | 9, 16 | wi 4 | 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmul0 30140 hvmul0or 30141 hvm1neg 30148 hvmulcom 30159 hvmulassi 30162 hvsubdistr2 30166 hilvc 30278 hhssnv 30380 h1de2bi 30670 spansncol 30684 h1datomi 30697 mayete3i 30844 homulass 30918 kbmul 31071 kbass5 31236 strlem1 31366 |
Copyright terms: Public domain | W3C validator |