Step | Hyp | Ref
| Expression |
1 | | simp11l 1285 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΎ β HL) |
2 | | simp22l 1293 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π΄) |
3 | | simp11 1204 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΎ β HL β§ π β π»)) |
4 | | simp212 1313 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΊ β π) |
5 | | cdlemk1.l |
. . . 4
β’ β€ =
(leβπΎ) |
6 | | cdlemk1.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
7 | | cdlemk1.h |
. . . 4
β’ π» = (LHypβπΎ) |
8 | | cdlemk1.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
9 | 5, 6, 7, 8 | ltrnat 39011 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
10 | 3, 4, 2, 9 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΊβπ) β π΄) |
11 | | simp23 1209 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΉ) = (π
βπ)) |
12 | | simp213 1314 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π) |
13 | | simp12 1205 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΉ β π) |
14 | | simp13 1206 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π· β π) |
15 | | simp211 1312 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π) |
16 | | simp331 1327 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ·) β (π
βπΉ)) |
17 | | simp333 1329 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ) β (π
βπ·)) |
18 | 17 | necomd 2997 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ·) β (π
βπ)) |
19 | 16, 18 | jca 513 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπ))) |
20 | | simp311 1321 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΉ β ( I βΎ π΅)) |
21 | | simp32l 1299 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β ( I βΎ π΅)) |
22 | | simp312 1322 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π· β ( I βΎ π΅)) |
23 | 20, 21, 22 | 3jca 1129 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ π· β ( I βΎ π΅))) |
24 | | simp22 1208 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β π΄ β§ Β¬ π β€ π)) |
25 | | cdlemk1.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
26 | | cdlemk1.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
27 | | cdlemk1.m |
. . . 4
β’ β§ =
(meetβπΎ) |
28 | | cdlemk1.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
29 | | cdlemk1.s |
. . . 4
β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))))) |
30 | | cdlemk1.o |
. . . 4
β’ π = (πβπ·) |
31 | | cdlemk1.u |
. . . 4
β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·)))))) |
32 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuat 39737 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ π β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπ)βπ) β π΄) |
33 | 3, 11, 12, 13, 14, 15, 19, 23, 24, 32 | syl333anc 1403 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ)βπ) β π΄) |
34 | | simp32r 1300 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β (π
βπ)) |
35 | 34 | necomd 2997 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ) β (π
βπΊ)) |
36 | 6, 7, 8, 28 | trlcocnvat 39595 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ πΊ β π) β§ (π
βπ) β (π
βπΊ)) β (π
β(π β β‘πΊ)) β π΄) |
37 | 3, 12, 4, 35, 36 | syl121anc 1376 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(π β β‘πΊ)) β π΄) |
38 | | simp332 1328 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β (π
βπ·)) |
39 | 38 | necomd 2997 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ·) β (π
βπΊ)) |
40 | 16, 39 | jca 513 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπΊ))) |
41 | | simp313 1323 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΊ β ( I βΎ π΅)) |
42 | 20, 41, 22 | 3jca 1129 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅))) |
43 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuat 39737 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) β π΄) |
44 | 3, 11, 4, 13, 14, 15, 40, 42, 24, 43 | syl333anc 1403 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β π΄) |
45 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuv2 39738 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) |
46 | 3, 11, 4, 13, 14, 15, 40, 42, 24, 45 | syl333anc 1403 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) |
47 | 1 | hllatd 38234 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΎ β Lat) |
48 | 25, 6, 7, 8, 28 | trlnidat 39044 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΊ β ( I βΎ π΅)) β (π
βπΊ) β π΄) |
49 | 3, 4, 41, 48 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β π΄) |
50 | 25, 26, 6 | hlatjcl 38237 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπΊ) β π΄) β (π β¨ (π
βπΊ)) β π΅) |
51 | 1, 2, 49, 50 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ (π
βπΊ)) β π΅) |
52 | | simp1 1137 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π)) |
53 | 15, 24, 11 | 3jca 1129 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) |
54 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30 | cdlemkoatnle 39722 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β ((πβπ) β π΄ β§ Β¬ (πβπ) β€ π)) |
55 | 54 | simpld 496 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β π΄) |
56 | 52, 53, 20, 22, 16, 55 | syl113anc 1383 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πβπ) β π΄) |
57 | 6, 7, 8, 28 | trlcocnvat 39595 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ π· β π) β§ (π
βπΊ) β (π
βπ·)) β (π
β(πΊ β β‘π·)) β π΄) |
58 | 3, 4, 14, 38, 57 | syl121anc 1376 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(πΊ β β‘π·)) β π΄) |
59 | 25, 26, 6 | hlatjcl 38237 |
. . . . . 6
β’ ((πΎ β HL β§ (πβπ) β π΄ β§ (π
β(πΊ β β‘π·)) β π΄) β ((πβπ) β¨ (π
β(πΊ β β‘π·))) β π΅) |
60 | 1, 56, 58, 59 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ) β¨ (π
β(πΊ β β‘π·))) β π΅) |
61 | 25, 5, 27 | latmle1 18417 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ (π
βπΊ)) β π΅ β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))) β π΅) β ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))) β€ (π β¨ (π
βπΊ))) |
62 | 47, 51, 60, 61 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))) β€ (π β¨ (π
βπΊ))) |
63 | 46, 62 | eqbrtrd 5171 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β€ (π β¨ (π
βπΊ))) |
64 | 5, 26, 6, 7, 8, 28 | trljat1 39037 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
βπΊ)) = (π β¨ (πΊβπ))) |
65 | 3, 4, 24, 64 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ (π
βπΊ)) = (π β¨ (πΊβπ))) |
66 | 63, 65 | breqtrd 5175 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β€ (π β¨ (πΊβπ))) |
67 | | simp2 1138 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) |
68 | | simp31 1210 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅))) |
69 | | simp33 1212 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·))) |
70 | | eqid 2733 |
. . . 4
β’ (((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·)))) = (((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·)))) |
71 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31, 70 | cdlemk11u 39742 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
72 | 52, 67, 68, 21, 69, 71 | syl113anc 1383 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
73 | 5, 26, 6 | hlatlej2 38246 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπΊ) β π΄) β (π
βπΊ) β€ (π β¨ (π
βπΊ))) |
74 | 1, 2, 49, 73 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β€ (π β¨ (π
βπΊ))) |
75 | 74, 65 | breqtrd 5175 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β€ (π β¨ (πΊβπ))) |
76 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuel 39736 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ π β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπ) β π) |
77 | 3, 11, 12, 13, 14, 15, 19, 23, 24, 76 | syl333anc 1403 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πβπ) β π) |
78 | 5, 6, 7, 8 | ltrnel 39010 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπ) β π β§ (π β π΄ β§ Β¬ π β€ π)) β (((πβπ)βπ) β π΄ β§ Β¬ ((πβπ)βπ) β€ π)) |
79 | 3, 77, 24, 78 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (((πβπ)βπ) β π΄ β§ Β¬ ((πβπ)βπ) β€ π)) |
80 | 7, 8 | ltrncnv 39017 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β β‘πΊ β π) |
81 | 3, 4, 80 | syl2anc 585 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β β‘πΊ β π) |
82 | 7, 8, 28 | trlcnv 39036 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
ββ‘πΊ) = (π
βπΊ)) |
83 | 3, 4, 82 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
ββ‘πΊ) = (π
βπΊ)) |
84 | 83, 34 | eqnetrd 3009 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
ββ‘πΊ) β (π
βπ)) |
85 | 25, 7, 8, 28 | trlcone 39599 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (β‘πΊ β π β§ π β π) β§ ((π
ββ‘πΊ) β (π
βπ) β§ π β ( I βΎ π΅))) β (π
ββ‘πΊ) β (π
β(β‘πΊ β π))) |
86 | 3, 81, 12, 84, 21, 85 | syl122anc 1380 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
ββ‘πΊ) β (π
β(β‘πΊ β π))) |
87 | 86 | necomd 2997 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(β‘πΊ β π)) β (π
ββ‘πΊ)) |
88 | 7, 8 | ltrncom 39609 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ β‘πΊ β π β§ π β π) β (β‘πΊ β π) = (π β β‘πΊ)) |
89 | 3, 81, 12, 88 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (β‘πΊ β π) = (π β β‘πΊ)) |
90 | 89 | fveq2d 6896 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(β‘πΊ β π)) = (π
β(π β β‘πΊ))) |
91 | 87, 90, 83 | 3netr3d 3018 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(π β β‘πΊ)) β (π
βπΊ)) |
92 | 7, 8 | ltrnco 39590 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π β§ β‘πΊ β π) β (π β β‘πΊ) β π) |
93 | 3, 12, 81, 92 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β β‘πΊ) β π) |
94 | 5, 7, 8, 28 | trlle 39055 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β β‘πΊ) β π) β (π
β(π β β‘πΊ)) β€ π) |
95 | 3, 93, 94 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(π β β‘πΊ)) β€ π) |
96 | 5, 7, 8, 28 | trlle 39055 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β€ π) |
97 | 3, 4, 96 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β€ π) |
98 | 5, 26, 6, 7 | lhp2atnle 38904 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (((πβπ)βπ) β π΄ β§ Β¬ ((πβπ)βπ) β€ π) β§ (π
β(π β β‘πΊ)) β (π
βπΊ)) β§ ((π
β(π β β‘πΊ)) β π΄ β§ (π
β(π β β‘πΊ)) β€ π) β§ ((π
βπΊ) β π΄ β§ (π
βπΊ) β€ π)) β Β¬ (π
βπΊ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
99 | 3, 79, 91, 37, 95, 49, 97, 98 | syl322anc 1399 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β Β¬ (π
βπΊ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
100 | | nbrne1 5168 |
. . 3
β’ (((π
βπΊ) β€ (π β¨ (πΊβπ)) β§ Β¬ (π
βπΊ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) β (π β¨ (πΊβπ)) β (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
101 | 75, 99, 100 | syl2anc 585 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ (πΊβπ)) β (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
102 | 5, 26, 27, 6 | 2atm 38398 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ (πΊβπ) β π΄) β§ (((πβπ)βπ) β π΄ β§ (π
β(π β β‘πΊ)) β π΄ β§ ((πβπΊ)βπ) β π΄) β§ (((πβπΊ)βπ) β€ (π β¨ (πΊβπ)) β§ ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))) β§ (π β¨ (πΊβπ)) β (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))))) |
103 | 1, 2, 10, 33, 37, 44, 66, 72, 101, 102 | syl333anc 1403 |
1
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))))) |