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 27030
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 9693 . . . 4 class
31, 2wcel 1938 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
54, 2wcel 1938 . . 3 wff 𝐵 ∈ ℂ
6 cC . . . 4 class 𝐶
7 chil 26942 . . . 4 class
86, 7wcel 1938 . . 3 wff 𝐶 ∈ ℋ
93, 5, 8w3a 1030 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10 cmul 9700 . . . . 5 class ·
111, 4, 10co 6431 . . . 4 class (𝐴 · 𝐵)
12 csm 26944 . . . 4 class ·
1311, 6, 12co 6431 . . 3 class ((𝐴 · 𝐵) · 𝐶)
144, 6, 12co 6431 . . . 4 class (𝐵 · 𝐶)
151, 14, 12co 6431 . . 3 class (𝐴 · (𝐵 · 𝐶))
1613, 15wceq 1474 . 2 wff ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
179, 16wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0  27047  hvmul0or  27048  hvm1neg  27055  hvmulcom  27066  hvmulassi  27069  hvsubdistr2  27073  hilvc  27185  hhssnv  27287  h1de2bi  27579  spansncol  27593  h1datomi  27606  mayete3i  27753  homulass  27827  kbmul  27980  kbass5  28145  strlem1  28275
  Copyright terms: Public domain W3C validator