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 30123
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 11090 . . . 4 class
31, 2wcel 2106 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
54, 2wcel 2106 . . 3 wff 𝐵 ∈ ℂ
6 cC . . . 4 class 𝐶
7 chba 30035 . . . 4 class
86, 7wcel 2106 . . 3 wff 𝐶 ∈ ℋ
93, 5, 8w3a 1087 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10 cmul 11097 . . . . 5 class ·
111, 4, 10co 7393 . . . 4 class (𝐴 · 𝐵)
12 csm 30037 . . . 4 class ·
1311, 6, 12co 7393 . . 3 class ((𝐴 · 𝐵) · 𝐶)
144, 6, 12co 7393 . . . 4 class (𝐵 · 𝐶)
151, 14, 12co 7393 . . 3 class (𝐴 · (𝐵 · 𝐶))
1613, 15wceq 1541 . 2 wff ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
179, 16wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0  30140  hvmul0or  30141  hvm1neg  30148  hvmulcom  30159  hvmulassi  30162  hvsubdistr2  30166  hilvc  30278  hhssnv  30380  h1de2bi  30670  spansncol  30684  h1datomi  30697  mayete3i  30844  homulass  30918  kbmul  31071  kbass5  31236  strlem1  31366
  Copyright terms: Public domain W3C validator