ipdi

Description: Distributive law for inner product (left-distributivity). (Contributed by NM, 20-Nov-2007) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	$⊢ F = Scalar (W)$
	phllmhm.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	phllmhm.v	$⊢ V = {Base}_{W}$
	ipdir.g	$⊢ \underset{˙}{+} = +_{W}$
	ipdir.p	$⊢ \underset{˙}{⨣} = +_{F}$
Assertion	ipdi	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to A \underset{˙}{,} (B \underset{˙}{+} C) = (A \underset{˙}{,} B) \underset{˙}{⨣} (A \underset{˙}{,} C)$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$⊢ F = Scalar (W)$
2		phllmhm.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		phllmhm.v	$⊢ V = {Base}_{W}$
4		ipdir.g	$⊢ \underset{˙}{+} = +_{W}$
5		ipdir.p	$⊢ \underset{˙}{⨣} = +_{F}$
6		simpl	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to W \in PreHil$
7		simpr2	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to B \in V$
8		simpr3	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to C \in V$
9		simpr1	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to A \in V$
10	1 2 3 4 5	ipdir	$⊢ (W \in PreHil \land (B \in V \land C \in V \land A \in V)) \to (B \underset{˙}{+} C) \underset{˙}{,} A = (B \underset{˙}{,} A) \underset{˙}{⨣} (C \underset{˙}{,} A)$
11	6 7 8 9 10	syl13anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (B \underset{˙}{+} C) \underset{˙}{,} A = (B \underset{˙}{,} A) \underset{˙}{⨣} (C \underset{˙}{,} A)$
12	11	fveq2d	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to {((B \underset{˙}{+} C) \underset{˙}{,} A)}^{_{F}} = {((B \underset{˙}{,} A) \underset{˙}{⨣} (C \underset{˙}{,} A))}^{_{F}}$
13	1	phlsrng	$⊢ W \in PreHil \to F \in *-Ring$
14	13	adantr	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to F \in *-Ring$
15		eqid	$⊢ {Base}_{F} = {Base}_{F}$
16	1 2 3 15	ipcl	$⊢ (W \in PreHil \land B \in V \land A \in V) \to B \underset{˙}{,} A \in {Base}_{F}$
17	6 7 9 16	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to B \underset{˙}{,} A \in {Base}_{F}$
18	1 2 3 15	ipcl	$⊢ (W \in PreHil \land C \in V \land A \in V) \to C \underset{˙}{,} A \in {Base}_{F}$
19	6 8 9 18	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to C \underset{˙}{,} A \in {Base}_{F}$
20		eqid	$⊢ _{F} = _{F}$
21	20 15 5	srngadd	$⊢ (F \in -Ring \land B \underset{˙}{,} A \in {Base}_{F} \land C \underset{˙}{,} A \in {Base}_{F}) \to {((B \underset{˙}{,} A) \underset{˙}{⨣} (C \underset{˙}{,} A))}^{_{F}} = {(B \underset{˙}{,} A)}^{_{F}} \underset{˙}{⨣} {(C \underset{˙}{,} A)}^{_{F}}$
22	14 17 19 21	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to {((B \underset{˙}{,} A) \underset{˙}{⨣} (C \underset{˙}{,} A))}^{_{F}} = {(B \underset{˙}{,} A)}^{_{F}} \underset{˙}{⨣} {(C \underset{˙}{,} A)}^{*_{F}}$
23	12 22	eqtrd	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to {((B \underset{˙}{+} C) \underset{˙}{,} A)}^{_{F}} = {(B \underset{˙}{,} A)}^{_{F}} \underset{˙}{⨣} {(C \underset{˙}{,} A)}^{*_{F}}$
24		phllmod	$⊢ W \in PreHil \to W \in LMod$
25	24	adantr	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to W \in LMod$
26	3 4	lmodvacl	$⊢ (W \in LMod \land B \in V \land C \in V) \to B \underset{˙}{+} C \in V$
27	25 7 8 26	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to B \underset{˙}{+} C \in V$
28	1 2 3 20	ipcj	$⊢ (W \in PreHil \land B \underset{˙}{+} C \in V \land A \in V) \to {((B \underset{˙}{+} C) \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} (B \underset{˙}{+} C)$
29	6 27 9 28	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to {((B \underset{˙}{+} C) \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} (B \underset{˙}{+} C)$
30	1 2 3 20	ipcj	$⊢ (W \in PreHil \land B \in V \land A \in V) \to {(B \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} B$
31	6 7 9 30	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to {(B \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} B$
32	1 2 3 20	ipcj	$⊢ (W \in PreHil \land C \in V \land A \in V) \to {(C \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} C$
33	6 8 9 32	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to {(C \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} C$
34	31 33	oveq12d	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to {(B \underset{˙}{,} A)}^{_{F}} \underset{˙}{⨣} {(C \underset{˙}{,} A)}^{_{F}} = (A \underset{˙}{,} B) \underset{˙}{⨣} (A \underset{˙}{,} C)$
35	23 29 34	3eqtr3d	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to A \underset{˙}{,} (B \underset{˙}{+} C) = (A \underset{˙}{,} B) \underset{˙}{⨣} (A \underset{˙}{,} C)$

Metamath Proof Explorer

Theorem ipdi

Proof