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 |
|
elex |
|- ( W e. X -> W e. _V ) |
7 |
1 2 3 4 5
|
ellkr |
|- ( ( W e. _V /\ G e. F ) -> ( x e. ( K ` G ) <-> ( x e. V /\ ( G ` x ) = .0. ) ) ) |
8 |
7
|
abbi2dv |
|- ( ( W e. _V /\ G e. F ) -> ( K ` G ) = { x | ( x e. V /\ ( G ` x ) = .0. ) } ) |
9 |
|
df-rab |
|- { x e. V | ( G ` x ) = .0. } = { x | ( x e. V /\ ( G ` x ) = .0. ) } |
10 |
8 9
|
eqtr4di |
|- ( ( W e. _V /\ G e. F ) -> ( K ` G ) = { x e. V | ( G ` x ) = .0. } ) |
11 |
6 10
|
sylan |
|- ( ( W e. X /\ G e. F ) -> ( K ` G ) = { x e. V | ( G ` x ) = .0. } ) |