lfladd

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

	Ref	Expression
Hypotheses	lfladd.d	$⊢ D = Scalar (W)$
	lfladd.p	$⊢ \underset{˙}{⨣} = +_{D}$
	lfladd.v	$⊢ V = {Base}_{W}$
	lfladd.a	$⊢ \underset{˙}{+} = +_{W}$
	lfladd.f	$⊢ F = LFnl (W)$
Assertion	lfladd	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X \underset{˙}{+} Y) = G (X) \underset{˙}{⨣} G (Y)$

Proof

Step	Hyp	Ref	Expression
1		lfladd.d	$⊢ D = Scalar (W)$
2		lfladd.p	$⊢ \underset{˙}{⨣} = +_{D}$
3		lfladd.v	$⊢ V = {Base}_{W}$
4		lfladd.a	$⊢ \underset{˙}{+} = +_{W}$
5		lfladd.f	$⊢ F = LFnl (W)$
6		simp1	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to W \in LMod$
7		simp2	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G \in F$
8		eqid	$⊢ {Base}_{D} = {Base}_{D}$
9		eqid	$⊢ 1_{D} = 1_{D}$
10	1 8 9	lmod1cl	$⊢ W \in LMod \to 1_{D} \in {Base}_{D}$
11	10	3ad2ant1	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to 1_{D} \in {Base}_{D}$
12		simp3l	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to X \in V$
13		simp3r	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to Y \in V$
14		eqid	$⊢ \cdot_{W} = \cdot_{W}$
15		eqid	$⊢ \cdot_{D} = \cdot_{D}$
16	3 4 1 14 8 2 15 5	lfli	$⊢ (W \in LMod \land G \in F \land (1_{D} \in {Base}_{D} \land X \in V \land Y \in V)) \to G ((1_{D} \cdot_{W} X) \underset{˙}{+} Y) = (1_{D} \cdot_{D} G (X)) \underset{˙}{⨣} G (Y)$
17	6 7 11 12 13 16	syl113anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G ((1_{D} \cdot_{W} X) \underset{˙}{+} Y) = (1_{D} \cdot_{D} G (X)) \underset{˙}{⨣} G (Y)$
18	3 1 14 9	lmodvs1	$⊢ (W \in LMod \land X \in V) \to 1_{D} \cdot_{W} X = X$
19	6 12 18	syl2anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to 1_{D} \cdot_{W} X = X$
20	19	fvoveq1d	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G ((1_{D} \cdot_{W} X) \underset{˙}{+} Y) = G (X \underset{˙}{+} Y)$
21	1	lmodring	$⊢ W \in LMod \to D \in Ring$
22	21	3ad2ant1	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to D \in Ring$
23	1 8 3 5	lflcl	$⊢ (W \in LMod \land G \in F \land X \in V) \to G (X) \in {Base}_{D}$
24	23	3adant3r	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X) \in {Base}_{D}$
25	8 15 9	ringlidm	$⊢ (D \in Ring \land G (X) \in {Base}_{D}) \to 1_{D} \cdot_{D} G (X) = G (X)$
26	22 24 25	syl2anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to 1_{D} \cdot_{D} G (X) = G (X)$
27	26	oveq1d	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to (1_{D} \cdot_{D} G (X)) \underset{˙}{⨣} G (Y) = G (X) \underset{˙}{⨣} G (Y)$
28	17 20 27	3eqtr3d	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X \underset{˙}{+} Y) = G (X) \underset{˙}{⨣} G (Y)$

Metamath Proof Explorer

Theorem lfladd

Proof