| 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 6750 |
. . . 4
| |
| 3 | 1, 2 | wcel 1588 |
. . 3
|
| 4 | cB |
. . . 4
| |
| 5 | 4, 2 | wcel 1588 |
. . 3
|
| 6 | cC |
. . . 4
| |
| 7 | chil 11258 |
. . . 4
| |
| 8 | 6, 7 | wcel 1588 |
. . 3
|
| 9 | 3, 5, 8 | w3a 1102 |
. 2
|
| 10 | cmul 6757 |
. . . . 5
| |
| 11 | 1, 4, 10 | co 4981 |
. . . 4
|
| 12 | csm 11260 |
. . . 4
| |
| 13 | 11, 6, 12 | co 4981 |
. . 3
|
| 14 | 4, 6, 12 | co 4981 |
. . . 4
|
| 15 | 1, 14, 12 | co 4981 |
. . 3
|
| 16 | 13, 15 | wceq 1586 |
. 2
|
| 17 | 9, 16 | wi 3 |
1
|
| Colors of variables: wff set class |
| This axiom is referenced by: hvmul0 11363 hvmul0or 11364 hvm1neg 11371 hvmulcom 11382 hvmulassi 11383 hvsubdistr2 11387 hilvc 11498 hhssnv 11601 h1de2bi 11944 spansncol 11958 h1datomi 11971 mayete3i 12140 mayete3OLDi 12141 homulass 12197 kbmul 12348 kbass5 12522 strlem1 12653 |