ldualvsdi1

Description: Distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	ldualvsdi1.f	$⊢ F = LFnl (W)$
	ldualvsdi1.r	$⊢ R = Scalar (W)$
	ldualvsdi1.k	$⊢ K = {Base}_{R}$
	ldualvsdi1.d	$⊢ D = LDual (W)$
	ldualvsdi1.p	$⊢ \underset{˙}{+} = +_{D}$
	ldualvsdi1.s	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	ldualvsdi1.w	$⊢ φ \to W \in LMod$
	ldualvsdi1.x	$⊢ φ \to X \in K$
	ldualvsdi1.g	$⊢ φ \to G \in F$
	ldualvsdi1.h	$⊢ φ \to H \in F$
Assertion	ldualvsdi1	$⊢ φ \to X \underset{˙}{\cdot} (G \underset{˙}{+} H) = (X \underset{˙}{\cdot} G) \underset{˙}{+} (X \underset{˙}{\cdot} H)$

Proof

Step	Hyp	Ref	Expression
1		ldualvsdi1.f	$⊢ F = LFnl (W)$
2		ldualvsdi1.r	$⊢ R = Scalar (W)$
3		ldualvsdi1.k	$⊢ K = {Base}_{R}$
4		ldualvsdi1.d	$⊢ D = LDual (W)$
5		ldualvsdi1.p	$⊢ \underset{˙}{+} = +_{D}$
6		ldualvsdi1.s	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
7		ldualvsdi1.w	$⊢ φ \to W \in LMod$
8		ldualvsdi1.x	$⊢ φ \to X \in K$
9		ldualvsdi1.g	$⊢ φ \to G \in F$
10		ldualvsdi1.h	$⊢ φ \to H \in F$
11		eqid	$⊢ {Base}_{W} = {Base}_{W}$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13	1 11 2 3 12 4 6 7 8 9	ldualvs	$⊢ φ \to X \underset{˙}{\cdot} G = G {\cdot_{R}}_{f} ({Base}_{W} \times \{X\})$
14	1 11 2 3 12 4 6 7 8 10	ldualvs	$⊢ φ \to X \underset{˙}{\cdot} H = H {\cdot_{R}}_{f} ({Base}_{W} \times \{X\})$
15	13 14	oveq12d	$⊢ φ \to (X \underset{˙}{\cdot} G) {+_{R}}_{f} (X \underset{˙}{\cdot} H) = (G {\cdot_{R}}_{f} ({Base}_{W} \times \{X\})) {+_{R}}_{f} (H {\cdot_{R}}_{f} ({Base}_{W} \times \{X\}))$
16		eqid	$⊢ +_{R} = +_{R}$
17	1 2 3 4 6 7 8 9	ldualvscl	$⊢ φ \to X \underset{˙}{\cdot} G \in F$
18	1 2 3 4 6 7 8 10	ldualvscl	$⊢ φ \to X \underset{˙}{\cdot} H \in F$
19	1 2 16 4 5 7 17 18	ldualvadd	$⊢ φ \to (X \underset{˙}{\cdot} G) \underset{˙}{+} (X \underset{˙}{\cdot} H) = (X \underset{˙}{\cdot} G) {+_{R}}_{f} (X \underset{˙}{\cdot} H)$
20	1 4 5 7 9 10	ldualvaddcl	$⊢ φ \to G \underset{˙}{+} H \in F$
21	1 11 2 3 12 4 6 7 8 20	ldualvs	$⊢ φ \to X \underset{˙}{\cdot} (G \underset{˙}{+} H) = (G \underset{˙}{+} H) {\cdot_{R}}_{f} ({Base}_{W} \times \{X\})$
22	1 2 16 4 5 7 9 10	ldualvadd	$⊢ φ \to G \underset{˙}{+} H = G {+_{R}}_{f} H$
23	22	oveq1d	$⊢ φ \to (G \underset{˙}{+} H) {\cdot_{R}}_{f} ({Base}_{W} \times \{X\}) = (G {+_{R}}_{f} H) {\cdot_{R}}_{f} ({Base}_{W} \times \{X\})$
24	11 2 3 16 12 1 7 8 9 10	lflvsdi1	$⊢ φ \to (G {+_{R}}_{f} H) {\cdot_{R}}_{f} ({Base}_{W} \times \{X\}) = (G {\cdot_{R}}_{f} ({Base}_{W} \times \{X\})) {+_{R}}_{f} (H {\cdot_{R}}_{f} ({Base}_{W} \times \{X\}))$
25	21 23 24	3eqtrd	$⊢ φ \to X \underset{˙}{\cdot} (G \underset{˙}{+} H) = (G {\cdot_{R}}_{f} ({Base}_{W} \times \{X\})) {+_{R}}_{f} (H {\cdot_{R}}_{f} ({Base}_{W} \times \{X\}))$
26	15 19 25	3eqtr4rd	$⊢ φ \to X \underset{˙}{\cdot} (G \underset{˙}{+} H) = (X \underset{˙}{\cdot} G) \underset{˙}{+} (X \underset{˙}{\cdot} H)$

Metamath Proof Explorer

Theorem ldualvsdi1

Proof