ipdir

Description: Distributive law for inner product (right-distributivity). Equation I3 of Ponnusamy p. 362. (Contributed by NM, 25-Aug-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	ipdir	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{+} B) \underset{˙}{,} C = (A \underset{˙}{,} C) \underset{˙}{⨣} (B \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		eqid	$⊢ (x \in V ⟼ x \underset{˙}{,} C) = (x \in V ⟼ x \underset{˙}{,} C)$
7	1 2 3 6	phllmhm	$⊢ (W \in PreHil \land C \in V) \to (x \in V ⟼ x \underset{˙}{,} C) \in (W LMHom ringLMod (F))$
8	7	3ad2antr3	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) \in (W LMHom ringLMod (F))$
9		lmghm	$⊢ (x \in V ⟼ x \underset{˙}{,} C) \in (W LMHom ringLMod (F)) \to (x \in V ⟼ x \underset{˙}{,} C) \in (W GrpHom ringLMod (F))$
10	8 9	syl	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) \in (W GrpHom ringLMod (F))$
11		simpr1	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to A \in V$
12		simpr2	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to B \in V$
13		rlmplusg	$⊢ +_{F} = +_{ringLMod (F)}$
14	5 13	eqtri	$⊢ \underset{˙}{⨣} = +_{ringLMod (F)}$
15	3 4 14	ghmlin	$⊢ ((x \in V ⟼ x \underset{˙}{,} C) \in (W GrpHom ringLMod (F)) \land A \in V \land B \in V) \to (x \in V ⟼ x \underset{˙}{,} C) (A \underset{˙}{+} B) = (x \in V ⟼ x \underset{˙}{,} C) (A) \underset{˙}{⨣} (x \in V ⟼ x \underset{˙}{,} C) (B)$
16	10 11 12 15	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) (A \underset{˙}{+} B) = (x \in V ⟼ x \underset{˙}{,} C) (A) \underset{˙}{⨣} (x \in V ⟼ x \underset{˙}{,} C) (B)$
17		phllmod	$⊢ W \in PreHil \to W \in LMod$
18	3 4	lmodvacl	$⊢ (W \in LMod \land A \in V \land B \in V) \to A \underset{˙}{+} B \in V$
19	17 18	syl3an1	$⊢ (W \in PreHil \land A \in V \land B \in V) \to A \underset{˙}{+} B \in V$
20	19	3adant3r3	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to A \underset{˙}{+} B \in V$
21		oveq1	$⊢ x = A \underset{˙}{+} B \to x \underset{˙}{,} C = (A \underset{˙}{+} B) \underset{˙}{,} C$
22		ovex	$⊢ x \underset{˙}{,} C \in V$
23	21 6 22	fvmpt3i	$⊢ A \underset{˙}{+} B \in V \to (x \in V ⟼ x \underset{˙}{,} C) (A \underset{˙}{+} B) = (A \underset{˙}{+} B) \underset{˙}{,} C$
24	20 23	syl	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) (A \underset{˙}{+} B) = (A \underset{˙}{+} B) \underset{˙}{,} C$
25		oveq1	$⊢ x = A \to x \underset{˙}{,} C = A \underset{˙}{,} C$
26	25 6 22	fvmpt3i	$⊢ A \in V \to (x \in V ⟼ x \underset{˙}{,} C) (A) = A \underset{˙}{,} C$
27	11 26	syl	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) (A) = A \underset{˙}{,} C$
28		oveq1	$⊢ x = B \to x \underset{˙}{,} C = B \underset{˙}{,} C$
29	28 6 22	fvmpt3i	$⊢ B \in V \to (x \in V ⟼ x \underset{˙}{,} C) (B) = B \underset{˙}{,} C$
30	12 29	syl	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) (B) = B \underset{˙}{,} C$
31	27 30	oveq12d	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) (A) \underset{˙}{⨣} (x \in V ⟼ x \underset{˙}{,} C) (B) = (A \underset{˙}{,} C) \underset{˙}{⨣} (B \underset{˙}{,} C)$
32	16 24 31	3eqtr3d	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{+} B) \underset{˙}{,} C = (A \underset{˙}{,} C) \underset{˙}{⨣} (B \underset{˙}{,} C)$

Metamath Proof Explorer

Theorem ipdir

Proof