Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hvmulass Structured version   Visualization version   GIF version

Axiom ax-hvmulass 27248
 Description: Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvmulass ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Detailed syntax breakdown of Axiom ax-hvmulass
StepHypRef Expression
1 cA . . . 4 class 𝐴
2 cc 9813 . . . 4 class
31, 2wcel 1977 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
54, 2wcel 1977 . . 3 wff 𝐵 ∈ ℂ
6 cC . . . 4 class 𝐶
7 chil 27160 . . . 4 class
86, 7wcel 1977 . . 3 wff 𝐶 ∈ ℋ
93, 5, 8w3a 1031 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10 cmul 9820 . . . . 5 class ·
111, 4, 10co 6549 . . . 4 class (𝐴 · 𝐵)
12 csm 27162 . . . 4 class ·
1311, 6, 12co 6549 . . 3 class ((𝐴 · 𝐵) · 𝐶)
144, 6, 12co 6549 . . . 4 class (𝐵 · 𝐶)
151, 14, 12co 6549 . . 3 class (𝐴 · (𝐵 · 𝐶))
1613, 15wceq 1475 . 2 wff ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
179, 16wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
 Colors of variables: wff setvar class This axiom is referenced by:  hvmul0  27265  hvmul0or  27266  hvm1neg  27273  hvmulcom  27284  hvmulassi  27287  hvsubdistr2  27291  hilvc  27403  hhssnv  27505  h1de2bi  27797  spansncol  27811  h1datomi  27824  mayete3i  27971  homulass  28045  kbmul  28198  kbass5  28363  strlem1  28493
 Copyright terms: Public domain W3C validator