lflvsdi1

Description: Distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014)

	Ref	Expression
Hypotheses	lfldi.v	$⊢ V = {Base}_{W}$
	lfldi.r	$⊢ R = Scalar (W)$
	lfldi.k	$⊢ K = {Base}_{R}$
	lfldi.p	$⊢ \underset{˙}{+} = +_{R}$
	lfldi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	lfldi.f	$⊢ F = LFnl (W)$
	lfldi.w	$⊢ φ \to W \in LMod$
	lfldi.x	$⊢ φ \to X \in K$
	lfldi1.g	$⊢ φ \to G \in F$
	lfldi1.h	$⊢ φ \to H \in F$
Assertion	lflvsdi1	$⊢ φ \to (G {\underset{˙}{+}}_{f} H) {\underset{˙}{\cdot}}_{f} (V \times \{X\}) = (G {\underset{˙}{\cdot}}_{f} (V \times \{X\})) {\underset{˙}{+}}_{f} (H {\underset{˙}{\cdot}}_{f} (V \times \{X\}))$

Step	Hyp	Ref	Expression
1		lfldi.v	$⊢ V = {Base}_{W}$
2		lfldi.r	$⊢ R = Scalar (W)$
3		lfldi.k	$⊢ K = {Base}_{R}$
4		lfldi.p	$⊢ \underset{˙}{+} = +_{R}$
5		lfldi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		lfldi.f	$⊢ F = LFnl (W)$
7		lfldi.w	$⊢ φ \to W \in LMod$
8		lfldi.x	$⊢ φ \to X \in K$
9		lfldi1.g	$⊢ φ \to G \in F$
10		lfldi1.h	$⊢ φ \to H \in F$
11	1	fvexi	$⊢ V \in V$
12	11	a1i	$⊢ φ \to V \in V$
13		fconst6g	$⊢ X \in K \to (V \times \{X\}) : V ⟶ K$
14	8 13	syl	$⊢ φ \to (V \times \{X\}) : V ⟶ K$
15	2 3 1 6	lflf	$⊢ (W \in LMod \land G \in F) \to G : V ⟶ K$
16	7 9 15	syl2anc	$⊢ φ \to G : V ⟶ K$
17	2 3 1 6	lflf	$⊢ (W \in LMod \land H \in F) \to H : V ⟶ K$
18	7 10 17	syl2anc	$⊢ φ \to H : V ⟶ K$
19	2	lmodring	$⊢ W \in LMod \to R \in Ring$
20	7 19	syl	$⊢ φ \to R \in Ring$
21	3 4 5	ringdir	$⊢ (R \in Ring \land (x \in K \land y \in K \land z \in K)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
22	20 21	sylan	$⊢ (φ \land (x \in K \land y \in K \land z \in K)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
23	12 14 16 18 22	caofdir	$⊢ φ \to (G {\underset{˙}{+}}_{f} H) {\underset{˙}{\cdot}}_{f} (V \times \{X\}) = (G {\underset{˙}{\cdot}}_{f} (V \times \{X\})) {\underset{˙}{+}}_{f} (H {\underset{˙}{\cdot}}_{f} (V \times \{X\}))$

Metamath Proof Explorer