Axiom ax-hvmulass 8901

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 5252	. . . 4 class ℂ
3	1, 2	wcel 962	. . 3 wff A ∈ ℂ
4		cB	. . . 4 class B
5	4, 2	wcel 962	. . 3 wff B ∈ ℂ
6		cC	. . . 4 class C
7		chil 8812	. . . 4 class ℋ
8	6, 7	wcel 962	. . 3 wff C ∈ ℋ
9	3, 5, 8	w3a 779	. 2 wff (A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℋ )
10		cmul 5259	. . . . 5 class ·
11	1, 4, 10	co 3979	. . . 4 class (A · B)
12		csm 8814	. . . 4 class ·h
13	11, 6, 12	co 3979	. . 3 class ((A · B) ·h C)
14	4, 6, 12	co 3979	. . . 4 class (B ·h C)
15	1, 14, 12	co 3979	. . 3 class (A ·h (B ·h C))
16	13, 15	wceq 960	. 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:  hvmul0 8917  hvmul0or 8918  hvm1neg 8925  hvmulcom 8936  hvmulassi 8937  hvsubdistr2 8941  hilvc 9053  hhssnv 9158  h1de2bi 9501  spansncol 9515  h1datomi 9528  mayete3i 9697  homulass 9752  kbmul 9903  kbass5 10077  strlem1 10202

Copyright terms: Public domain