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 27834
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 9919 . . . 4 class
31, 2wcel 1988 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
54, 2wcel 1988 . . 3 wff 𝐵 ∈ ℂ
6 cC . . . 4 class 𝐶
7 chil 27746 . . . 4 class
86, 7wcel 1988 . . 3 wff 𝐶 ∈ ℋ
93, 5, 8w3a 1036 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10 cmul 9926 . . . . 5 class ·
111, 4, 10co 6635 . . . 4 class (𝐴 · 𝐵)
12 csm 27748 . . . 4 class ·
1311, 6, 12co 6635 . . 3 class ((𝐴 · 𝐵) · 𝐶)
144, 6, 12co 6635 . . . 4 class (𝐵 · 𝐶)
151, 14, 12co 6635 . . 3 class (𝐴 · (𝐵 · 𝐶))
1613, 15wceq 1481 . 2 wff ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
179, 16wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0  27851  hvmul0or  27852  hvm1neg  27859  hvmulcom  27870  hvmulassi  27873  hvsubdistr2  27877  hilvc  27989  hhssnv  28091  h1de2bi  28383  spansncol  28397  h1datomi  28410  mayete3i  28557  homulass  28631  kbmul  28784  kbass5  28949  strlem1  29079
  Copyright terms: Public domain W3C validator