Metamath Proof Explorer

Theorem lkr0f

Description: The kernel of the zero functional is the set of all vectors. (Contributed by NM, 17-Apr-2014)

Ref Expression
Hypotheses lkr0f.d 
|- D = ( Scalar ` W )
lkr0f.o 
|- .0. = ( 0g ` D )
lkr0f.v 
|- V = ( Base ` W )
lkr0f.f 
|- F = ( LFnl ` W )
lkr0f.k 
|- K = ( LKer ` W )
Assertion lkr0f 
|- ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V <-> G = ( V X. { .0. } ) ) )

Proof

Step Hyp Ref Expression
1 lkr0f.d 
 |-  D = ( Scalar ` W )
2 lkr0f.o 
 |-  .0. = ( 0g ` D )
3 lkr0f.v 
 |-  V = ( Base ` W )
4 lkr0f.f 
 |-  F = ( LFnl ` W )
5 lkr0f.k 
 |-  K = ( LKer ` W )
6 eqid 
 |-  ( Base ` D ) = ( Base ` D )
7 1 6 3 4 lflf 
 |-  ( ( W e. LMod /\ G e. F ) -> G : V --> ( Base ` D ) )
8 7 ffnd 
 |-  ( ( W e. LMod /\ G e. F ) -> G Fn V )
9 8 adantr 
 |-  ( ( ( W e. LMod /\ G e. F ) /\ ( K ` G ) = V ) -> G Fn V )
10 1 2 4 5 lkrval 
 |-  ( ( W e. LMod /\ G e. F ) -> ( K ` G ) = ( `' G " { .0. } ) )
11 10 eqeq1d 
 |-  ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V <-> ( `' G " { .0. } ) = V ) )
12 11 biimpa 
 |-  ( ( ( W e. LMod /\ G e. F ) /\ ( K ` G ) = V ) -> ( `' G " { .0. } ) = V )
13 2 fvexi 
 |-  .0. e. _V
14 13 fconst2 
 |-  ( G : V --> { .0. } <-> G = ( V X. { .0. } ) )
15 fconst4 
 |-  ( G : V --> { .0. } <-> ( G Fn V /\ ( `' G " { .0. } ) = V ) )
16 14 15 bitr3i 
 |-  ( G = ( V X. { .0. } ) <-> ( G Fn V /\ ( `' G " { .0. } ) = V ) )
17 9 12 16 sylanbrc 
 |-  ( ( ( W e. LMod /\ G e. F ) /\ ( K ` G ) = V ) -> G = ( V X. { .0. } ) )
18 17 ex 
 |-  ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V -> G = ( V X. { .0. } ) ) )
19 16 biimpi 
 |-  ( G = ( V X. { .0. } ) -> ( G Fn V /\ ( `' G " { .0. } ) = V ) )
20 19 adantl 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> ( G Fn V /\ ( `' G " { .0. } ) = V ) )
21 simpr 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> G = ( V X. { .0. } ) )
22 eqid 
 |-  ( LFnl ` W ) = ( LFnl ` W )
23 1 2 3 22 lfl0f 
 |-  ( W e. LMod -> ( V X. { .0. } ) e. ( LFnl ` W ) )
24 23 adantr 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> ( V X. { .0. } ) e. ( LFnl ` W ) )
25 21 24 eqeltrd 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> G e. ( LFnl ` W ) )
26 1 2 22 5 lkrval 
 |-  ( ( W e. LMod /\ G e. ( LFnl ` W ) ) -> ( K ` G ) = ( `' G " { .0. } ) )
27 25 26 syldan 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> ( K ` G ) = ( `' G " { .0. } ) )
28 27 eqeq1d 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> ( ( K ` G ) = V <-> ( `' G " { .0. } ) = V ) )
29 ffn 
 |-  ( G : V --> { .0. } -> G Fn V )
30 14 29 sylbir 
 |-  ( G = ( V X. { .0. } ) -> G Fn V )
31 30 adantl 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> G Fn V )
32 31 biantrurd 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> ( ( `' G " { .0. } ) = V <-> ( G Fn V /\ ( `' G " { .0. } ) = V ) ) )
33 28 32 bitrd 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> ( ( K ` G ) = V <-> ( G Fn V /\ ( `' G " { .0. } ) = V ) ) )
34 20 33 mpbird 
 |-  ( ( W e. LMod /\ G = ( V X. { .0. } ) ) -> ( K ` G ) = V )
35 34 ex 
 |-  ( W e. LMod -> ( G = ( V X. { .0. } ) -> ( K ` G ) = V ) )
36 35 adantr 
 |-  ( ( W e. LMod /\ G e. F ) -> ( G = ( V X. { .0. } ) -> ( K ` G ) = V ) )
37 18 36 impbid 
 |-  ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V <-> G = ( V X. { .0. } ) ) )