ax-hvdistr1

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

		Ref	Expression
	Assertion	ax-hvdistr1	$⊢ (A \in ℂ \land B \in ℋ \land C \in ℋ) \to A \cdot_{ℎ} (B +_{ℎ} C) = (A \cdot_{ℎ} B) +_{ℎ} (A \cdot_{ℎ} C)$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cc	$class ℂ$
2	0 1	wcel	$wff A \in ℂ$
3		cB	$class B$
4		chba	$class ℋ$
5	3 4	wcel	$wff B \in ℋ$
6		cC	$class C$
7	6 4	wcel	$wff C \in ℋ$
8	2 5 7	w3a	$wff (A \in ℂ \land B \in ℋ \land C \in ℋ)$
9		csm	$class \cdot_{ℎ}$
10		cva	$class +_{ℎ}$
11	3 6 10	co	$class (B +_{ℎ} C)$
12	0 11 9	co	$class (A \cdot_{ℎ} (B +_{ℎ} C))$
13	0 3 9	co	$class (A \cdot_{ℎ} B)$
14	0 6 9	co	$class (A \cdot_{ℎ} C)$
15	13 14 10	co	$class ((A \cdot_{ℎ} B) +_{ℎ} (A \cdot_{ℎ} C))$
16	12 15	wceq	$wff A \cdot_{ℎ} (B +_{ℎ} C) = (A \cdot_{ℎ} B) +_{ℎ} (A \cdot_{ℎ} C)$
17	8 16	wi	$wff ((A \in ℂ \land B \in ℋ \land C \in ℋ) \to A \cdot_{ℎ} (B +_{ℎ} C) = (A \cdot_{ℎ} B) +_{ℎ} (A \cdot_{ℎ} C))$

Metamath Proof Explorer