| 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 |
|
elex |
|- ( W e. X -> W e. _V ) |
| 6 |
|
fveq2 |
|- ( w = W -> ( LFnl ` w ) = ( LFnl ` W ) ) |
| 7 |
6 3
|
eqtr4di |
|- ( w = W -> ( LFnl ` w ) = F ) |
| 8 |
|
fveq2 |
|- ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) ) |
| 9 |
8 1
|
eqtr4di |
|- ( w = W -> ( Scalar ` w ) = D ) |
| 10 |
9
|
fveq2d |
|- ( w = W -> ( 0g ` ( Scalar ` w ) ) = ( 0g ` D ) ) |
| 11 |
10 2
|
eqtr4di |
|- ( w = W -> ( 0g ` ( Scalar ` w ) ) = .0. ) |
| 12 |
11
|
sneqd |
|- ( w = W -> { ( 0g ` ( Scalar ` w ) ) } = { .0. } ) |
| 13 |
12
|
imaeq2d |
|- ( w = W -> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) = ( `' f " { .0. } ) ) |
| 14 |
7 13
|
mpteq12dv |
|- ( w = W -> ( f e. ( LFnl ` w ) |-> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) ) = ( f e. F |-> ( `' f " { .0. } ) ) ) |
| 15 |
|
df-lkr |
|- LKer = ( w e. _V |-> ( f e. ( LFnl ` w ) |-> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) ) ) |
| 16 |
14 15 3
|
mptfvmpt |
|- ( W e. _V -> ( LKer ` W ) = ( f e. F |-> ( `' f " { .0. } ) ) ) |
| 17 |
4 16
|
eqtrid |
|- ( W e. _V -> K = ( f e. F |-> ( `' f " { .0. } ) ) ) |
| 18 |
5 17
|
syl |
|- ( W e. X -> K = ( f e. F |-> ( `' f " { .0. } ) ) ) |