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

Axiom ax-hvmulass 31026
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 11153 . . . 4 class
31, 2wcel 2108 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
54, 2wcel 2108 . . 3 wff 𝐵 ∈ ℂ
6 cC . . . 4 class 𝐶
7 chba 30938 . . . 4 class
86, 7wcel 2108 . . 3 wff 𝐶 ∈ ℋ
93, 5, 8w3a 1087 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10 cmul 11160 . . . . 5 class ·
111, 4, 10co 7431 . . . 4 class (𝐴 · 𝐵)
12 csm 30940 . . . 4 class ·
1311, 6, 12co 7431 . . 3 class ((𝐴 · 𝐵) · 𝐶)
144, 6, 12co 7431 . . . 4 class (𝐵 · 𝐶)
151, 14, 12co 7431 . . 3 class (𝐴 · (𝐵 · 𝐶))
1613, 15wceq 1540 . 2 wff ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
179, 16wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0  31043  hvmul0or  31044  hvm1neg  31051  hvmulcom  31062  hvmulassi  31065  hvsubdistr2  31069  hilvc  31181  hhssnv  31283  h1de2bi  31573  spansncol  31587  h1datomi  31600  mayete3i  31747  homulass  31821  kbmul  31974  kbass5  32139  strlem1  32269
  Copyright terms: Public domain W3C validator