Theorem 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	|- .0. = ( 0g ` D )
	lfl0.z	|- Z = ( 0g ` W )
	lfl0.f	|- F = ( LFnl ` W )
Assertion	lfl0	|- ( ( W e. LMod /\ G e. F ) -> ( G ` Z ) = .0. )

Proof

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