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 28204
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 10136 . . . 4 class
31, 2wcel 2145 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
54, 2wcel 2145 . . 3 wff 𝐵 ∈ ℂ
6 cC . . . 4 class 𝐶
7 chil 28116 . . . 4 class
86, 7wcel 2145 . . 3 wff 𝐶 ∈ ℋ
93, 5, 8w3a 1071 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10 cmul 10143 . . . . 5 class ·
111, 4, 10co 6793 . . . 4 class (𝐴 · 𝐵)
12 csm 28118 . . . 4 class ·
1311, 6, 12co 6793 . . 3 class ((𝐴 · 𝐵) · 𝐶)
144, 6, 12co 6793 . . . 4 class (𝐵 · 𝐶)
151, 14, 12co 6793 . . 3 class (𝐴 · (𝐵 · 𝐶))
1613, 15wceq 1631 . 2 wff ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
179, 16wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0  28221  hvmul0or  28222  hvm1neg  28229  hvmulcom  28240  hvmulassi  28243  hvsubdistr2  28247  hilvc  28359  hhssnv  28461  h1de2bi  28753  spansncol  28767  h1datomi  28780  mayete3i  28927  homulass  29001  kbmul  29154  kbass5  29319  strlem1  29449
  Copyright terms: Public domain W3C validator