Metamath Proof Explorer

Theorem lkrval

Description: Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014)

Ref Expression
Hypotheses lkrfval.d 
|- D = ( Scalar ` W )
lkrfval.o 
|- .0. = ( 0g ` D )
lkrfval.f 
|- F = ( LFnl ` W )
lkrfval.k 
|- K = ( LKer ` W )
Assertion lkrval 
|- ( ( W e. X /\ G e. F ) -> ( K ` G ) = ( `' G " { .0. } ) )

Proof

Step Hyp Ref Expression
1 lkrfval.d 
 |-  D = ( Scalar ` W )
2 lkrfval.o 
 |-  .0. = ( 0g ` D )
3 lkrfval.f 
 |-  F = ( LFnl ` W )
4 lkrfval.k 
 |-  K = ( LKer ` W )
5 1 2 3 4 lkrfval 
 |-  ( W e. X -> K = ( f e. F |-> ( `' f " { .0. } ) ) )
6 5 fveq1d 
 |-  ( W e. X -> ( K ` G ) = ( ( f e. F |-> ( `' f " { .0. } ) ) ` G ) )
7 cnvexg 
 |-  ( G e. F -> `' G e. _V )
8 imaexg 
 |-  ( `' G e. _V -> ( `' G " { .0. } ) e. _V )
9 7 8 syl 
 |-  ( G e. F -> ( `' G " { .0. } ) e. _V )
10 cnveq 
 |-  ( f = G -> `' f = `' G )
11 10 imaeq1d 
 |-  ( f = G -> ( `' f " { .0. } ) = ( `' G " { .0. } ) )
12 eqid 
 |-  ( f e. F |-> ( `' f " { .0. } ) ) = ( f e. F |-> ( `' f " { .0. } ) )
13 11 12 fvmptg 
 |-  ( ( G e. F /\ ( `' G " { .0. } ) e. _V ) -> ( ( f e. F |-> ( `' f " { .0. } ) ) ` G ) = ( `' G " { .0. } ) )
14 9 13 mpdan 
 |-  ( G e. F -> ( ( f e. F |-> ( `' f " { .0. } ) ) ` G ) = ( `' G " { .0. } ) )
15 6 14 sylan9eq 
 |-  ( ( W e. X /\ G e. F ) -> ( K ` G ) = ( `' G " { .0. } ) )