lflmul

Description: Property of a linear functional. ( lnfnmuli analog.) (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	lflmul.d	$⊢ D = Scalar (W)$
	lflmul.k	$⊢ K = {Base}_{D}$
	lflmul.t	$⊢ \underset{˙}{\times} = \cdot_{D}$
	lflmul.v	$⊢ V = {Base}_{W}$
	lflmul.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lflmul.f	$⊢ F = LFnl (W)$
Assertion	lflmul	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to G (R \underset{˙}{\cdot} X) = R \underset{˙}{\times} G (X)$

Proof

Step	Hyp	Ref	Expression
1		lflmul.d	$⊢ D = Scalar (W)$
2		lflmul.k	$⊢ K = {Base}_{D}$
3		lflmul.t	$⊢ \underset{˙}{\times} = \cdot_{D}$
4		lflmul.v	$⊢ V = {Base}_{W}$
5		lflmul.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		lflmul.f	$⊢ F = LFnl (W)$
7		simp1	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to W \in LMod$
8		simp2	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to G \in F$
9		simp3l	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to R \in K$
10		simp3r	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to X \in V$
11		eqid	$⊢ 0_{W} = 0_{W}$
12	4 11	lmod0vcl	$⊢ W \in LMod \to 0_{W} \in V$
13	12	3ad2ant1	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to 0_{W} \in V$
14		eqid	$⊢ +_{W} = +_{W}$
15		eqid	$⊢ +_{D} = +_{D}$
16	4 14 1 5 2 15 3 6	lfli	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V \land 0_{W} \in V)) \to G ((R \underset{˙}{\cdot} X) +_{W} 0_{W}) = (R \underset{˙}{\times} G (X)) +_{D} G (0_{W})$
17	7 8 9 10 13 16	syl113anc	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to G ((R \underset{˙}{\cdot} X) +_{W} 0_{W}) = (R \underset{˙}{\times} G (X)) +_{D} G (0_{W})$
18	4 1 5 2	lmodvscl	$⊢ (W \in LMod \land R \in K \land X \in V) \to R \underset{˙}{\cdot} X \in V$
19	7 9 10 18	syl3anc	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to R \underset{˙}{\cdot} X \in V$
20	4 14 11	lmod0vrid	$⊢ (W \in LMod \land R \underset{˙}{\cdot} X \in V) \to (R \underset{˙}{\cdot} X) +_{W} 0_{W} = R \underset{˙}{\cdot} X$
21	7 19 20	syl2anc	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to (R \underset{˙}{\cdot} X) +_{W} 0_{W} = R \underset{˙}{\cdot} X$
22	21	fveq2d	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to G ((R \underset{˙}{\cdot} X) +_{W} 0_{W}) = G (R \underset{˙}{\cdot} X)$
23		eqid	$⊢ 0_{D} = 0_{D}$
24	1 23 11 6	lfl0	$⊢ (W \in LMod \land G \in F) \to G (0_{W}) = 0_{D}$
25	24	3adant3	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to G (0_{W}) = 0_{D}$
26	25	oveq2d	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to (R \underset{˙}{\times} G (X)) +_{D} G (0_{W}) = (R \underset{˙}{\times} G (X)) +_{D} 0_{D}$
27	1	lmodfgrp	$⊢ W \in LMod \to D \in Grp$
28	27	3ad2ant1	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to D \in Grp$
29	1 2 4 6	lflcl	$⊢ (W \in LMod \land G \in F \land X \in V) \to G (X) \in K$
30	29	3adant3l	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to G (X) \in K$
31	1 2 3	lmodmcl	$⊢ (W \in LMod \land R \in K \land G (X) \in K) \to R \underset{˙}{\times} G (X) \in K$
32	7 9 30 31	syl3anc	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to R \underset{˙}{\times} G (X) \in K$
33	2 15 23	grprid	$⊢ (D \in Grp \land R \underset{˙}{\times} G (X) \in K) \to (R \underset{˙}{\times} G (X)) +_{D} 0_{D} = R \underset{˙}{\times} G (X)$
34	28 32 33	syl2anc	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to (R \underset{˙}{\times} G (X)) +_{D} 0_{D} = R \underset{˙}{\times} G (X)$
35	26 34	eqtrd	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to (R \underset{˙}{\times} G (X)) +_{D} G (0_{W}) = R \underset{˙}{\times} G (X)$
36	17 22 35	3eqtr3d	$⊢ (W \in LMod \land G \in F \land (R \in K \land X \in V)) \to G (R \underset{˙}{\cdot} X) = R \underset{˙}{\times} G (X)$

Metamath Proof Explorer

Theorem lflmul

Proof