Axiom ax-hvdistr2 8818

Description: Scalar multiplication distributive law

Assertion

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

Detailed syntax breakdown of Axiom ax-hvdistr2

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		caddc 5217	. . . . 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	1, 6, 12	co 3954	. . . 4 class (A ·h C)
15	4, 6, 12	co 3954	. . . 4 class (B ·h C)
16		cva 8728	. . . 4 class +h
17	14, 15, 16	co 3954	. . 3 class ((A ·h C) +h (B ·h C))
18	13, 17	wceq 954	. 2 wff ((A + B) ·h C) = ((A ·h C) +h (B ·h C))
19	9, 18	wi 3	1 wff ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℋ ) → ((A + B) ·h C) = ((A ·h C) +h (B ·h C)))

This axiom is referenced by:  hvsubidt 8834  hvsubdistr2t 8856  hv2timest 8867  hilvc 8968  hhssnv 9073  hoadddirt 9670  superpos 10218

Copyright terms: Public domain