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 27992
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 9972 . . . 4 class
31, 2wcel 2030 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
54, 2wcel 2030 . . 3 wff 𝐵 ∈ ℂ
6 cC . . . 4 class 𝐶
7 chil 27904 . . . 4 class
86, 7wcel 2030 . . 3 wff 𝐶 ∈ ℋ
93, 5, 8w3a 1054 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10 cmul 9979 . . . . 5 class ·
111, 4, 10co 6690 . . . 4 class (𝐴 · 𝐵)
12 csm 27906 . . . 4 class ·
1311, 6, 12co 6690 . . 3 class ((𝐴 · 𝐵) · 𝐶)
144, 6, 12co 6690 . . . 4 class (𝐵 · 𝐶)
151, 14, 12co 6690 . . 3 class (𝐴 · (𝐵 · 𝐶))
1613, 15wceq 1523 . 2 wff ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
179, 16wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0  28009  hvmul0or  28010  hvm1neg  28017  hvmulcom  28028  hvmulassi  28031  hvsubdistr2  28035  hilvc  28147  hhssnv  28249  h1de2bi  28541  spansncol  28555  h1datomi  28568  mayete3i  28715  homulass  28789  kbmul  28942  kbass5  29107  strlem1  29237
  Copyright terms: Public domain W3C validator