Metamath Proof Explorer

Theorem ellkr

Description: Membership in the kernel of a functional. ( elnlfn analog.) (Contributed by NM, 16-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 lkrfval2.v 
 |-  V = ( Base ` W )
2 lkrfval2.d 
 |-  D = ( Scalar ` W )
3 lkrfval2.o 
 |-  .0. = ( 0g ` D )
4 lkrfval2.f 
 |-  F = ( LFnl ` W )
5 lkrfval2.k 
 |-  K = ( LKer ` W )
6 2 3 4 5 lkrval 
 |-  ( ( W e. Y /\ G e. F ) -> ( K ` G ) = ( `' G " { .0. } ) )
7 6 eleq2d 
 |-  ( ( W e. Y /\ G e. F ) -> ( X e. ( K ` G ) <-> X e. ( `' G " { .0. } ) ) )
8 eqid 
 |-  ( Base ` D ) = ( Base ` D )
9 2 8 1 4 lflf 
 |-  ( ( W e. Y /\ G e. F ) -> G : V --> ( Base ` D ) )
10 ffn 
 |-  ( G : V --> ( Base ` D ) -> G Fn V )
11 elpreima 
 |-  ( G Fn V -> ( X e. ( `' G " { .0. } ) <-> ( X e. V /\ ( G ` X ) e. { .0. } ) ) )
12 9 10 11 3syl 
 |-  ( ( W e. Y /\ G e. F ) -> ( X e. ( `' G " { .0. } ) <-> ( X e. V /\ ( G ` X ) e. { .0. } ) ) )
13 fvex 
 |-  ( G ` X ) e. _V
14 13 elsn 
 |-  ( ( G ` X ) e. { .0. } <-> ( G ` X ) = .0. )
15 14 anbi2i 
 |-  ( ( X e. V /\ ( G ` X ) e. { .0. } ) <-> ( X e. V /\ ( G ` X ) = .0. ) )
16 12 15 bitrdi 
 |-  ( ( W e. Y /\ G e. F ) -> ( X e. ( `' G " { .0. } ) <-> ( X e. V /\ ( G ` X ) = .0. ) ) )
17 7 16 bitrd 
 |-  ( ( W e. Y /\ G e. F ) -> ( X e. ( K ` G ) <-> ( X e. V /\ ( G ` X ) = .0. ) ) )