Step | Hyp | Ref
| Expression |
1 | | simp31 1209 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅))) |
2 | | simp33 1211 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·))) |
3 | 1, 2 | jca 512 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) |
4 | | cdlemk1.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
5 | | cdlemk1.l |
. . . 4
β’ β€ =
(leβπΎ) |
6 | | cdlemk1.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
7 | | cdlemk1.m |
. . . 4
β’ β§ =
(meetβπΎ) |
8 | | cdlemk1.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
9 | | cdlemk1.h |
. . . 4
β’ π» = (LHypβπΎ) |
10 | | cdlemk1.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
11 | | cdlemk1.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
12 | | cdlemk1.s |
. . . 4
β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))))) |
13 | | cdlemk1.o |
. . . 4
β’ π = (πβπ·) |
14 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | cdlemk6u 39721 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))) β€ ((((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·)))) β¨ (((πβπ) β¨ π) β§ ((π
β(π β β‘π·)) β¨ (πβπ))))) |
15 | 3, 14 | syld3an3 1409 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))) β€ ((((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·)))) β¨ (((πβπ) β¨ π) β§ ((π
β(π β β‘π·)) β¨ (πβπ))))) |
16 | | simp11l 1284 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΎ β HL) |
17 | | simp11r 1285 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π») |
18 | 16, 17 | jca 512 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΎ β HL β§ π β π»)) |
19 | | simp23 1208 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΉ) = (π
βπ)) |
20 | | simp212 1312 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΊ β π) |
21 | | simp12 1204 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΉ β π) |
22 | | simp13 1205 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π· β π) |
23 | | simp211 1311 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π) |
24 | 21, 22, 23 | 3jca 1128 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β π β§ π· β π β§ π β π)) |
25 | | simp331 1326 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ·) β (π
βπΉ)) |
26 | | simp332 1327 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπΊ) β (π
βπ·)) |
27 | 26 | necomd 2996 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ·) β (π
βπΊ)) |
28 | 25, 27 | jca 512 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπΊ))) |
29 | | simp311 1320 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΉ β ( I βΎ π΅)) |
30 | | simp313 1322 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΊ β ( I βΎ π΅)) |
31 | | simp312 1321 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π· β ( I βΎ π΅)) |
32 | 29, 30, 31 | 3jca 1128 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅))) |
33 | | simp22 1207 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β π΄ β§ Β¬ π β€ π)) |
34 | | cdlemk1.u |
. . . . 5
β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·)))))) |
35 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 34 | cdlemkuv2 39726 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) |
36 | 18, 19, 20, 24, 28, 32, 33, 35 | syl313anc 1394 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) |
37 | 5, 6, 8, 9, 10, 11 | trljat1 39025 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
βπΊ)) = (π β¨ (πΊβπ))) |
38 | 18, 20, 33, 37 | syl3anc 1371 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ (π
βπΊ)) = (π β¨ (πΊβπ))) |
39 | 38 | oveq1d 7420 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))) = ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) |
40 | 36, 39 | eqtrd 2772 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) |
41 | 16 | hllatd 38222 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β πΎ β Lat) |
42 | | simp213 1313 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π) |
43 | | simp333 1328 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ) β (π
βπ·)) |
44 | 43 | necomd 2996 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
βπ·) β (π
βπ)) |
45 | 25, 44 | jca 512 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπ))) |
46 | | simp32 1210 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β ( I βΎ π΅)) |
47 | 29, 46, 31 | 3jca 1128 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ π· β ( I βΎ π΅))) |
48 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 34 | cdlemkuat 39725 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ π β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπ)βπ) β π΄) |
49 | 18, 19, 42, 24, 45, 47, 33, 48 | syl313anc 1394 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ)βπ) β π΄) |
50 | 4, 8 | atbase 38147 |
. . . . 5
β’ (((πβπ)βπ) β π΄ β ((πβπ)βπ) β π΅) |
51 | 49, 50 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ)βπ) β π΅) |
52 | | simp22l 1292 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π΄) |
53 | | cdlemk1.v |
. . . . . 6
β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·)))) |
54 | 4, 5, 6, 8, 9, 10,
11, 7, 53 | cdlemkvcl 39701 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π· β π β§ πΊ β π β§ π β π) β§ π β π΄) β π β π΅) |
55 | 16, 17, 22, 20, 42, 52, 54 | syl231anc 1390 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π β π΅) |
56 | 4, 6 | latjcom 18396 |
. . . 4
β’ ((πΎ β Lat β§ ((πβπ)βπ) β π΅ β§ π β π΅) β (((πβπ)βπ) β¨ π) = (π β¨ ((πβπ)βπ))) |
57 | 41, 51, 55, 56 | syl3anc 1371 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (((πβπ)βπ) β¨ π) = (π β¨ ((πβπ)βπ))) |
58 | 53 | a1i 11 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β π = (((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·))))) |
59 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 34 | cdlemkuv2 39726 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ) β§ π β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π
βπ·) β (π
βπΉ) β§ (π
βπ·) β (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπ)βπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·))))) |
60 | 18, 19, 42, 24, 45, 47, 33, 59 | syl313anc 1394 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ)βπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·))))) |
61 | 5, 6, 8, 9, 10, 11 | trljat1 39025 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
βπ)) = (π β¨ (πβπ))) |
62 | 18, 42, 33, 61 | syl3anc 1371 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ (π
βπ)) = (π β¨ (πβπ))) |
63 | 5, 8, 9, 10 | ltrnat 38999 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π΄) β (πβπ) β π΄) |
64 | 18, 42, 52, 63 | syl3anc 1371 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πβπ) β π΄) |
65 | 6, 8 | hlatjcom 38226 |
. . . . . . . 8
β’ ((πΎ β HL β§ (πβπ) β π΄ β§ π β π΄) β ((πβπ) β¨ π) = (π β¨ (πβπ))) |
66 | 16, 64, 52, 65 | syl3anc 1371 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ) β¨ π) = (π β¨ (πβπ))) |
67 | 62, 66 | eqtr4d 2775 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ (π
βπ)) = ((πβπ) β¨ π)) |
68 | | simp1 1136 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π)) |
69 | 23, 33, 19 | 3jca 1128 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) |
70 | 29, 31, 25 | 3jca 1128 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) |
71 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | cdlemkoatnle 39710 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β ((πβπ) β π΄ β§ Β¬ (πβπ) β€ π)) |
72 | 71 | simpld 495 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β π΄) |
73 | 68, 69, 70, 72 | syl3anc 1371 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (πβπ) β π΄) |
74 | 42, 22 | jca 512 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β π β§ π· β π)) |
75 | 8, 9, 10, 11 | trlcocnvat 39583 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π· β π) β§ (π
βπ) β (π
βπ·)) β (π
β(π β β‘π·)) β π΄) |
76 | 18, 74, 43, 75 | syl3anc 1371 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π
β(π β β‘π·)) β π΄) |
77 | 6, 8 | hlatjcom 38226 |
. . . . . . 7
β’ ((πΎ β HL β§ (πβπ) β π΄ β§ (π
β(π β β‘π·)) β π΄) β ((πβπ) β¨ (π
β(π β β‘π·))) = ((π
β(π β β‘π·)) β¨ (πβπ))) |
78 | 16, 73, 76, 77 | syl3anc 1371 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ) β¨ (π
β(π β β‘π·))) = ((π
β(π β β‘π·)) β¨ (πβπ))) |
79 | 67, 78 | oveq12d 7423 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·)))) = (((πβπ) β¨ π) β§ ((π
β(π β β‘π·)) β¨ (πβπ)))) |
80 | 60, 79 | eqtrd 2772 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπ)βπ) = (((πβπ) β¨ π) β§ ((π
β(π β β‘π·)) β¨ (πβπ)))) |
81 | 58, 80 | oveq12d 7423 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (π β¨ ((πβπ)βπ)) = ((((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·)))) β¨ (((πβπ) β¨ π) β§ ((π
β(π β β‘π·)) β¨ (πβπ))))) |
82 | 57, 81 | eqtrd 2772 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β (((πβπ)βπ) β¨ π) = ((((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘π·)) β¨ (π
β(π β β‘π·)))) β¨ (((πβπ) β¨ π) β§ ((π
β(π β β‘π·)) β¨ (πβπ))))) |
83 | 15, 40, 82 | 3brtr4d 5179 |
1
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π
βπ·) β (π
βπΉ) β§ (π
βπΊ) β (π
βπ·) β§ (π
βπ) β (π
βπ·)))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ π)) |