This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. )