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 28436
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 10270 . . . 4 class
31, 2wcel 2107 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
54, 2wcel 2107 . . 3 wff 𝐵 ∈ ℂ
6 cC . . . 4 class 𝐶
7 chba 28348 . . . 4 class
86, 7wcel 2107 . . 3 wff 𝐶 ∈ ℋ
93, 5, 8w3a 1071 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10 cmul 10277 . . . . 5 class ·
111, 4, 10co 6922 . . . 4 class (𝐴 · 𝐵)
12 csm 28350 . . . 4 class ·
1311, 6, 12co 6922 . . 3 class ((𝐴 · 𝐵) · 𝐶)
144, 6, 12co 6922 . . . 4 class (𝐵 · 𝐶)
151, 14, 12co 6922 . . 3 class (𝐴 · (𝐵 · 𝐶))
1613, 15wceq 1601 . 2 wff ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
179, 16wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0  28453  hvmul0or  28454  hvm1neg  28461  hvmulcom  28472  hvmulassi  28475  hvsubdistr2  28479  hilvc  28591  hhssnv  28693  h1de2bi  28985  spansncol  28999  h1datomi  29012  mayete3i  29159  homulass  29233  kbmul  29386  kbass5  29551  strlem1  29681
  Copyright terms: Public domain W3C validator