Step | Hyp | Ref
| Expression |
1 | | simp11l 1281 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΎ β HL) |
2 | | simp22l 1289 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π΄) |
3 | | simp11 1200 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΎ β HL β§ π β π»)) |
4 | | simp212 1309 |
. . 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 39524 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
10 | 3, 4, 2, 9 | syl3anc 1368 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΊβπ) β π΄) |
11 | | simp23 1205 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΉ) = (π
βπ)) |
12 | | simp213 1310 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π) |
13 | | simp12 1201 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΉ β π) |
14 | | simp13 1202 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π· β π) |
15 | | simp211 1308 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π) |
16 | | simp331 1323 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ·) β (π
βπΉ)) |
17 | | simp333 1325 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ) β (π
βπ·)) |
18 | 17 | necomd 2990 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ·) β (π
βπ)) |
19 | 16, 18 | jca 511 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπ))) |
20 | | simp311 1317 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΉ β ( I βΎ π΅)) |
21 | | simp32l 1295 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β ( I βΎ π΅)) |
22 | | simp312 1318 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π· β ( I βΎ π΅)) |
23 | 20, 21, 22 | 3jca 1125 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ π· β ( I βΎ π΅))) |
24 | | simp22 1204 |
. . 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 40250 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ π β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπ)βπ) β π΄) |
33 | 3, 11, 12, 13, 14, 15, 19, 23, 24, 32 | syl333anc 1399 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ)βπ) β π΄) |
34 | | simp32r 1296 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β (π
βπ)) |
35 | 34 | necomd 2990 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ) β (π
βπΊ)) |
36 | 6, 7, 8, 28 | trlcocnvat 40108 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ πΊ β π) β§ (π
βπ) β (π
βπΊ)) β (π
β(π β β‘πΊ)) β π΄) |
37 | 3, 12, 4, 35, 36 | syl121anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(π β β‘πΊ)) β π΄) |
38 | | simp332 1324 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β (π
βπ·)) |
39 | 38 | necomd 2990 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ·) β (π
βπΊ)) |
40 | 16, 39 | jca 511 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπΊ))) |
41 | | simp313 1319 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΊ β ( I βΎ π΅)) |
42 | 20, 41, 22 | 3jca 1125 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅))) |
43 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuat 40250 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) β π΄) |
44 | 3, 11, 4, 13, 14, 15, 40, 42, 24, 43 | syl333anc 1399 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β π΄) |
45 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuv2 40251 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) |
46 | 3, 11, 4, 13, 14, 15, 40, 42, 24, 45 | syl333anc 1399 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) |
47 | 1 | hllatd 38747 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΎ β Lat) |
48 | 25, 6, 7, 8, 28 | trlnidat 39557 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΊ β ( I βΎ π΅)) β (π
βπΊ) β π΄) |
49 | 3, 4, 41, 48 | syl3anc 1368 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β π΄) |
50 | 25, 26, 6 | hlatjcl 38750 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπΊ) β π΄) β (π β¨ (π
βπΊ)) β π΅) |
51 | 1, 2, 49, 50 | syl3anc 1368 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ (π
βπΊ)) β π΅) |
52 | | simp1 1133 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π)) |
53 | 15, 24, 11 | 3jca 1125 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) |
54 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30 | cdlemkoatnle 40235 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β ((πβπ) β π΄ β§ Β¬ (πβπ) β€ π)) |
55 | 54 | simpld 494 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β π΄) |
56 | 52, 53, 20, 22, 16, 55 | syl113anc 1379 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πβπ) β π΄) |
57 | 6, 7, 8, 28 | trlcocnvat 40108 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ π· β π) β§ (π
βπΊ) β (π
βπ·)) β (π
β(πΊ β β‘π·)) β π΄) |
58 | 3, 4, 14, 38, 57 | syl121anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(πΊ β β‘π·)) β π΄) |
59 | 25, 26, 6 | hlatjcl 38750 |
. . . . . 6
β’ ((πΎ β HL β§ (πβπ) β π΄ β§ (π
β(πΊ β β‘π·)) β π΄) β ((πβπ) β¨ (π
β(πΊ β β‘π·))) β π΅) |
60 | 1, 56, 58, 59 | syl3anc 1368 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ) β¨ (π
β(πΊ β β‘π·))) β π΅) |
61 | 25, 5, 27 | latmle1 18429 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ (π
βπΊ)) β π΅ β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))) β π΅) β ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))) β€ (π β¨ (π
βπΊ))) |
62 | 47, 51, 60, 61 | syl3anc 1368 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))) β€ (π β¨ (π
βπΊ))) |
63 | 46, 62 | eqbrtrd 5163 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β€ (π β¨ (π
βπΊ))) |
64 | 5, 26, 6, 7, 8, 28 | trljat1 39550 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
βπΊ)) = (π β¨ (πΊβπ))) |
65 | 3, 4, 24, 64 | syl3anc 1368 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ (π
βπΊ)) = (π β¨ (πΊβπ))) |
66 | 63, 65 | breqtrd 5167 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β€ (π β¨ (πΊβπ))) |
67 | | simp2 1134 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) |
68 | | simp31 1206 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅))) |
69 | | simp33 1208 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·))) |
70 | | eqid 2726 |
. . . 4
β’ (((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·)))) = (((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·)))) |
71 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31, 70 | cdlemk11u 40255 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
72 | 52, 67, 68, 21, 69, 71 | syl113anc 1379 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
73 | 5, 26, 6 | hlatlej2 38759 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπΊ) β π΄) β (π
βπΊ) β€ (π β¨ (π
βπΊ))) |
74 | 1, 2, 49, 73 | syl3anc 1368 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β€ (π β¨ (π
βπΊ))) |
75 | 74, 65 | breqtrd 5167 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β€ (π β¨ (πΊβπ))) |
76 | 25, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31 | cdlemkuel 40249 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ π β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπ) β π) |
77 | 3, 11, 12, 13, 14, 15, 19, 23, 24, 76 | syl333anc 1399 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πβπ) β π) |
78 | 5, 6, 7, 8 | ltrnel 39523 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπ) β π β§ (π β π΄ β§ Β¬ π β€ π)) β (((πβπ)βπ) β π΄ β§ Β¬ ((πβπ)βπ) β€ π)) |
79 | 3, 77, 24, 78 | syl3anc 1368 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (((πβπ)βπ) β π΄ β§ Β¬ ((πβπ)βπ) β€ π)) |
80 | 7, 8 | ltrncnv 39530 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β β‘πΊ β π) |
81 | 3, 4, 80 | syl2anc 583 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β β‘πΊ β π) |
82 | 7, 8, 28 | trlcnv 39549 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
ββ‘πΊ) = (π
βπΊ)) |
83 | 3, 4, 82 | syl2anc 583 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
ββ‘πΊ) = (π
βπΊ)) |
84 | 83, 34 | eqnetrd 3002 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
ββ‘πΊ) β (π
βπ)) |
85 | 25, 7, 8, 28 | trlcone 40112 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (β‘πΊ β π β§ π β π) β§ ((π
ββ‘πΊ) β (π
βπ) β§ π β ( I βΎ π΅))) β (π
ββ‘πΊ) β (π
β(β‘πΊ β π))) |
86 | 3, 81, 12, 84, 21, 85 | syl122anc 1376 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
ββ‘πΊ) β (π
β(β‘πΊ β π))) |
87 | 86 | necomd 2990 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(β‘πΊ β π)) β (π
ββ‘πΊ)) |
88 | 7, 8 | ltrncom 40122 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ β‘πΊ β π β§ π β π) β (β‘πΊ β π) = (π β β‘πΊ)) |
89 | 3, 81, 12, 88 | syl3anc 1368 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (β‘πΊ β π) = (π β β‘πΊ)) |
90 | 89 | fveq2d 6889 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(β‘πΊ β π)) = (π
β(π β β‘πΊ))) |
91 | 87, 90, 83 | 3netr3d 3011 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(π β β‘πΊ)) β (π
βπΊ)) |
92 | 7, 8 | ltrnco 40103 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π β§ β‘πΊ β π) β (π β β‘πΊ) β π) |
93 | 3, 12, 81, 92 | syl3anc 1368 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β β‘πΊ) β π) |
94 | 5, 7, 8, 28 | trlle 39568 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β β‘πΊ) β π) β (π
β(π β β‘πΊ)) β€ π) |
95 | 3, 93, 94 | syl2anc 583 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(π β β‘πΊ)) β€ π) |
96 | 5, 7, 8, 28 | trlle 39568 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β€ π) |
97 | 3, 4, 96 | syl2anc 583 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β€ π) |
98 | 5, 26, 6, 7 | lhp2atnle 39417 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (((πβπ)βπ) β π΄ β§ Β¬ ((πβπ)βπ) β€ π) β§ (π
β(π β β‘πΊ)) β (π
βπΊ)) β§ ((π
β(π β β‘πΊ)) β π΄ β§ (π
β(π β β‘πΊ)) β€ π) β§ ((π
βπΊ) β π΄ β§ (π
βπΊ) β€ π)) β Β¬ (π
βπΊ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
99 | 3, 79, 91, 37, 95, 49, 97, 98 | syl322anc 1395 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β Β¬ (π
βπΊ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
100 | | nbrne1 5160 |
. . 3
β’ (((π
βπΊ) β€ (π β¨ (πΊβπ)) β§ Β¬ (π
βπΊ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) β (π β¨ (πΊβπ)) β (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
101 | 75, 99, 100 | syl2anc 583 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ (πΊβπ)) β (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
102 | 5, 26, 27, 6 | 2atm 38911 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ (πΊβπ) β π΄) β§ (((πβπ)βπ) β π΄ β§ (π
β(π β β‘πΊ)) β π΄ β§ ((πβπΊ)βπ) β π΄) β§ (((πβπΊ)βπ) β€ (π β¨ (πΊβπ)) β§ ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))) β§ (π β¨ (πΊβπ)) β (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))))) |
103 | 1, 2, 10, 33, 37, 44, 66, 72, 101, 102 | syl333anc 1399 |
1
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπ)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))))) |