lflvsdi2a

Description: Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 21-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$
	lfldi2.y	$⊢ φ \to Y \in K$
	lfldi2.g	$⊢ φ \to G \in F$
Assertion	lflvsdi2a	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{X \underset{˙}{+} Y\}) = (G {\underset{˙}{\cdot}}_{f} (V \times \{X\})) {\underset{˙}{+}}_{f} (G {\underset{˙}{\cdot}}_{f} (V \times \{Y\}))$

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		lfldi2.y	$⊢ φ \to Y \in K$
10		lfldi2.g	$⊢ φ \to G \in F$
11	1	fvexi	$⊢ V \in V$
12	11	a1i	$⊢ φ \to V \in V$
13	12 8 9	ofc12	$⊢ φ \to (V \times \{X\}) {\underset{˙}{+}}_{f} (V \times \{Y\}) = V \times \{X \underset{˙}{+} Y\}$
14	13	oveq2d	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} ((V \times \{X\}) {\underset{˙}{+}}_{f} (V \times \{Y\})) = G {\underset{˙}{\cdot}}_{f} (V \times \{X \underset{˙}{+} Y\})$
15	1 2 3 4 5 6 7 8 9 10	lflvsdi2	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} ((V \times \{X\}) {\underset{˙}{+}}_{f} (V \times \{Y\})) = (G {\underset{˙}{\cdot}}_{f} (V \times \{X\})) {\underset{˙}{+}}_{f} (G {\underset{˙}{\cdot}}_{f} (V \times \{Y\}))$
16	14 15	eqtr3d	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{X \underset{˙}{+} Y\}) = (G {\underset{˙}{\cdot}}_{f} (V \times \{X\})) {\underset{˙}{+}}_{f} (G {\underset{˙}{\cdot}}_{f} (V \times \{Y\}))$

Metamath Proof Explorer