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