Metamath Proof Explorer

Theorem lkrss2N

Description: Two functionals with kernels in a subset relationship. (Contributed by NM, 17-Feb-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lkrss2.s 
|- S = ( Scalar ` W )
lkrss2.r 
|- R = ( Base ` S )
lkrss2.f 
|- F = ( LFnl ` W )
lkrss2.k 
|- K = ( LKer ` W )
lkrss2.d 
|- D = ( LDual ` W )
lkrss2.t 
|- .x. = ( .s ` D )
lkrss2.w 
|- ( ph -> W e. LVec )
lkrss2.g 
|- ( ph -> G e. F )
lkrss2.h 
|- ( ph -> H e. F )
Assertion lkrss2N 
|- ( ph -> ( ( K ` G ) C_ ( K ` H ) <-> E. r e. R H = ( r .x. G ) ) )

Proof

Step Hyp Ref Expression
1 lkrss2.s 
 |-  S = ( Scalar ` W )
2 lkrss2.r 
 |-  R = ( Base ` S )
3 lkrss2.f 
 |-  F = ( LFnl ` W )
4 lkrss2.k 
 |-  K = ( LKer ` W )
5 lkrss2.d 
 |-  D = ( LDual ` W )
6 lkrss2.t 
 |-  .x. = ( .s ` D )
7 lkrss2.w 
 |-  ( ph -> W e. LVec )
8 lkrss2.g 
 |-  ( ph -> G e. F )
9 lkrss2.h 
 |-  ( ph -> H e. F )
10 sspss 
 |-  ( ( K ` G ) C_ ( K ` H ) <-> ( ( K ` G ) C. ( K ` H ) \/ ( K ` G ) = ( K ` H ) ) )
11 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
12 3 4 5 11 7 8 9 lkrpssN 
 |-  ( ph -> ( ( K ` G ) C. ( K ` H ) <-> ( G =/= ( 0g ` D ) /\ H = ( 0g ` D ) ) ) )
13 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
14 7 13 syl 
 |-  ( ph -> W e. LMod )
15 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
16 1 2 15 lmod0cl 
 |-  ( W e. LMod -> ( 0g ` S ) e. R )
17 14 16 syl 
 |-  ( ph -> ( 0g ` S ) e. R )
18 17 adantr 
 |-  ( ( ph /\ H = ( 0g ` D ) ) -> ( 0g ` S ) e. R )
19 simpr 
 |-  ( ( ph /\ H = ( 0g ` D ) ) -> H = ( 0g ` D ) )
20 3 1 15 5 6 11 14 8 ldual0vs 
 |-  ( ph -> ( ( 0g ` S ) .x. G ) = ( 0g ` D ) )
21 20 adantr 
 |-  ( ( ph /\ H = ( 0g ` D ) ) -> ( ( 0g ` S ) .x. G ) = ( 0g ` D ) )
22 19 21 eqtr4d 
 |-  ( ( ph /\ H = ( 0g ` D ) ) -> H = ( ( 0g ` S ) .x. G ) )
23 oveq1 
 |-  ( r = ( 0g ` S ) -> ( r .x. G ) = ( ( 0g ` S ) .x. G ) )
24 23 rspceeqv 
 |-  ( ( ( 0g ` S ) e. R /\ H = ( ( 0g ` S ) .x. G ) ) -> E. r e. R H = ( r .x. G ) )
25 18 22 24 syl2anc 
 |-  ( ( ph /\ H = ( 0g ` D ) ) -> E. r e. R H = ( r .x. G ) )
26 25 ex 
 |-  ( ph -> ( H = ( 0g ` D ) -> E. r e. R H = ( r .x. G ) ) )
27 26 adantld 
 |-  ( ph -> ( ( G =/= ( 0g ` D ) /\ H = ( 0g ` D ) ) -> E. r e. R H = ( r .x. G ) ) )
28 12 27 sylbid 
 |-  ( ph -> ( ( K ` G ) C. ( K ` H ) -> E. r e. R H = ( r .x. G ) ) )
29 28 imp 
 |-  ( ( ph /\ ( K ` G ) C. ( K ` H ) ) -> E. r e. R H = ( r .x. G ) )
30 7 adantr 
 |-  ( ( ph /\ ( K ` G ) = ( K ` H ) ) -> W e. LVec )
31 8 adantr 
 |-  ( ( ph /\ ( K ` G ) = ( K ` H ) ) -> G e. F )
32 9 adantr 
 |-  ( ( ph /\ ( K ` G ) = ( K ` H ) ) -> H e. F )
33 simpr 
 |-  ( ( ph /\ ( K ` G ) = ( K ` H ) ) -> ( K ` G ) = ( K ` H ) )
34 1 2 3 4 5 6 30 31 32 33 eqlkr4 
 |-  ( ( ph /\ ( K ` G ) = ( K ` H ) ) -> E. r e. R H = ( r .x. G ) )
35 29 34 jaodan 
 |-  ( ( ph /\ ( ( K ` G ) C. ( K ` H ) \/ ( K ` G ) = ( K ` H ) ) ) -> E. r e. R H = ( r .x. G ) )
36 10 35 sylan2b 
 |-  ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) -> E. r e. R H = ( r .x. G ) )
37 7 adantr 
 |-  ( ( ph /\ r e. R ) -> W e. LVec )
38 8 adantr 
 |-  ( ( ph /\ r e. R ) -> G e. F )
39 simpr 
 |-  ( ( ph /\ r e. R ) -> r e. R )
40 1 2 3 4 5 6 37 38 39 lkrss 
 |-  ( ( ph /\ r e. R ) -> ( K ` G ) C_ ( K ` ( r .x. G ) ) )
41 40 ex 
 |-  ( ph -> ( r e. R -> ( K ` G ) C_ ( K ` ( r .x. G ) ) ) )
42 fveq2 
 |-  ( H = ( r .x. G ) -> ( K ` H ) = ( K ` ( r .x. G ) ) )
43 42 sseq2d 
 |-  ( H = ( r .x. G ) -> ( ( K ` G ) C_ ( K ` H ) <-> ( K ` G ) C_ ( K ` ( r .x. G ) ) ) )
44 43 biimprcd 
 |-  ( ( K ` G ) C_ ( K ` ( r .x. G ) ) -> ( H = ( r .x. G ) -> ( K ` G ) C_ ( K ` H ) ) )
45 41 44 syl6 
 |-  ( ph -> ( r e. R -> ( H = ( r .x. G ) -> ( K ` G ) C_ ( K ` H ) ) ) )
46 45 rexlimdv 
 |-  ( ph -> ( E. r e. R H = ( r .x. G ) -> ( K ` G ) C_ ( K ` H ) ) )
47 46 imp 
 |-  ( ( ph /\ E. r e. R H = ( r .x. G ) ) -> ( K ` G ) C_ ( K ` H ) )
48 36 47 impbida 
 |-  ( ph -> ( ( K ` G ) C_ ( K ` H ) <-> E. r e. R H = ( r .x. G ) ) )