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 syl5bb
 |-  ( 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. ) ) )