Step | Hyp | Ref
| Expression |
1 | | 4thatlem.ph |
. . . 4
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π
β π΄ β§ Β¬ π
β€ π β§ (π β¨ π
) = (π β¨ π
)) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) |
2 | | 4thatlem0.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | 4thatlem0.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
4 | | 4thatlem0.m |
. . . 4
β’ β§ =
(meetβπΎ) |
5 | | 4thatlem0.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
6 | | 4thatlem0.h |
. . . 4
β’ π» = (LHypβπΎ) |
7 | | 4thatlem0.u |
. . . 4
β’ π = ((π β¨ π) β§ π) |
8 | | 4thatlem0.v |
. . . 4
β’ π = ((π β¨ π) β§ π) |
9 | | 4thatlem0.c |
. . . 4
β’ πΆ = ((π β¨ π) β§ (π β¨ π)) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | 4atexlemc 38940 |
. . 3
β’ (π β πΆ β π΄) |
11 | 10 | adantr 482 |
. 2
β’ ((π β§ πΆ β π) β πΆ β π΄) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | 4atexlemnclw 38941 |
. . 3
β’ (π β Β¬ πΆ β€ π) |
13 | 12 | adantr 482 |
. 2
β’ ((π β§ πΆ β π) β Β¬ πΆ β€ π) |
14 | 1, 2, 3, 4, 5, 6, 7, 8 | 4atexlemntlpq 38939 |
. . . . 5
β’ (π β Β¬ π β€ (π β¨ π)) |
15 | | id 22 |
. . . . . . . . . . 11
β’ (πΆ = π β πΆ = π) |
16 | 9, 15 | eqtr3id 2787 |
. . . . . . . . . 10
β’ (πΆ = π β ((π β¨ π) β§ (π β¨ π)) = π) |
17 | 16 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ πΆ = π) β ((π β¨ π) β§ (π β¨ π)) = π) |
18 | 1 | 4atexlemkl 38928 |
. . . . . . . . . . . 12
β’ (π β πΎ β Lat) |
19 | 1, 3, 5 | 4atexlemqtb 38932 |
. . . . . . . . . . . 12
β’ (π β (π β¨ π) β (BaseβπΎ)) |
20 | 1, 3, 5 | 4atexlempsb 38931 |
. . . . . . . . . . . 12
β’ (π β (π β¨ π) β (BaseβπΎ)) |
21 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(BaseβπΎ) =
(BaseβπΎ) |
22 | 21, 2, 4 | latmle1 18417 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
23 | 18, 19, 20, 22 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
24 | 1 | 4atexlemk 38918 |
. . . . . . . . . . . 12
β’ (π β πΎ β HL) |
25 | 1 | 4atexlemq 38922 |
. . . . . . . . . . . 12
β’ (π β π β π΄) |
26 | 1 | 4atexlemt 38924 |
. . . . . . . . . . . 12
β’ (π β π β π΄) |
27 | 3, 5 | hlatjcom 38238 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
28 | 24, 25, 26, 27 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (π β¨ π) = (π β¨ π)) |
29 | 23, 28 | breqtrd 5175 |
. . . . . . . . . 10
β’ (π β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
30 | 29 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΆ = π) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
31 | 17, 30 | eqbrtrrd 5173 |
. . . . . . . 8
β’ ((π β§ πΆ = π) β π β€ (π β¨ π)) |
32 | 1 | 4atexlemkc 38929 |
. . . . . . . . . 10
β’ (π β πΎ β CvLat) |
33 | 1 | 4atexlemp 38921 |
. . . . . . . . . 10
β’ (π β π β π΄) |
34 | 1 | 4atexlempnq 38926 |
. . . . . . . . . 10
β’ (π β π β π) |
35 | 2, 3, 5 | cvlatexch2 38207 |
. . . . . . . . . 10
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
36 | 32, 33, 26, 25, 34, 35 | syl131anc 1384 |
. . . . . . . . 9
β’ (π β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
37 | 36 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ = π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
38 | 31, 37 | mpd 15 |
. . . . . . 7
β’ ((π β§ πΆ = π) β π β€ (π β¨ π)) |
39 | 38 | ex 414 |
. . . . . 6
β’ (π β (πΆ = π β π β€ (π β¨ π))) |
40 | 39 | necon3bd 2955 |
. . . . 5
β’ (π β (Β¬ π β€ (π β¨ π) β πΆ β π)) |
41 | 14, 40 | mpd 15 |
. . . 4
β’ (π β πΆ β π) |
42 | 41 | adantr 482 |
. . 3
β’ ((π β§ πΆ β π) β πΆ β π) |
43 | | simpr 486 |
. . 3
β’ ((π β§ πΆ β π) β πΆ β π) |
44 | 21, 2, 4 | latmle2 18418 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
45 | 18, 19, 20, 44 | syl3anc 1372 |
. . . . 5
β’ (π β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
46 | 9, 45 | eqbrtrid 5184 |
. . . 4
β’ (π β πΆ β€ (π β¨ π)) |
47 | 46 | adantr 482 |
. . 3
β’ ((π β§ πΆ β π) β πΆ β€ (π β¨ π)) |
48 | 1 | 4atexlems 38923 |
. . . . 5
β’ (π β π β π΄) |
49 | 1, 2, 3, 5 | 4atexlempns 38933 |
. . . . 5
β’ (π β π β π) |
50 | 5, 2, 3 | cvlsupr2 38213 |
. . . . 5
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ πΆ β π΄) β§ π β π) β ((π β¨ πΆ) = (π β¨ πΆ) β (πΆ β π β§ πΆ β π β§ πΆ β€ (π β¨ π)))) |
51 | 32, 33, 48, 10, 49, 50 | syl131anc 1384 |
. . . 4
β’ (π β ((π β¨ πΆ) = (π β¨ πΆ) β (πΆ β π β§ πΆ β π β§ πΆ β€ (π β¨ π)))) |
52 | 51 | adantr 482 |
. . 3
β’ ((π β§ πΆ β π) β ((π β¨ πΆ) = (π β¨ πΆ) β (πΆ β π β§ πΆ β π β§ πΆ β€ (π β¨ π)))) |
53 | 42, 43, 47, 52 | mpbir3and 1343 |
. 2
β’ ((π β§ πΆ β π) β (π β¨ πΆ) = (π β¨ πΆ)) |
54 | | breq1 5152 |
. . . . 5
β’ (π§ = πΆ β (π§ β€ π β πΆ β€ π)) |
55 | 54 | notbid 318 |
. . . 4
β’ (π§ = πΆ β (Β¬ π§ β€ π β Β¬ πΆ β€ π)) |
56 | | oveq2 7417 |
. . . . 5
β’ (π§ = πΆ β (π β¨ π§) = (π β¨ πΆ)) |
57 | | oveq2 7417 |
. . . . 5
β’ (π§ = πΆ β (π β¨ π§) = (π β¨ πΆ)) |
58 | 56, 57 | eqeq12d 2749 |
. . . 4
β’ (π§ = πΆ β ((π β¨ π§) = (π β¨ π§) β (π β¨ πΆ) = (π β¨ πΆ))) |
59 | 55, 58 | anbi12d 632 |
. . 3
β’ (π§ = πΆ β ((Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§)) β (Β¬ πΆ β€ π β§ (π β¨ πΆ) = (π β¨ πΆ)))) |
60 | 59 | rspcev 3613 |
. 2
β’ ((πΆ β π΄ β§ (Β¬ πΆ β€ π β§ (π β¨ πΆ) = (π β¨ πΆ))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |
61 | 11, 13, 53, 60 | syl12anc 836 |
1
β’ ((π β§ πΆ β π) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |