Step | Hyp | Ref
| Expression |
1 | | simp11 1203 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΎ β HL β§ π β π»)) |
2 | | simp23 1208 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
βπΉ) = (π
βπ)) |
3 | | simp12l 1286 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΉ β π) |
4 | | simp3l 1201 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β π) |
5 | | simp21 1206 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β π) |
6 | | simp3r2 1282 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
βπ) β (π
βπΉ)) |
7 | | simp12r 1287 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΉ β ( I βΎ π΅)) |
8 | | simp3r1 1281 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β ( I βΎ π΅)) |
9 | 7, 8 | jca 512 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅))) |
10 | | simp22 1207 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π β π΄ β§ Β¬ π β€ π)) |
11 | | cdlemk5.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
12 | | cdlemk5.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
13 | | cdlemk5.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
14 | | cdlemk5.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
15 | | cdlemk5.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
16 | | cdlemk5.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
17 | | cdlemk5.t |
. . . . . . 7
β’ π = ((LTrnβπΎ)βπ) |
18 | | cdlemk5.r |
. . . . . . 7
β’ π
= ((trLβπΎ)βπ) |
19 | | cdlemk5b.s |
. . . . . . 7
β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))))) |
20 | 11, 12, 13, 14, 15, 16, 17, 18, 19 | cdlemk30 39753 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β π β§ π β π β§ π β π) β§ ((π
βπ) β (π
βπΉ) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπ)βπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ))))) |
21 | 1, 2, 3, 4, 5, 6, 9, 10, 20 | syl233anc 1399 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((πβπ)βπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ))))) |
22 | | cdlemk5.z |
. . . . 5
β’ π = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) |
23 | 21, 22 | eqtr4di 2790 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((πβπ)βπ) = π) |
24 | 23 | oveq1d 7420 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (((πβπ)βπ) β¨ (π
β(πΊ β β‘π))) = (π β¨ (π
β(πΊ β β‘π)))) |
25 | 24 | oveq2d 7421 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((π β¨ (π
βπΊ)) β§ (((πβπ)βπ) β¨ (π
β(πΊ β β‘π)))) = ((π β¨ (π
βπΊ)) β§ (π β¨ (π
β(πΊ β β‘π))))) |
26 | 3, 4, 5 | 3jca 1128 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΉ β π β§ π β π β§ π β π)) |
27 | | simp13l 1288 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΊ β π) |
28 | | simp3r3 1283 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
βπ) β (π
βπΊ)) |
29 | 6, 28 | jca 512 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ))) |
30 | | simp13r 1289 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΊ β ( I βΎ π΅)) |
31 | 7, 8, 30 | 3jca 1128 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅))) |
32 | | cdlemk5b.u1 |
. . . 4
β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘π)))))) |
33 | 11, 12, 13, 14, 15, 16, 17, 18, 19, 32 | cdlemk31 39755 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ π β π β§ π β π) β§ πΊ β π) β§ (((π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πππΊ)βπ) = ((π β¨ (π
βπΊ)) β§ (((πβπ)βπ) β¨ (π
β(πΊ β β‘π))))) |
34 | 1, 2, 26, 27, 29, 31, 10, 33 | syl223anc 1396 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((πππΊ)βπ) = ((π β¨ (π
βπΊ)) β§ (((πβπ)βπ) β¨ (π
β(πΊ β β‘π))))) |
35 | | cdlemk5.y |
. . . 4
β’ π = ((π β¨ (π
βπ)) β§ (π β¨ (π
β(π β β‘π)))) |
36 | 35 | cdlemk41 39779 |
. . 3
β’ (πΊ β π β β¦πΊ / πβ¦π = ((π β¨ (π
βπΊ)) β§ (π β¨ (π
β(πΊ β β‘π))))) |
37 | 27, 36 | syl 17 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β β¦πΊ / πβ¦π = ((π β¨ (π
βπΊ)) β§ (π β¨ (π
β(πΊ β β‘π))))) |
38 | 25, 34, 37 | 3eqtr4rd 2783 |
1
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β β¦πΊ / πβ¦π = ((πππΊ)βπ)) |