This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lkrval2

Description: Value of the kernel of a functional. (Contributed by NM, 15-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 lkrval2 
|- ( ( W e. X /\ G e. F ) -> ( 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 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 eqabdv 
 |-  ( ( 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. } )