Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (πΎ β HL β§ π β π»)) |
2 | | simpl31 1255 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β π΄ β§ Β¬ π β€ π)) |
3 | | simpl2 1193 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β πΉ β π) |
4 | | simpr 486 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (πΉβπ) = π) |
5 | | trlval3.l |
. . . . 5
β’ β€ =
(leβπΎ) |
6 | | eqid 2737 |
. . . . 5
β’
(0.βπΎ) =
(0.βπΎ) |
7 | | trlval3.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
8 | | trlval3.h |
. . . . 5
β’ π» = (LHypβπΎ) |
9 | | trlval3.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
10 | | trlval3.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
11 | 5, 6, 7, 8, 9, 10 | trl0 38636 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) = π)) β (π
βπΉ) = (0.βπΎ)) |
12 | 1, 2, 3, 4, 11 | syl112anc 1375 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π
βπΉ) = (0.βπΎ)) |
13 | | simpl33 1257 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β¨ (πΉβπ)) β (π β¨ (πΉβπ))) |
14 | | simpl1l 1225 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β πΎ β HL) |
15 | | hlatl 37825 |
. . . . . 6
β’ (πΎ β HL β πΎ β AtLat) |
16 | 14, 15 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β πΎ β AtLat) |
17 | 4 | oveq2d 7374 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β¨ (πΉβπ)) = (π β¨ π)) |
18 | | simp31l 1297 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β π β π΄) |
19 | 18 | adantr 482 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β π β π΄) |
20 | | trlval3.j |
. . . . . . . . 9
β’ β¨ =
(joinβπΎ) |
21 | 20, 7 | hlatjidm 37834 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
22 | 14, 19, 21 | syl2anc 585 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β¨ π) = π) |
23 | 17, 22 | eqtrd 2777 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β¨ (πΉβπ)) = π) |
24 | 23, 19 | eqeltrd 2838 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β¨ (πΉβπ)) β π΄) |
25 | | simp1 1137 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β (πΎ β HL β§ π β π»)) |
26 | | simp2 1138 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β πΉ β π) |
27 | | simp31 1210 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β (π β π΄ β§ Β¬ π β€ π)) |
28 | | simp32 1211 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β (π β π΄ β§ Β¬ π β€ π)) |
29 | 5, 7, 8, 9 | ltrn2ateq 38646 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πΉβπ) = π β (πΉβπ) = π)) |
30 | 25, 26, 27, 28, 29 | syl13anc 1373 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β ((πΉβπ) = π β (πΉβπ) = π)) |
31 | 30 | biimpa 478 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (πΉβπ) = π) |
32 | 31 | oveq2d 7374 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β¨ (πΉβπ)) = (π β¨ π)) |
33 | | simp32l 1299 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β π β π΄) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β π β π΄) |
35 | 20, 7 | hlatjidm 37834 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
36 | 14, 34, 35 | syl2anc 585 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β¨ π) = π) |
37 | 32, 36 | eqtrd 2777 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β¨ (πΉβπ)) = π) |
38 | 37, 34 | eqeltrd 2838 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π β¨ (πΉβπ)) β π΄) |
39 | | trlval3.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
40 | 39, 6, 7 | atnem0 37783 |
. . . . 5
β’ ((πΎ β AtLat β§ (π β¨ (πΉβπ)) β π΄ β§ (π β¨ (πΉβπ)) β π΄) β ((π β¨ (πΉβπ)) β (π β¨ (πΉβπ)) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) = (0.βπΎ))) |
41 | 16, 24, 38, 40 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β ((π β¨ (πΉβπ)) β (π β¨ (πΉβπ)) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) = (0.βπΎ))) |
42 | 13, 41 | mpbid 231 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) = (0.βπΎ)) |
43 | 12, 42 | eqtr4d 2780 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) = π) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ)))) |
44 | | simpl1 1192 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (πΎ β HL β§ π β π»)) |
45 | | simpl2 1193 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β πΉ β π) |
46 | | simpl31 1255 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π β π΄ β§ Β¬ π β€ π)) |
47 | 5, 20, 39, 7, 8, 9,
10 | trlval2 38629 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ π)) |
48 | 44, 45, 46, 47 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ π)) |
49 | | simpl1l 1225 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β πΎ β HL) |
50 | 49 | hllatd 37829 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β πΎ β Lat) |
51 | 18 | adantr 482 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β π β π΄) |
52 | 5, 7, 8, 9 | ltrnat 38606 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) |
53 | 44, 45, 51, 52 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (πΉβπ) β π΄) |
54 | | eqid 2737 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
55 | 54, 20, 7 | hlatjcl 37832 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβπ) β π΄) β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
56 | 49, 51, 53, 55 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
57 | | simpl1r 1226 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β π β π») |
58 | 54, 8 | lhpbase 38464 |
. . . . . . 7
β’ (π β π» β π β (BaseβπΎ)) |
59 | 57, 58 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β π β (BaseβπΎ)) |
60 | 54, 5, 39 | latmle1 18354 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β¨ (πΉβπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ (πΉβπ)) β§ π) β€ (π β¨ (πΉβπ))) |
61 | 50, 56, 59, 60 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β ((π β¨ (πΉβπ)) β§ π) β€ (π β¨ (πΉβπ))) |
62 | 48, 61 | eqbrtrd 5128 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π
βπΉ) β€ (π β¨ (πΉβπ))) |
63 | | simpl32 1256 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π β π΄ β§ Β¬ π β€ π)) |
64 | 5, 20, 39, 7, 8, 9,
10 | trlval2 38629 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ π)) |
65 | 44, 45, 63, 64 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ π)) |
66 | 33 | adantr 482 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β π β π΄) |
67 | 5, 7, 8, 9 | ltrnat 38606 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) |
68 | 44, 45, 66, 67 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (πΉβπ) β π΄) |
69 | 54, 20, 7 | hlatjcl 37832 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβπ) β π΄) β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
70 | 49, 66, 68, 69 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
71 | 54, 5, 39 | latmle1 18354 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β¨ (πΉβπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ (πΉβπ)) β§ π) β€ (π β¨ (πΉβπ))) |
72 | 50, 70, 59, 71 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β ((π β¨ (πΉβπ)) β§ π) β€ (π β¨ (πΉβπ))) |
73 | 65, 72 | eqbrtrd 5128 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π
βπΉ) β€ (π β¨ (πΉβπ))) |
74 | 54, 8, 9, 10 | trlcl 38630 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β (BaseβπΎ)) |
75 | 44, 45, 74 | syl2anc 585 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π
βπΉ) β (BaseβπΎ)) |
76 | 54, 5, 39 | latlem12 18356 |
. . . . 5
β’ ((πΎ β Lat β§ ((π
βπΉ) β (BaseβπΎ) β§ (π β¨ (πΉβπ)) β (BaseβπΎ) β§ (π β¨ (πΉβπ)) β (BaseβπΎ))) β (((π
βπΉ) β€ (π β¨ (πΉβπ)) β§ (π
βπΉ) β€ (π β¨ (πΉβπ))) β (π
βπΉ) β€ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))))) |
77 | 50, 75, 56, 70, 76 | syl13anc 1373 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (((π
βπΉ) β€ (π β¨ (πΉβπ)) β§ (π
βπΉ) β€ (π β¨ (πΉβπ))) β (π
βπΉ) β€ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))))) |
78 | 62, 73, 77 | mpbi2and 711 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π
βπΉ) β€ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ)))) |
79 | 49, 15 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β πΎ β AtLat) |
80 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (πΉβπ) β π) |
81 | 5, 7, 8, 9, 10 | trlat 38635 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) β π)) β (π
βπΉ) β π΄) |
82 | 44, 46, 45, 80, 81 | syl112anc 1375 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π
βπΉ) β π΄) |
83 | 54, 39 | latmcl 18330 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β¨ (πΉβπ)) β (BaseβπΎ) β§ (π β¨ (πΉβπ)) β (BaseβπΎ)) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β (BaseβπΎ)) |
84 | 50, 56, 70, 83 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β (BaseβπΎ)) |
85 | 54, 5, 6, 7 | atlen0 37775 |
. . . . . . 7
β’ (((πΎ β AtLat β§ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β (BaseβπΎ) β§ (π
βπΉ) β π΄) β§ (π
βπΉ) β€ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ)))) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β (0.βπΎ)) |
86 | 79, 84, 82, 78, 85 | syl31anc 1374 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β (0.βπΎ)) |
87 | 86 | neneqd 2949 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β Β¬ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) = (0.βπΎ)) |
88 | | simpl33 1257 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π β¨ (πΉβπ)) β (π β¨ (πΉβπ))) |
89 | 20, 39, 6, 7 | 2atmat0 37992 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ (πΉβπ) β π΄) β§ (π β π΄ β§ (πΉβπ) β π΄ β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β (((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β π΄ β¨ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) = (0.βπΎ))) |
90 | 49, 51, 53, 66, 68, 88, 89 | syl33anc 1386 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β π΄ β¨ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) = (0.βπΎ))) |
91 | 90 | ord 863 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (Β¬ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β π΄ β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) = (0.βπΎ))) |
92 | 87, 91 | mt3d 148 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β π΄) |
93 | 5, 7 | atcmp 37776 |
. . . 4
β’ ((πΎ β AtLat β§ (π
βπΉ) β π΄ β§ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β π΄) β ((π
βπΉ) β€ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))))) |
94 | 79, 82, 92, 93 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β ((π
βπΉ) β€ ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))))) |
95 | 78, 94 | mpbid 231 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β§ (πΉβπ) β π) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ)))) |
96 | 43, 95 | pm2.61dane 3033 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ)))) |