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

Metamath Proof Explorer

Theorem lkrss

Description: The kernel of a scalar product of a functional includes the kernel of the functional. (Contributed by NM, 27-Jan-2015)

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

Proof

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