ax-his2

Description: Distributive law for inner product. Postulate (S2) of Beran p. 95. (Contributed by NM, 31-Jul-1999) (New usage is discouraged.)

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

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

Metamath Proof Explorer