Metamath Proof Explorer

Theorem lkrscss

Description: The kernel of a scalar product of a functional includes the kernel of the functional. (The inclusion is proper for the zero product and equality otherwise.) (Contributed by NM, 9-Oct-2014)

Ref Expression
Hypotheses lkrsc.v 
|- V = ( Base ` W )
lkrsc.d 
|- D = ( Scalar ` W )
lkrsc.k 
|- K = ( Base ` D )
lkrsc.t 
|- .x. = ( .r ` D )
lkrsc.f 
|- F = ( LFnl ` W )
lkrsc.l 
|- L = ( LKer ` W )
lkrsc.w 
|- ( ph -> W e. LVec )
lkrsc.g 
|- ( ph -> G e. F )
lkrsc.r 
|- ( ph -> R e. K )
Assertion lkrscss 
|- ( ph -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { R } ) ) ) )

Proof

Step Hyp Ref Expression
1 lkrsc.v 
 |-  V = ( Base ` W )
2 lkrsc.d 
 |-  D = ( Scalar ` W )
3 lkrsc.k 
 |-  K = ( Base ` D )
4 lkrsc.t 
 |-  .x. = ( .r ` D )
5 lkrsc.f 
 |-  F = ( LFnl ` W )
6 lkrsc.l 
 |-  L = ( LKer ` W )
7 lkrsc.w 
 |-  ( ph -> W e. LVec )
8 lkrsc.g 
 |-  ( ph -> G e. F )
9 lkrsc.r 
 |-  ( ph -> R e. K )
10 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
11 7 10 syl 
 |-  ( ph -> W e. LMod )
12 1 5 6 11 8 lkrssv 
 |-  ( ph -> ( L ` G ) C_ V )
13 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
14 1 2 5 3 4 13 11 8 lfl0sc 
 |-  ( ph -> ( G oF .x. ( V X. { ( 0g ` D ) } ) ) = ( V X. { ( 0g ` D ) } ) )
15 14 fveq2d 
 |-  ( ph -> ( L ` ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) = ( L ` ( V X. { ( 0g ` D ) } ) ) )
16 eqid 
 |-  ( V X. { ( 0g ` D ) } ) = ( V X. { ( 0g ` D ) } )
17 2 13 1 5 lfl0f 
 |-  ( W e. LMod -> ( V X. { ( 0g ` D ) } ) e. F )
18 2 13 1 5 6 lkr0f 
 |-  ( ( W e. LMod /\ ( V X. { ( 0g ` D ) } ) e. F ) -> ( ( L ` ( V X. { ( 0g ` D ) } ) ) = V <-> ( V X. { ( 0g ` D ) } ) = ( V X. { ( 0g ` D ) } ) ) )
19 11 17 18 syl2anc2 
 |-  ( ph -> ( ( L ` ( V X. { ( 0g ` D ) } ) ) = V <-> ( V X. { ( 0g ` D ) } ) = ( V X. { ( 0g ` D ) } ) ) )
20 16 19 mpbiri 
 |-  ( ph -> ( L ` ( V X. { ( 0g ` D ) } ) ) = V )
21 15 20 eqtr2d 
 |-  ( ph -> V = ( L ` ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) )
22 12 21 sseqtrd 
 |-  ( ph -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) )
23 22 adantr 
 |-  ( ( ph /\ R = ( 0g ` D ) ) -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) )
24 sneq 
 |-  ( R = ( 0g ` D ) -> { R } = { ( 0g ` D ) } )
25 24 xpeq2d 
 |-  ( R = ( 0g ` D ) -> ( V X. { R } ) = ( V X. { ( 0g ` D ) } ) )
26 25 oveq2d 
 |-  ( R = ( 0g ` D ) -> ( G oF .x. ( V X. { R } ) ) = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) )
27 26 fveq2d 
 |-  ( R = ( 0g ` D ) -> ( L ` ( G oF .x. ( V X. { R } ) ) ) = ( L ` ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) )
28 27 adantl 
 |-  ( ( ph /\ R = ( 0g ` D ) ) -> ( L ` ( G oF .x. ( V X. { R } ) ) ) = ( L ` ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) )
29 23 28 sseqtrrd 
 |-  ( ( ph /\ R = ( 0g ` D ) ) -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { R } ) ) ) )
30 7 adantr 
 |-  ( ( ph /\ R =/= ( 0g ` D ) ) -> W e. LVec )
31 8 adantr 
 |-  ( ( ph /\ R =/= ( 0g ` D ) ) -> G e. F )
32 9 adantr 
 |-  ( ( ph /\ R =/= ( 0g ` D ) ) -> R e. K )
33 simpr 
 |-  ( ( ph /\ R =/= ( 0g ` D ) ) -> R =/= ( 0g ` D ) )
34 1 2 3 4 5 6 30 31 32 13 33 lkrsc 
 |-  ( ( ph /\ R =/= ( 0g ` D ) ) -> ( L ` ( G oF .x. ( V X. { R } ) ) ) = ( L ` G ) )
35 eqimss2 
 |-  ( ( L ` ( G oF .x. ( V X. { R } ) ) ) = ( L ` G ) -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { R } ) ) ) )
36 34 35 syl 
 |-  ( ( ph /\ R =/= ( 0g ` D ) ) -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { R } ) ) ) )
37 29 36 pm2.61dane 
 |-  ( ph -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { R } ) ) ) )