Axiom ax-hvdistr1

Description: Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hvdistr1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·ℎ ( 𝐵 +ℎ 𝐶 ) ) = ( ( 𝐴 ·ℎ 𝐵 ) +ℎ ( 𝐴 ·ℎ 𝐶 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cc	⊢ ℂ
2	0 1	wcel	⊢ 𝐴 ∈ ℂ
3		cB	⊢ 𝐵
4		chba	⊢ ℋ
5	3 4	wcel	⊢ 𝐵 ∈ ℋ
6		cC	⊢ 𝐶
7	6 4	wcel	⊢ 𝐶 ∈ ℋ
8	2 5 7	w3a	⊢ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ )
9		csm	⊢ ·ℎ
10		cva	⊢ +ℎ
11	3 6 10	co	⊢ ( 𝐵 +ℎ 𝐶 )
12	0 11 9	co	⊢ ( 𝐴 ·ℎ ( 𝐵 +ℎ 𝐶 ) )
13	0 3 9	co	⊢ ( 𝐴 ·ℎ 𝐵 )
14	0 6 9	co	⊢ ( 𝐴 ·ℎ 𝐶 )
15	13 14 10	co	⊢ ( ( 𝐴 ·ℎ 𝐵 ) +ℎ ( 𝐴 ·ℎ 𝐶 ) )
16	12 15	wceq	⊢ ( 𝐴 ·ℎ ( 𝐵 +ℎ 𝐶 ) ) = ( ( 𝐴 ·ℎ 𝐵 ) +ℎ ( 𝐴 ·ℎ 𝐶 ) )
17	8 16	wi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·ℎ ( 𝐵 +ℎ 𝐶 ) ) = ( ( 𝐴 ·ℎ 𝐵 ) +ℎ ( 𝐴 ·ℎ 𝐶 ) ) )