| Hilbert Space Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Scalar multiplication associative law |
| Ref | Expression |
|---|---|
| ax-hvmulass |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . . 4
| |
| 2 | cc 5204 |
. . . 4
| |
| 3 | 1, 2 | wcel 955 |
. . 3
|
| 4 | cB |
. . . 4
| |
| 5 | 4, 2 | wcel 955 |
. . 3
|
| 6 | cC |
. . . 4
| |
| 7 | chil 8727 |
. . . 4
| |
| 8 | 6, 7 | wcel 955 |
. . 3
|
| 9 | 3, 5, 8 | w3a 773 |
. 2
|
| 10 | cmul 5211 |
. . . . 5
| |
| 11 | 1, 4, 10 | co 3948 |
. . . 4
|
| 12 | csm 8729 |
. . . 4
| |
| 13 | 11, 6, 12 | co 3948 |
. . 3
|
| 14 | 4, 6, 12 | co 3948 |
. . . 4
|
| 15 | 1, 14, 12 | co 3948 |
. . 3
|
| 16 | 13, 15 | wceq 953 |
. 2
|
| 17 | 9, 16 | wi 3 |
1
|
| Colors of variables: wff set class |
| This axiom is referenced by: hvmul0t 8814 hvmul0ort 8815 hvm1negt 8822 hvmulcomt 8833 hvmulass 8834 hvsubdistr2t 8838 hilvc 8950 hhssnv 9054 h1de2b 9392 h1de2bOLD 9393 spansncol 9407 h1datom 9421 mayete3 9590 homulasst 9645 kbmult 9795 kbass5t 9965 strlem1 10087 |