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 39032 |
. . 3
β’ (π β πΆ β π΄) |
11 | 10 | adantr 481 |
. 2
β’ ((π β§ πΆ β π) β πΆ β π΄) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | 4atexlemnclw 39033 |
. . 3
β’ (π β Β¬ πΆ β€ π) |
13 | 12 | adantr 481 |
. 2
β’ ((π β§ πΆ β π) β Β¬ πΆ β€ π) |
14 | 1, 2, 3, 4, 5, 6, 7, 8 | 4atexlemntlpq 39031 |
. . . . 5
β’ (π β Β¬ π β€ (π β¨ π)) |
15 | | id 22 |
. . . . . . . . . . 11
β’ (πΆ = π β πΆ = π) |
16 | 9, 15 | eqtr3id 2786 |
. . . . . . . . . 10
β’ (πΆ = π β ((π β¨ π) β§ (π β¨ π)) = π) |
17 | 16 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ πΆ = π) β ((π β¨ π) β§ (π β¨ π)) = π) |
18 | 1 | 4atexlemkl 39020 |
. . . . . . . . . . . 12
β’ (π β πΎ β Lat) |
19 | 1, 3, 5 | 4atexlemqtb 39024 |
. . . . . . . . . . . 12
β’ (π β (π β¨ π) β (BaseβπΎ)) |
20 | 1, 3, 5 | 4atexlempsb 39023 |
. . . . . . . . . . . 12
β’ (π β (π β¨ π) β (BaseβπΎ)) |
21 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(BaseβπΎ) =
(BaseβπΎ) |
22 | 21, 2, 4 | latmle1 18419 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
23 | 18, 19, 20, 22 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (π β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
24 | 1 | 4atexlemk 39010 |
. . . . . . . . . . . 12
β’ (π β πΎ β HL) |
25 | 1 | 4atexlemq 39014 |
. . . . . . . . . . . 12
β’ (π β π β π΄) |
26 | 1 | 4atexlemt 39016 |
. . . . . . . . . . . 12
β’ (π β π β π΄) |
27 | 3, 5 | hlatjcom 38330 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
28 | 24, 25, 26, 27 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (π β (π β¨ π) = (π β¨ π)) |
29 | 23, 28 | breqtrd 5174 |
. . . . . . . . . 10
β’ (π β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
30 | 29 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ πΆ = π) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
31 | 17, 30 | eqbrtrrd 5172 |
. . . . . . . 8
β’ ((π β§ πΆ = π) β π β€ (π β¨ π)) |
32 | 1 | 4atexlemkc 39021 |
. . . . . . . . . 10
β’ (π β πΎ β CvLat) |
33 | 1 | 4atexlemp 39013 |
. . . . . . . . . 10
β’ (π β π β π΄) |
34 | 1 | 4atexlempnq 39018 |
. . . . . . . . . 10
β’ (π β π β π) |
35 | 2, 3, 5 | cvlatexch2 38299 |
. . . . . . . . . 10
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
36 | 32, 33, 26, 25, 34, 35 | syl131anc 1383 |
. . . . . . . . 9
β’ (π β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
37 | 36 | adantr 481 |
. . . . . . . 8
β’ ((π β§ πΆ = π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
38 | 31, 37 | mpd 15 |
. . . . . . 7
β’ ((π β§ πΆ = π) β π β€ (π β¨ π)) |
39 | 38 | ex 413 |
. . . . . 6
β’ (π β (πΆ = π β π β€ (π β¨ π))) |
40 | 39 | necon3bd 2954 |
. . . . 5
β’ (π β (Β¬ π β€ (π β¨ π) β πΆ β π)) |
41 | 14, 40 | mpd 15 |
. . . 4
β’ (π β πΆ β π) |
42 | 41 | adantr 481 |
. . 3
β’ ((π β§ πΆ β π) β πΆ β π) |
43 | | simpr 485 |
. . 3
β’ ((π β§ πΆ β π) β πΆ β π) |
44 | 21, 2, 4 | latmle2 18420 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
45 | 18, 19, 20, 44 | syl3anc 1371 |
. . . . 5
β’ (π β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
46 | 9, 45 | eqbrtrid 5183 |
. . . 4
β’ (π β πΆ β€ (π β¨ π)) |
47 | 46 | adantr 481 |
. . 3
β’ ((π β§ πΆ β π) β πΆ β€ (π β¨ π)) |
48 | 1 | 4atexlems 39015 |
. . . . 5
β’ (π β π β π΄) |
49 | 1, 2, 3, 5 | 4atexlempns 39025 |
. . . . 5
β’ (π β π β π) |
50 | 5, 2, 3 | cvlsupr2 38305 |
. . . . 5
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ πΆ β π΄) β§ π β π) β ((π β¨ πΆ) = (π β¨ πΆ) β (πΆ β π β§ πΆ β π β§ πΆ β€ (π β¨ π)))) |
51 | 32, 33, 48, 10, 49, 50 | syl131anc 1383 |
. . . 4
β’ (π β ((π β¨ πΆ) = (π β¨ πΆ) β (πΆ β π β§ πΆ β π β§ πΆ β€ (π β¨ π)))) |
52 | 51 | adantr 481 |
. . 3
β’ ((π β§ πΆ β π) β ((π β¨ πΆ) = (π β¨ πΆ) β (πΆ β π β§ πΆ β π β§ πΆ β€ (π β¨ π)))) |
53 | 42, 43, 47, 52 | mpbir3and 1342 |
. 2
β’ ((π β§ πΆ β π) β (π β¨ πΆ) = (π β¨ πΆ)) |
54 | | breq1 5151 |
. . . . 5
β’ (π§ = πΆ β (π§ β€ π β πΆ β€ π)) |
55 | 54 | notbid 317 |
. . . 4
β’ (π§ = πΆ β (Β¬ π§ β€ π β Β¬ πΆ β€ π)) |
56 | | oveq2 7419 |
. . . . 5
β’ (π§ = πΆ β (π β¨ π§) = (π β¨ πΆ)) |
57 | | oveq2 7419 |
. . . . 5
β’ (π§ = πΆ β (π β¨ π§) = (π β¨ πΆ)) |
58 | 56, 57 | eqeq12d 2748 |
. . . 4
β’ (π§ = πΆ β ((π β¨ π§) = (π β¨ π§) β (π β¨ πΆ) = (π β¨ πΆ))) |
59 | 55, 58 | anbi12d 631 |
. . 3
β’ (π§ = πΆ β ((Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§)) β (Β¬ πΆ β€ π β§ (π β¨ πΆ) = (π β¨ πΆ)))) |
60 | 59 | rspcev 3612 |
. 2
β’ ((πΆ β π΄ β§ (Β¬ πΆ β€ π β§ (π β¨ πΆ) = (π β¨ πΆ))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |
61 | 11, 13, 53, 60 | syl12anc 835 |
1
β’ ((π β§ πΆ β π) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |