Metamath Proof Explorer

Theorem lkrpssN

Description: Proper subset relation between kernels. (Contributed by NM, 16-Feb-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lkrpss.f 
|- F = ( LFnl ` W )
lkrpss.k 
|- K = ( LKer ` W )
lkrpss.d 
|- D = ( LDual ` W )
lkrpss.o 
|- .0. = ( 0g ` D )
lkrpss.w 
|- ( ph -> W e. LVec )
lkrpss.g 
|- ( ph -> G e. F )
lkrpss.h 
|- ( ph -> H e. F )
Assertion lkrpssN 
|- ( ph -> ( ( K ` G ) C. ( K ` H ) <-> ( G =/= .0. /\ H = .0. ) ) )

Proof

Step Hyp Ref Expression
1 lkrpss.f 
 |-  F = ( LFnl ` W )
2 lkrpss.k 
 |-  K = ( LKer ` W )
3 lkrpss.d 
 |-  D = ( LDual ` W )
4 lkrpss.o 
 |-  .0. = ( 0g ` D )
5 lkrpss.w 
 |-  ( ph -> W e. LVec )
6 lkrpss.g 
 |-  ( ph -> G e. F )
7 lkrpss.h 
 |-  ( ph -> H e. F )
8 df-pss 
 |-  ( ( K ` G ) C. ( K ` H ) <-> ( ( K ` G ) C_ ( K ` H ) /\ ( K ` G ) =/= ( K ` H ) ) )
9 simpr 
 |-  ( ( ph /\ ( K ` G ) C. ( K ` H ) ) -> ( K ` G ) C. ( K ` H ) )
10 eqid 
 |-  ( Base ` W ) = ( Base ` W )
11 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
12 5 11 syl 
 |-  ( ph -> W e. LMod )
13 10 1 2 12 7 lkrssv 
 |-  ( ph -> ( K ` H ) C_ ( Base ` W ) )
14 13 adantr 
 |-  ( ( ph /\ ( K ` G ) C. ( K ` H ) ) -> ( K ` H ) C_ ( Base ` W ) )
15 9 14 psssstrd 
 |-  ( ( ph /\ ( K ` G ) C. ( K ` H ) ) -> ( K ` G ) C. ( Base ` W ) )
16 15 pssned 
 |-  ( ( ph /\ ( K ` G ) C. ( K ` H ) ) -> ( K ` G ) =/= ( Base ` W ) )
17 8 16 sylan2br 
 |-  ( ( ph /\ ( ( K ` G ) C_ ( K ` H ) /\ ( K ` G ) =/= ( K ` H ) ) ) -> ( K ` G ) =/= ( Base ` W ) )
18 simplr 
 |-  ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) -> ( K ` G ) C_ ( K ` H ) )
19 eqid 
 |-  ( LSHyp ` W ) = ( LSHyp ` W )
20 5 ad2antrr 
 |-  ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) -> W e. LVec )
21 simpr 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) e. ( LSHyp ` W ) ) -> ( K ` G ) e. ( LSHyp ` W ) )
22 simplr 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> ( K ` H ) e. ( LSHyp ` W ) )
23 13 ad3antrrr 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> ( K ` H ) C_ ( Base ` W ) )
24 simpr 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> ( K ` G ) = ( Base ` W ) )
25 simpllr 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> ( K ` G ) C_ ( K ` H ) )
26 24 25 eqsstrrd 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> ( Base ` W ) C_ ( K ` H ) )
27 23 26 eqssd 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> ( K ` H ) = ( Base ` W ) )
28 10 19 1 2 5 7 lkrshp4 
 |-  ( ph -> ( ( K ` H ) =/= ( Base ` W ) <-> ( K ` H ) e. ( LSHyp ` W ) ) )
29 28 ad3antrrr 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> ( ( K ` H ) =/= ( Base ` W ) <-> ( K ` H ) e. ( LSHyp ` W ) ) )
30 29 necon1bbid 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> ( -. ( K ` H ) e. ( LSHyp ` W ) <-> ( K ` H ) = ( Base ` W ) ) )
31 27 30 mpbird 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> -. ( K ` H ) e. ( LSHyp ` W ) )
32 22 31 pm2.21dd 
 |-  ( ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) /\ ( K ` G ) = ( Base ` W ) ) -> ( K ` G ) e. ( LSHyp ` W ) )
33 10 19 1 2 5 6 lkrshpor 
 |-  ( ph -> ( ( K ` G ) e. ( LSHyp ` W ) \/ ( K ` G ) = ( Base ` W ) ) )
34 33 ad2antrr 
 |-  ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) -> ( ( K ` G ) e. ( LSHyp ` W ) \/ ( K ` G ) = ( Base ` W ) ) )
35 21 32 34 mpjaodan 
 |-  ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) -> ( K ` G ) e. ( LSHyp ` W ) )
36 simpr 
 |-  ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) -> ( K ` H ) e. ( LSHyp ` W ) )
37 19 20 35 36 lshpcmp 
 |-  ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) -> ( ( K ` G ) C_ ( K ` H ) <-> ( K ` G ) = ( K ` H ) ) )
38 18 37 mpbid 
 |-  ( ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) /\ ( K ` H ) e. ( LSHyp ` W ) ) -> ( K ` G ) = ( K ` H ) )
39 38 ex 
 |-  ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) -> ( ( K ` H ) e. ( LSHyp ` W ) -> ( K ` G ) = ( K ` H ) ) )
40 39 necon3ad 
 |-  ( ( ph /\ ( K ` G ) C_ ( K ` H ) ) -> ( ( K ` G ) =/= ( K ` H ) -> -. ( K ` H ) e. ( LSHyp ` W ) ) )
41 40 impr 
 |-  ( ( ph /\ ( ( K ` G ) C_ ( K ` H ) /\ ( K ` G ) =/= ( K ` H ) ) ) -> -. ( K ` H ) e. ( LSHyp ` W ) )
42 28 necon1bbid 
 |-  ( ph -> ( -. ( K ` H ) e. ( LSHyp ` W ) <-> ( K ` H ) = ( Base ` W ) ) )
43 42 adantr 
 |-  ( ( ph /\ ( ( K ` G ) C_ ( K ` H ) /\ ( K ` G ) =/= ( K ` H ) ) ) -> ( -. ( K ` H ) e. ( LSHyp ` W ) <-> ( K ` H ) = ( Base ` W ) ) )
44 41 43 mpbid 
 |-  ( ( ph /\ ( ( K ` G ) C_ ( K ` H ) /\ ( K ` G ) =/= ( K ` H ) ) ) -> ( K ` H ) = ( Base ` W ) )
45 17 44 jca 
 |-  ( ( ph /\ ( ( K ` G ) C_ ( K ` H ) /\ ( K ` G ) =/= ( K ` H ) ) ) -> ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) )
46 10 1 2 12 6 lkrssv 
 |-  ( ph -> ( K ` G ) C_ ( Base ` W ) )
47 46 adantr 
 |-  ( ( ph /\ ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) ) -> ( K ` G ) C_ ( Base ` W ) )
48 simprr 
 |-  ( ( ph /\ ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) ) -> ( K ` H ) = ( Base ` W ) )
49 48 eqcomd 
 |-  ( ( ph /\ ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) ) -> ( Base ` W ) = ( K ` H ) )
50 47 49 sseqtrd 
 |-  ( ( ph /\ ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) ) -> ( K ` G ) C_ ( K ` H ) )
51 simprl 
 |-  ( ( ph /\ ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) ) -> ( K ` G ) =/= ( Base ` W ) )
52 51 49 neeqtrd 
 |-  ( ( ph /\ ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) ) -> ( K ` G ) =/= ( K ` H ) )
53 50 52 jca 
 |-  ( ( ph /\ ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) ) -> ( ( K ` G ) C_ ( K ` H ) /\ ( K ` G ) =/= ( K ` H ) ) )
54 45 53 impbida 
 |-  ( ph -> ( ( ( K ` G ) C_ ( K ` H ) /\ ( K ` G ) =/= ( K ` H ) ) <-> ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) ) )
55 8 54 bitrid 
 |-  ( ph -> ( ( K ` G ) C. ( K ` H ) <-> ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) ) )
56 10 1 2 3 4 12 6 lkr0f2 
 |-  ( ph -> ( ( K ` G ) = ( Base ` W ) <-> G = .0. ) )
57 56 necon3bid 
 |-  ( ph -> ( ( K ` G ) =/= ( Base ` W ) <-> G =/= .0. ) )
58 10 1 2 3 4 12 7 lkr0f2 
 |-  ( ph -> ( ( K ` H ) = ( Base ` W ) <-> H = .0. ) )
59 57 58 anbi12d 
 |-  ( ph -> ( ( ( K ` G ) =/= ( Base ` W ) /\ ( K ` H ) = ( Base ` W ) ) <-> ( G =/= .0. /\ H = .0. ) ) )
60 55 59 bitrd 
 |-  ( ph -> ( ( K ` G ) C. ( K ` H ) <-> ( G =/= .0. /\ H = .0. ) ) )