Step | Hyp | Ref
| Expression |
1 | | dihglblem6.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | dihglblem6.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | eqid 2737 |
. . . 4
β’
(meetβπΎ) =
(meetβπΎ) |
4 | | dihglblem6.g |
. . . 4
β’ πΊ = (glbβπΎ) |
5 | | dihglblem6.h |
. . . 4
β’ π» = (LHypβπΎ) |
6 | | eqid 2737 |
. . . 4
β’ {π’ β π΅ β£ βπ£ β π π’ = (π£(meetβπΎ)π)} = {π’ β π΅ β£ βπ£ β π π’ = (π£(meetβπΎ)π)} |
7 | | eqid 2737 |
. . . 4
β’
((DIsoBβπΎ)βπ) = ((DIsoBβπΎ)βπ) |
8 | | dihglblem6.i |
. . . 4
β’ πΌ = ((DIsoHβπΎ)βπ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | dihglblem4 39789 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) |
10 | | fal 1556 |
. . . . 5
β’ Β¬
β₯ |
11 | | dihglblem6.s |
. . . . . . . 8
β’ π = (LSubSpβπ) |
12 | | dihglblem6.d |
. . . . . . . 8
β’ π· = (LSAtomsβπ) |
13 | | dihglblem6.u |
. . . . . . . . 9
β’ π = ((DVecHβπΎ)βπ) |
14 | | simpll 766 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β (πΎ β HL β§ π β π»)) |
15 | 5, 13, 14 | dvhlmod 39602 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β π β LMod) |
16 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β πΎ β HL) |
17 | | hlclat 37849 |
. . . . . . . . . . 11
β’ (πΎ β HL β πΎ β CLat) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β πΎ β CLat) |
19 | | simplrl 776 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β π β π΅) |
20 | 1, 4 | clatglbcl 18401 |
. . . . . . . . . 10
β’ ((πΎ β CLat β§ π β π΅) β (πΊβπ) β π΅) |
21 | 18, 19, 20 | syl2anc 585 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β (πΊβπ) β π΅) |
22 | 1, 5, 8, 13, 11 | dihlss 39742 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΊβπ) β π΅) β (πΌβ(πΊβπ)) β π) |
23 | 14, 21, 22 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β (πΌβ(πΊβπ)) β π) |
24 | 1, 4, 5, 13, 8, 11 | dihglblem5 39790 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β β© π₯ β π (πΌβπ₯) β π) |
25 | 24 | adantr 482 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β β©
π₯ β π (πΌβπ₯) β π) |
26 | | simpr 486 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) |
27 | 11, 12, 15, 23, 25, 26 | lpssat 37504 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) β βπ β π· (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) |
28 | 27 | ex 414 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β βπ β π· (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ))))) |
29 | | simp1l 1198 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β (πΎ β HL β§ π β π»)) |
30 | 5, 13, 8, 12 | dih1dimat 39822 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ π β π·) β π β ran πΌ) |
31 | 30 | adantlr 714 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β π β ran πΌ) |
32 | 31 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β π β ran πΌ) |
33 | 5, 8 | dihcnvid2 39765 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (πΌβ(β‘πΌβπ)) = π) |
34 | 29, 32, 33 | syl2anc 585 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β (πΌβ(β‘πΌβπ)) = π) |
35 | | simp3l 1202 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β π β β©
π₯ β π (πΌβπ₯)) |
36 | | ssiin 5020 |
. . . . . . . . . . . . 13
β’ (π β β© π₯ β π (πΌβπ₯) β βπ₯ β π π β (πΌβπ₯)) |
37 | 35, 36 | sylib 217 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β βπ₯ β π π β (πΌβπ₯)) |
38 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β§ π₯ β π) β (πΎ β HL β§ π β π»)) |
39 | | simpll 766 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β (πΎ β HL β§ π β π»)) |
40 | 1, 5, 8, 13, 11 | dihf11 39759 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β HL β§ π β π») β πΌ:π΅β1-1βπ) |
41 | | f1f1orn 6800 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΌ:π΅β1-1βπ β πΌ:π΅β1-1-ontoβran
πΌ) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β πΌ:π΅β1-1-ontoβran
πΌ) |
43 | | f1ocnvdm 7236 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ:π΅β1-1-ontoβran
πΌ β§ π β ran πΌ) β (β‘πΌβπ) β π΅) |
44 | 42, 31, 43 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β (β‘πΌβπ) β π΅) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β§ π₯ β π) β (β‘πΌβπ) β π΅) |
46 | | simplrl 776 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β π β π΅) |
47 | 46 | sselda 3949 |
. . . . . . . . . . . . . . . 16
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β§ π₯ β π) β π₯ β π΅) |
48 | 1, 2, 5, 8 | dihord 39756 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ (β‘πΌβπ) β π΅ β§ π₯ β π΅) β ((πΌβ(β‘πΌβπ)) β (πΌβπ₯) β (β‘πΌβπ) β€ π₯)) |
49 | 38, 45, 47, 48 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β§ π₯ β π) β ((πΌβ(β‘πΌβπ)) β (πΌβπ₯) β (β‘πΌβπ) β€ π₯)) |
50 | 39, 31, 33 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β (πΌβ(β‘πΌβπ)) = π) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β§ π₯ β π) β (πΌβ(β‘πΌβπ)) = π) |
52 | 51 | sseq1d 3980 |
. . . . . . . . . . . . . . 15
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β§ π₯ β π) β ((πΌβ(β‘πΌβπ)) β (πΌβπ₯) β π β (πΌβπ₯))) |
53 | 49, 52 | bitr3d 281 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β§ π₯ β π) β ((β‘πΌβπ) β€ π₯ β π β (πΌβπ₯))) |
54 | 53 | ralbidva 3173 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π·) β (βπ₯ β π (β‘πΌβπ) β€ π₯ β βπ₯ β π π β (πΌβπ₯))) |
55 | 54 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β (βπ₯ β π (β‘πΌβπ) β€ π₯ β βπ₯ β π π β (πΌβπ₯))) |
56 | 37, 55 | mpbird 257 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β βπ₯ β π (β‘πΌβπ) β€ π₯) |
57 | | simp1ll 1237 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β πΎ β HL) |
58 | 57, 17 | syl 17 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β πΎ β CLat) |
59 | 44 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β (β‘πΌβπ) β π΅) |
60 | | simp1rl 1239 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β π β π΅) |
61 | 1, 2, 4 | clatleglb 18414 |
. . . . . . . . . . . 12
β’ ((πΎ β CLat β§ (β‘πΌβπ) β π΅ β§ π β π΅) β ((β‘πΌβπ) β€ (πΊβπ) β βπ₯ β π (β‘πΌβπ) β€ π₯)) |
62 | 58, 59, 60, 61 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β ((β‘πΌβπ) β€ (πΊβπ) β βπ₯ β π (β‘πΌβπ) β€ π₯)) |
63 | 56, 62 | mpbird 257 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β (β‘πΌβπ) β€ (πΊβπ)) |
64 | 58, 60, 20 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β (πΊβπ) β π΅) |
65 | 1, 2, 5, 8 | dihord 39756 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (β‘πΌβπ) β π΅ β§ (πΊβπ) β π΅) β ((πΌβ(β‘πΌβπ)) β (πΌβ(πΊβπ)) β (β‘πΌβπ) β€ (πΊβπ))) |
66 | 29, 59, 64, 65 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β ((πΌβ(β‘πΌβπ)) β (πΌβ(πΊβπ)) β (β‘πΌβπ) β€ (πΊβπ))) |
67 | 63, 66 | mpbird 257 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β (πΌβ(β‘πΌβπ)) β (πΌβ(πΊβπ))) |
68 | 34, 67 | eqsstrrd 3988 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β π β (πΌβ(πΊβπ))) |
69 | | simp3r 1203 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β Β¬ π β (πΌβ(πΊβπ))) |
70 | 68, 69 | pm2.21fal 1564 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π β π· β§ (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ)))) β β₯) |
71 | 70 | rexlimdv3a 3157 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β (βπ β π· (π β β©
π₯ β π (πΌβπ₯) β§ Β¬ π β (πΌβ(πΊβπ))) β β₯)) |
72 | 28, 71 | syld 47 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β β₯)) |
73 | 10, 72 | mtoi 198 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β Β¬ (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) |
74 | | dfpss3 4051 |
. . . . . 6
β’ ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β§ Β¬ β© π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ)))) |
75 | 74 | notbii 320 |
. . . . 5
β’ (Β¬
(πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β Β¬ ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β§ Β¬ β© π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ)))) |
76 | | iman 403 |
. . . . 5
β’ (((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β β©
π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ))) β Β¬ ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β§ Β¬ β© π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ)))) |
77 | | anclb 547 |
. . . . 5
β’ (((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β β©
π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ))) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β§ β©
π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ))))) |
78 | 75, 76, 77 | 3bitr2i 299 |
. . . 4
β’ (Β¬
(πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β§ β©
π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ))))) |
79 | 73, 78 | sylib 217 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β§ β©
π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ))))) |
80 | 9, 79 | mpd 15 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β§ β©
π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ)))) |
81 | | eqss 3964 |
. 2
β’ ((πΌβ(πΊβπ)) = β©
π₯ β π (πΌβπ₯) β ((πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯) β§ β©
π₯ β π (πΌβπ₯) β (πΌβ(πΊβπ)))) |
82 | 80, 81 | sylibr 233 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β (πΌβ(πΊβπ)) = β©
π₯ β π (πΌβπ₯)) |