Step | Hyp | Ref
| Expression |
1 | | simp11 1204 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (πΎ β HL β§ π β π»)) |
2 | | simp12 1205 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (πΉ β π β§ πΉ β ( I βΎ π΅))) |
3 | | simp13l 1289 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β πΊ β π) |
4 | | simp31 1210 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β πΌ β π) |
5 | | cdlemk5.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
6 | | cdlemk5.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
7 | 5, 6 | ltrnco 39228 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΌ β π) β (πΊ β πΌ) β π) |
8 | 1, 3, 4, 7 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (πΊ β πΌ) β π) |
9 | | simp33 1212 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (πΊ β πΌ) β ( I βΎ π΅)) |
10 | 8, 9 | jca 513 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β ((πΊ β πΌ) β π β§ (πΊ β πΌ) β ( I βΎ π΅))) |
11 | | simp2 1138 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) |
12 | | simp32 1211 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β πΌ β ( I βΎ π΅)) |
13 | | cdlemk5.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
14 | | cdlemk5.l |
. . . 4
β’ β€ =
(leβπΎ) |
15 | | cdlemk5.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
16 | | cdlemk5.m |
. . . 4
β’ β§ =
(meetβπΎ) |
17 | | cdlemk5.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
18 | | cdlemk5.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
19 | | cdlemk5.z |
. . . 4
β’ π = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) |
20 | | cdlemk5.y |
. . . 4
β’ π = ((π β¨ (π
βπ)) β§ (π β¨ (π
β(π β β‘π)))) |
21 | | cdlemk5.x |
. . . 4
β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§βπ) = π)) |
22 | 13, 14, 15, 16, 17, 5, 6, 18, 19, 20, 21 | cdlemk11t 39455 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ ((πΊ β πΌ) β π β§ (πΊ β πΌ) β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π
β(πΌ β β‘(πΊ β πΌ))))) |
23 | 1, 2, 10, 11, 4, 12, 22 | syl312anc 1392 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π
β(πΌ β β‘(πΊ β πΌ))))) |
24 | | cnvco 5842 |
. . . . . . . 8
β’ β‘(πΊ β πΌ) = (β‘πΌ β β‘πΊ) |
25 | 24 | coeq2i 5817 |
. . . . . . 7
β’ (πΌ β β‘(πΊ β πΌ)) = (πΌ β (β‘πΌ β β‘πΊ)) |
26 | | coass 6218 |
. . . . . . 7
β’ ((πΌ β β‘πΌ) β β‘πΊ) = (πΌ β (β‘πΌ β β‘πΊ)) |
27 | 25, 26 | eqtr4i 2764 |
. . . . . 6
β’ (πΌ β β‘(πΊ β πΌ)) = ((πΌ β β‘πΌ) β β‘πΊ) |
28 | 13, 5, 6 | ltrn1o 38633 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΌ β π) β πΌ:π΅β1-1-ontoβπ΅) |
29 | 1, 4, 28 | syl2anc 585 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β πΌ:π΅β1-1-ontoβπ΅) |
30 | | f1ococnv2 6812 |
. . . . . . . . 9
β’ (πΌ:π΅β1-1-ontoβπ΅ β (πΌ β β‘πΌ) = ( I βΎ π΅)) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (πΌ β β‘πΌ) = ( I βΎ π΅)) |
32 | 31 | coeq1d 5818 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β ((πΌ β β‘πΌ) β β‘πΊ) = (( I βΎ π΅) β β‘πΊ)) |
33 | 13, 5, 6 | ltrn1o 38633 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β πΊ:π΅β1-1-ontoβπ΅) |
34 | 1, 3, 33 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β πΊ:π΅β1-1-ontoβπ΅) |
35 | | f1ocnv 6797 |
. . . . . . . 8
β’ (πΊ:π΅β1-1-ontoβπ΅ β β‘πΊ:π΅β1-1-ontoβπ΅) |
36 | | f1of 6785 |
. . . . . . . 8
β’ (β‘πΊ:π΅β1-1-ontoβπ΅ β β‘πΊ:π΅βΆπ΅) |
37 | | fcoi2 6718 |
. . . . . . . 8
β’ (β‘πΊ:π΅βΆπ΅ β (( I βΎ π΅) β β‘πΊ) = β‘πΊ) |
38 | 34, 35, 36, 37 | 4syl 19 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (( I βΎ π΅) β β‘πΊ) = β‘πΊ) |
39 | 32, 38 | eqtrd 2773 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β ((πΌ β β‘πΌ) β β‘πΊ) = β‘πΊ) |
40 | 27, 39 | eqtrid 2785 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (πΌ β β‘(πΊ β πΌ)) = β‘πΊ) |
41 | 40 | fveq2d 6847 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (π
β(πΌ β β‘(πΊ β πΌ))) = (π
ββ‘πΊ)) |
42 | 5, 6, 18 | trlcnv 38674 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
ββ‘πΊ) = (π
βπΊ)) |
43 | 1, 3, 42 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (π
ββ‘πΊ) = (π
βπΊ)) |
44 | 41, 43 | eqtrd 2773 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (π
β(πΌ β β‘(πΊ β πΌ))) = (π
βπΊ)) |
45 | 44 | oveq2d 7374 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β ((β¦πΌ / πβ¦πβπ) β¨ (π
β(πΌ β β‘(πΊ β πΌ)))) = ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ))) |
46 | 23, 45 | breqtrd 5132 |
1
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ))) |