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

Metamath Proof Explorer

Theorem ldualkrsc

Description: The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 28-Dec-2014)

Ref Expression
Hypotheses ldualkrsc.r 
|- R = ( Scalar ` W )
ldualkrsc.k 
|- K = ( Base ` R )
ldualkrsc.o 
|- .0. = ( 0g ` R )
ldualkrsc.f 
|- F = ( LFnl ` W )
ldualkrsc.l 
|- L = ( LKer ` W )
ldualkrsc.d 
|- D = ( LDual ` W )
ldualkrsc.s 
|- .x. = ( .s ` D )
ldualkrsc.w 
|- ( ph -> W e. LVec )
ldualkrsc.g 
|- ( ph -> G e. F )
ldualkrsc.x 
|- ( ph -> X e. K )
ldualkrsc.e 
|- ( ph -> X =/= .0. )
Assertion ldualkrsc 
|- ( ph -> ( L ` ( X .x. G ) ) = ( L ` G ) )

Proof

Step Hyp Ref Expression
1 ldualkrsc.r 
 |-  R = ( Scalar ` W )
2 ldualkrsc.k 
 |-  K = ( Base ` R )
3 ldualkrsc.o 
 |-  .0. = ( 0g ` R )
4 ldualkrsc.f 
 |-  F = ( LFnl ` W )
5 ldualkrsc.l 
 |-  L = ( LKer ` W )
6 ldualkrsc.d 
 |-  D = ( LDual ` W )
7 ldualkrsc.s 
 |-  .x. = ( .s ` D )
8 ldualkrsc.w 
 |-  ( ph -> W e. LVec )
9 ldualkrsc.g 
 |-  ( ph -> G e. F )
10 ldualkrsc.x 
 |-  ( ph -> X e. K )
11 ldualkrsc.e 
 |-  ( ph -> X =/= .0. )
12 eqid 
 |-  ( Base ` W ) = ( Base ` W )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 4 12 1 2 13 6 7 8 10 9 ldualvs 
 |-  ( ph -> ( X .x. G ) = ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) )
15 14 fveq2d 
 |-  ( ph -> ( L ` ( X .x. G ) ) = ( L ` ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) ) )
16 12 1 2 13 4 5 8 9 10 3 11 lkrsc 
 |-  ( ph -> ( L ` ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) ) = ( L ` G ) )
17 15 16 eqtrd 
 |-  ( ph -> ( L ` ( X .x. G ) ) = ( L ` G ) )