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