Axiom ax-hvmulass 8816

Description: Scalar multiplication associative law

Assertion

Ref	Expression
ax-hvmulass	⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℋ ) → ((A · B) ·h C) = (A ·h (B ·h C)))

Detailed syntax breakdown of Axiom ax-hvmulass

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 5212	. . . 4 class ℂ
3	1, 2	wcel 956	. . 3 wff A ∈ ℂ
4		cB	. . . 4 class B
5	4, 2	wcel 956	. . 3 wff B ∈ ℂ
6		cC	. . . 4 class C
7		chil 8727	. . . 4 class ℋ
8	6, 7	wcel 956	. . 3 wff C ∈ ℋ
9	3, 5, 8	w3a 774	. 2 wff (A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℋ )
10		cmul 5219	. . . . 5 class ·
11	1, 4, 10	co 3954	. . . 4 class (A · B)
12		csm 8729	. . . 4 class ·h
13	11, 6, 12	co 3954	. . 3 class ((A · B) ·h C)
14	4, 6, 12	co 3954	. . . 4 class (B ·h C)
15	1, 14, 12	co 3954	. . 3 class (A ·h (B ·h C))
16	13, 15	wceq 954	. 2 wff ((A · B) ·h C) = (A ·h (B ·h C))
17	9, 16	wi 3	1 wff ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℋ ) → ((A · B) ·h C) = (A ·h (B ·h C)))

This axiom is referenced by:  hvmul0t 8832  hvmul0ort 8833  hvm1negt 8840  hvmulcomt 8851  hvmulass 8852  hvsubdistr2t 8856  hilvc 8968  hhssnv 9073  h1de2b 9415  h1de2bOLD 9416  spansncol 9430  h1datom 9444  mayete3 9613  homulasst 9668  kbmult 9818  kbass5t 9991  strlem1 10115

Copyright terms: Public domain