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 )