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 28776
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 10527 . . . 4 class
31, 2wcel 2108 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
54, 2wcel 2108 . . 3 wff 𝐵 ∈ ℂ
6 cC . . . 4 class 𝐶
7 chba 28688 . . . 4 class
86, 7wcel 2108 . . 3 wff 𝐶 ∈ ℋ
93, 5, 8w3a 1082 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10 cmul 10534 . . . . 5 class ·
111, 4, 10co 7148 . . . 4 class (𝐴 · 𝐵)
12 csm 28690 . . . 4 class ·
1311, 6, 12co 7148 . . 3 class ((𝐴 · 𝐵) · 𝐶)
144, 6, 12co 7148 . . . 4 class (𝐵 · 𝐶)
151, 14, 12co 7148 . . 3 class (𝐴 · (𝐵 · 𝐶))
1613, 15wceq 1531 . 2 wff ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
179, 16wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0  28793  hvmul0or  28794  hvm1neg  28801  hvmulcom  28812  hvmulassi  28815  hvsubdistr2  28819  hilvc  28931  hhssnv  29033  h1de2bi  29323  spansncol  29337  h1datomi  29350  mayete3i  29497  homulass  29571  kbmul  29724  kbass5  29889  strlem1  30019
  Copyright terms: Public domain W3C validator