Step | Hyp | Ref
| Expression |
1 | | nonconne 2947 |
. 2
β’ Β¬
(π = π β§ π β π) |
2 | | dochexmidlem1.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
3 | | dochexmidlem1.u |
. . . . . . 7
β’ π = ((DVecHβπΎ)βπ) |
4 | | dochexmidlem1.k |
. . . . . . 7
β’ (π β (πΎ β HL β§ π β π»)) |
5 | 2, 3, 4 | dvhlmod 40520 |
. . . . . 6
β’ (π β π β LMod) |
6 | | dochexmidlem1.x |
. . . . . 6
β’ (π β π β π) |
7 | | dochexmidlem1.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
8 | | dochexmidlem1.s |
. . . . . . . . 9
β’ π = (LSubSpβπ) |
9 | 7, 8 | lssss 20809 |
. . . . . . . 8
β’ (π β π β π β π) |
10 | 6, 9 | syl 17 |
. . . . . . 7
β’ (π β π β π) |
11 | | dochexmidlem1.o |
. . . . . . . 8
β’ β₯ =
((ocHβπΎ)βπ) |
12 | 2, 3, 7, 8, 11 | dochlss 40764 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β π) |
13 | 4, 10, 12 | syl2anc 583 |
. . . . . 6
β’ (π β ( β₯ βπ) β π) |
14 | | dochexmidlem1.p |
. . . . . . 7
β’ β =
(LSSumβπ) |
15 | 8, 14 | lsmcl 20957 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ ( β₯ βπ) β π) β (π β ( β₯
βπ)) β π) |
16 | 5, 6, 13, 15 | syl3anc 1369 |
. . . . 5
β’ (π β (π β ( β₯
βπ)) β π) |
17 | 7, 8 | lssss 20809 |
. . . . 5
β’ ((π β ( β₯
βπ)) β π β (π β ( β₯
βπ)) β π) |
18 | 16, 17 | syl 17 |
. . . 4
β’ (π β (π β ( β₯
βπ)) β π) |
19 | | dochexmidlem1.a |
. . . . . . 7
β’ π΄ = (LSAtomsβπ) |
20 | 5 | adantr 480 |
. . . . . . 7
β’ ((π β§ ((π β ( β₯
βπ)) β π β§ (π β ( β₯
βπ)) β π)) β π β LMod) |
21 | 16 | adantr 480 |
. . . . . . 7
β’ ((π β§ ((π β ( β₯
βπ)) β π β§ (π β ( β₯
βπ)) β π)) β (π β ( β₯
βπ)) β π) |
22 | 7, 8 | lss1 20811 |
. . . . . . . . 9
β’ (π β LMod β π β π) |
23 | 5, 22 | syl 17 |
. . . . . . . 8
β’ (π β π β π) |
24 | 23 | adantr 480 |
. . . . . . 7
β’ ((π β§ ((π β ( β₯
βπ)) β π β§ (π β ( β₯
βπ)) β π)) β π β π) |
25 | | df-pss 3963 |
. . . . . . . . 9
β’ ((π β ( β₯
βπ)) β π β ((π β ( β₯
βπ)) β π β§ (π β ( β₯
βπ)) β π)) |
26 | 25 | biimpri 227 |
. . . . . . . 8
β’ (((π β ( β₯
βπ)) β π β§ (π β ( β₯
βπ)) β π) β (π β ( β₯
βπ)) β π) |
27 | 26 | adantl 481 |
. . . . . . 7
β’ ((π β§ ((π β ( β₯
βπ)) β π β§ (π β ( β₯
βπ)) β π)) β (π β ( β₯
βπ)) β π) |
28 | 8, 19, 20, 21, 24, 27 | lpssat 38422 |
. . . . . 6
β’ ((π β§ ((π β ( β₯
βπ)) β π β§ (π β ( β₯
βπ)) β π)) β βπ β π΄ (π β π β§ Β¬ π β (π β ( β₯
βπ)))) |
29 | 28 | ex 412 |
. . . . 5
β’ (π β (((π β ( β₯
βπ)) β π β§ (π β ( β₯
βπ)) β π) β βπ β π΄ (π β π β§ Β¬ π β (π β ( β₯
βπ))))) |
30 | | dochexmidlem1.n |
. . . . . . . . 9
β’ π = (LSpanβπ) |
31 | 4 | 3ad2ant1 1131 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ Β¬ π β (π β ( β₯
βπ))) β (πΎ β HL β§ π β π»)) |
32 | 6 | 3ad2ant1 1131 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ Β¬ π β (π β ( β₯
βπ))) β π β π) |
33 | | simp2 1135 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ Β¬ π β (π β ( β₯
βπ))) β π β π΄) |
34 | | dochexmidlem8.z |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
35 | | eqid 2727 |
. . . . . . . . 9
β’ (π β π) = (π β π) |
36 | | dochexmidlem8.xn |
. . . . . . . . . 10
β’ (π β π β { 0 }) |
37 | 36 | 3ad2ant1 1131 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ Β¬ π β (π β ( β₯
βπ))) β π β { 0 }) |
38 | | dochexmidlem8.c |
. . . . . . . . . 10
β’ (π β ( β₯ β( β₯
βπ)) = π) |
39 | 38 | 3ad2ant1 1131 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ Β¬ π β (π β ( β₯
βπ))) β ( β₯
β( β₯ βπ)) = π) |
40 | | simp3 1136 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ Β¬ π β (π β ( β₯
βπ))) β Β¬
π β (π β ( β₯
βπ))) |
41 | 2, 11, 3, 7, 8, 30,
14, 19, 31, 32, 33, 34, 35, 37, 39, 40 | dochexmidlem6 40875 |
. . . . . . . 8
β’ ((π β§ π β π΄ β§ Β¬ π β (π β ( β₯
βπ))) β (π β π) = π) |
42 | 2, 11, 3, 7, 8, 30,
14, 19, 31, 32, 33, 34, 35, 37, 39, 40 | dochexmidlem7 40876 |
. . . . . . . 8
β’ ((π β§ π β π΄ β§ Β¬ π β (π β ( β₯
βπ))) β (π β π) β π) |
43 | 41, 42 | pm2.21ddne 3021 |
. . . . . . 7
β’ ((π β§ π β π΄ β§ Β¬ π β (π β ( β₯
βπ))) β (π = π β§ π β π)) |
44 | 43 | 3adant3l 1178 |
. . . . . 6
β’ ((π β§ π β π΄ β§ (π β π β§ Β¬ π β (π β ( β₯
βπ)))) β (π = π β§ π β π)) |
45 | 44 | rexlimdv3a 3154 |
. . . . 5
β’ (π β (βπ β π΄ (π β π β§ Β¬ π β (π β ( β₯
βπ))) β (π = π β§ π β π))) |
46 | 29, 45 | syld 47 |
. . . 4
β’ (π β (((π β ( β₯
βπ)) β π β§ (π β ( β₯
βπ)) β π) β (π = π β§ π β π))) |
47 | 18, 46 | mpand 694 |
. . 3
β’ (π β ((π β ( β₯
βπ)) β π β (π = π β§ π β π))) |
48 | 47 | necon1bd 2953 |
. 2
β’ (π β (Β¬ (π = π β§ π β π) β (π β ( β₯
βπ)) = π)) |
49 | 1, 48 | mpi 20 |
1
β’ (π β (π β ( β₯
βπ)) = π) |