Metamath Proof Explorer

Theorem lfl0f

Description: The zero function is a functional. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lfl0f.d 
|- D = ( Scalar ` W )
lfl0f.o 
|- .0. = ( 0g ` D )
lfl0f.v 
|- V = ( Base ` W )
lfl0f.f 
|- F = ( LFnl ` W )
Assertion lfl0f 
|- ( W e. LMod -> ( V X. { .0. } ) e. F )

Proof

Step Hyp Ref Expression
1 lfl0f.d 
 |-  D = ( Scalar ` W )
2 lfl0f.o 
 |-  .0. = ( 0g ` D )
3 lfl0f.v 
 |-  V = ( Base ` W )
4 lfl0f.f 
 |-  F = ( LFnl ` W )
5 2 fvexi 
 |-  .0. e. _V
6 5 fconst 
 |-  ( V X. { .0. } ) : V --> { .0. }
7 eqid 
 |-  ( Base ` D ) = ( Base ` D )
8 1 7 2 lmod0cl 
 |-  ( W e. LMod -> .0. e. ( Base ` D ) )
9 8 snssd 
 |-  ( W e. LMod -> { .0. } C_ ( Base ` D ) )
10 fss 
 |-  ( ( ( V X. { .0. } ) : V --> { .0. } /\ { .0. } C_ ( Base ` D ) ) -> ( V X. { .0. } ) : V --> ( Base ` D ) )
11 6 9 10 sylancr 
 |-  ( W e. LMod -> ( V X. { .0. } ) : V --> ( Base ` D ) )
12 1 lmodring 
 |-  ( W e. LMod -> D e. Ring )
13 12 ad2antrr 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> D e. Ring )
14 simplrl 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> r e. ( Base ` D ) )
15 eqid 
 |-  ( .r ` D ) = ( .r ` D )
16 7 15 2 ringrz 
 |-  ( ( D e. Ring /\ r e. ( Base ` D ) ) -> ( r ( .r ` D ) .0. ) = .0. )
17 13 14 16 syl2anc 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( r ( .r ` D ) .0. ) = .0. )
18 17 oveq1d 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( r ( .r ` D ) .0. ) ( +g ` D ) .0. ) = ( .0. ( +g ` D ) .0. ) )
19 ringgrp 
 |-  ( D e. Ring -> D e. Grp )
20 13 19 syl 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> D e. Grp )
21 7 2 grpidcl 
 |-  ( D e. Grp -> .0. e. ( Base ` D ) )
22 eqid 
 |-  ( +g ` D ) = ( +g ` D )
23 7 22 2 grplid 
 |-  ( ( D e. Grp /\ .0. e. ( Base ` D ) ) -> ( .0. ( +g ` D ) .0. ) = .0. )
24 20 21 23 syl2anc2 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( .0. ( +g ` D ) .0. ) = .0. )
25 18 24 eqtrd 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( r ( .r ` D ) .0. ) ( +g ` D ) .0. ) = .0. )
26 simplrr 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> x e. V )
27 5 fvconst2 
 |-  ( x e. V -> ( ( V X. { .0. } ) ` x ) = .0. )
28 26 27 syl 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( V X. { .0. } ) ` x ) = .0. )
29 28 oveq2d 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) = ( r ( .r ` D ) .0. ) )
30 5 fvconst2 
 |-  ( y e. V -> ( ( V X. { .0. } ) ` y ) = .0. )
31 30 adantl 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( V X. { .0. } ) ` y ) = .0. )
32 29 31 oveq12d 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) = ( ( r ( .r ` D ) .0. ) ( +g ` D ) .0. ) )
33 simpll 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> W e. LMod )
34 eqid 
 |-  ( .s ` W ) = ( .s ` W )
35 3 1 34 7 lmodvscl 
 |-  ( ( W e. LMod /\ r e. ( Base ` D ) /\ x e. V ) -> ( r ( .s ` W ) x ) e. V )
36 33 14 26 35 syl3anc 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( r ( .s ` W ) x ) e. V )
37 simpr 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> y e. V )
38 eqid 
 |-  ( +g ` W ) = ( +g ` W )
39 3 38 lmodvacl 
 |-  ( ( W e. LMod /\ ( r ( .s ` W ) x ) e. V /\ y e. V ) -> ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V )
40 33 36 37 39 syl3anc 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V )
41 5 fvconst2 
 |-  ( ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V -> ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = .0. )
42 40 41 syl 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = .0. )
43 25 32 42 3eqtr4rd 
 |-  ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) )
44 43 ralrimiva 
 |-  ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) -> A. y e. V ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) )
45 44 ralrimivva 
 |-  ( W e. LMod -> A. r e. ( Base ` D ) A. x e. V A. y e. V ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) )
46 3 38 1 34 7 22 15 4 islfl 
 |-  ( W e. LMod -> ( ( V X. { .0. } ) e. F <-> ( ( V X. { .0. } ) : V --> ( Base ` D ) /\ A. r e. ( Base ` D ) A. x e. V A. y e. V ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) ) ) )
47 11 45 46 mpbir2and 
 |-  ( W e. LMod -> ( V X. { .0. } ) e. F )