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