lfl0

Description: A linear functional is zero at the zero vector. ( lnfn0i analog.) (Contributed by NM, 16-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lfl0.d	$⊢ D = Scalar (W)$
	lfl0.o	$⊢ \underset{˙}{0} = 0_{D}$
	lfl0.z	$⊢ Z = 0_{W}$
	lfl0.f	$⊢ F = LFnl (W)$
Assertion	lfl0	$⊢ (W \in LMod \land G \in F) \to G (Z) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		lfl0.d	$⊢ D = Scalar (W)$
2		lfl0.o	$⊢ \underset{˙}{0} = 0_{D}$
3		lfl0.z	$⊢ Z = 0_{W}$
4		lfl0.f	$⊢ F = LFnl (W)$
5		simpl	$⊢ (W \in LMod \land G \in F) \to W \in LMod$
6		simpr	$⊢ (W \in LMod \land G \in F) \to G \in F$
7		eqid	$⊢ {Base}_{D} = {Base}_{D}$
8		eqid	$⊢ 1_{D} = 1_{D}$
9	1 7 8	lmod1cl	$⊢ W \in LMod \to 1_{D} \in {Base}_{D}$
10	9	adantr	$⊢ (W \in LMod \land G \in F) \to 1_{D} \in {Base}_{D}$
11		eqid	$⊢ {Base}_{W} = {Base}_{W}$
12	11 3	lmod0vcl	$⊢ W \in LMod \to Z \in {Base}_{W}$
13	12	adantr	$⊢ (W \in LMod \land G \in F) \to Z \in {Base}_{W}$
14		eqid	$⊢ +_{W} = +_{W}$
15		eqid	$⊢ \cdot_{W} = \cdot_{W}$
16		eqid	$⊢ +_{D} = +_{D}$
17		eqid	$⊢ \cdot_{D} = \cdot_{D}$
18	11 14 1 15 7 16 17 4	lfli	$⊢ (W \in LMod \land G \in F \land (1_{D} \in {Base}_{D} \land Z \in {Base}_{W} \land Z \in {Base}_{W})) \to G ((1_{D} \cdot_{W} Z) +_{W} Z) = (1_{D} \cdot_{D} G (Z)) +_{D} G (Z)$
19	5 6 10 13 13 18	syl113anc	$⊢ (W \in LMod \land G \in F) \to G ((1_{D} \cdot_{W} Z) +_{W} Z) = (1_{D} \cdot_{D} G (Z)) +_{D} G (Z)$
20	11 1 15 7	lmodvscl	$⊢ (W \in LMod \land 1_{D} \in {Base}_{D} \land Z \in {Base}_{W}) \to 1_{D} \cdot_{W} Z \in {Base}_{W}$
21	5 10 13 20	syl3anc	$⊢ (W \in LMod \land G \in F) \to 1_{D} \cdot_{W} Z \in {Base}_{W}$
22	11 14 3	lmod0vrid	$⊢ (W \in LMod \land 1_{D} \cdot_{W} Z \in {Base}_{W}) \to (1_{D} \cdot_{W} Z) +_{W} Z = 1_{D} \cdot_{W} Z$
23	21 22	syldan	$⊢ (W \in LMod \land G \in F) \to (1_{D} \cdot_{W} Z) +_{W} Z = 1_{D} \cdot_{W} Z$
24	11 1 15 8	lmodvs1	$⊢ (W \in LMod \land Z \in {Base}_{W}) \to 1_{D} \cdot_{W} Z = Z$
25	13 24	syldan	$⊢ (W \in LMod \land G \in F) \to 1_{D} \cdot_{W} Z = Z$
26	23 25	eqtrd	$⊢ (W \in LMod \land G \in F) \to (1_{D} \cdot_{W} Z) +_{W} Z = Z$
27	26	fveq2d	$⊢ (W \in LMod \land G \in F) \to G ((1_{D} \cdot_{W} Z) +_{W} Z) = G (Z)$
28	1	lmodring	$⊢ W \in LMod \to D \in Ring$
29	28	adantr	$⊢ (W \in LMod \land G \in F) \to D \in Ring$
30	1 7 11 4	lflcl	$⊢ (W \in LMod \land G \in F \land Z \in {Base}_{W}) \to G (Z) \in {Base}_{D}$
31	13 30	mpd3an3	$⊢ (W \in LMod \land G \in F) \to G (Z) \in {Base}_{D}$
32	7 17 8	ringlidm	$⊢ (D \in Ring \land G (Z) \in {Base}_{D}) \to 1_{D} \cdot_{D} G (Z) = G (Z)$
33	29 31 32	syl2anc	$⊢ (W \in LMod \land G \in F) \to 1_{D} \cdot_{D} G (Z) = G (Z)$
34	33	oveq1d	$⊢ (W \in LMod \land G \in F) \to (1_{D} \cdot_{D} G (Z)) +_{D} G (Z) = G (Z) +_{D} G (Z)$
35	19 27 34	3eqtr3d	$⊢ (W \in LMod \land G \in F) \to G (Z) = G (Z) +_{D} G (Z)$
36	35	oveq1d	$⊢ (W \in LMod \land G \in F) \to G (Z) -_{D} G (Z) = (G (Z) +_{D} G (Z)) -_{D} G (Z)$
37		ringgrp	$⊢ D \in Ring \to D \in Grp$
38	29 37	syl	$⊢ (W \in LMod \land G \in F) \to D \in Grp$
39		eqid	$⊢ -_{D} = -_{D}$
40	7 2 39	grpsubid	$⊢ (D \in Grp \land G (Z) \in {Base}_{D}) \to G (Z) -_{D} G (Z) = \underset{˙}{0}$
41	38 31 40	syl2anc	$⊢ (W \in LMod \land G \in F) \to G (Z) -_{D} G (Z) = \underset{˙}{0}$
42	7 16 39	grppncan	$⊢ (D \in Grp \land G (Z) \in {Base}_{D} \land G (Z) \in {Base}_{D}) \to (G (Z) +_{D} G (Z)) -_{D} G (Z) = G (Z)$
43	38 31 31 42	syl3anc	$⊢ (W \in LMod \land G \in F) \to (G (Z) +_{D} G (Z)) -_{D} G (Z) = G (Z)$
44	36 41 43	3eqtr3rd	$⊢ (W \in LMod \land G \in F) \to G (Z) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem lfl0

Proof