Step | Hyp | Ref
| Expression |
1 | | cdlemk5.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | cdlemk5.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | simp11l 1285 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΎ β HL) |
4 | 3 | hllatd 37876 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΎ β Lat) |
5 | | simp11 1204 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΎ β HL β§ π β π»)) |
6 | | simp12 1205 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΉ β π β§ πΉ β ( I βΎ π΅))) |
7 | | simp13 1206 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΊ β π β§ πΊ β ( I βΎ π΅))) |
8 | | simp21 1207 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β π β π) |
9 | | simp22 1208 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π β π΄ β§ Β¬ π β€ π)) |
10 | | simp23 1209 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΉ) = (π
βπ)) |
11 | | cdlemk5.j |
. . . . . . . . 9
β’ β¨ =
(joinβπΎ) |
12 | | cdlemk5.m |
. . . . . . . . 9
β’ β§ =
(meetβπΎ) |
13 | | cdlemk5.a |
. . . . . . . . 9
β’ π΄ = (AtomsβπΎ) |
14 | | cdlemk5.h |
. . . . . . . . 9
β’ π» = (LHypβπΎ) |
15 | | cdlemk5.t |
. . . . . . . . 9
β’ π = ((LTrnβπΎ)βπ) |
16 | | cdlemk5.r |
. . . . . . . . 9
β’ π
= ((trLβπΎ)βπ) |
17 | | cdlemk5.z |
. . . . . . . . 9
β’ π = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) |
18 | | cdlemk5.y |
. . . . . . . . 9
β’ π = ((π β¨ (π
βπ)) β§ (π β¨ (π
β(π β β‘π)))) |
19 | | cdlemk5.x |
. . . . . . . . 9
β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§βπ) = π)) |
20 | 1, 2, 11, 12, 13, 14, 15, 16, 17, 18, 19 | cdlemk35s 39450 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β β¦πΊ / πβ¦π β π) |
21 | 5, 6, 7, 8, 9, 10,
20 | syl132anc 1389 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β β¦πΊ / πβ¦π β π) |
22 | | simp31 1210 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΌ β π) |
23 | | simp32 1211 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΌ β ( I βΎ π΅)) |
24 | 22, 23 | jca 513 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΌ β π β§ πΌ β ( I βΎ π΅))) |
25 | 1, 2, 11, 12, 13, 14, 15, 16, 17, 18, 19 | cdlemk35s 39450 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β β¦πΌ / πβ¦π β π) |
26 | 5, 6, 24, 8, 9, 10, 25 | syl132anc 1389 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β β¦πΌ / πβ¦π β π) |
27 | 14, 15 | ltrnco 39232 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ β¦πΊ / πβ¦π β π β§ β¦πΌ / πβ¦π β π) β (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π) β π) |
28 | 5, 21, 26, 27 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π) β π) |
29 | | simp22l 1293 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β π β π΄) |
30 | 2, 13, 14, 15 | ltrnat 38653 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π) β π β§ π β π΄) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β π΄) |
31 | 5, 28, 29, 30 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β π΄) |
32 | 1, 13 | atbase 37801 |
. . . . 5
β’
(((β¦πΊ
/ πβ¦π β β¦πΌ / πβ¦π)βπ) β π΄ β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β π΅) |
33 | 31, 32 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β π΅) |
34 | 2, 13, 14, 15 | ltrnat 38653 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ β¦πΊ / πβ¦π β π β§ π β π΄) β (β¦πΊ / πβ¦πβπ) β π΄) |
35 | 5, 21, 29, 34 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦πΊ / πβ¦πβπ) β π΄) |
36 | 1, 13 | atbase 37801 |
. . . . . . 7
β’
((β¦πΊ /
πβ¦πβπ) β π΄ β (β¦πΊ / πβ¦πβπ) β π΅) |
37 | 35, 36 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦πΊ / πβ¦πβπ) β π΅) |
38 | 1, 14, 15, 16 | trlcl 38677 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ β¦πΌ / πβ¦π β π) β (π
ββ¦πΌ / πβ¦π) β π΅) |
39 | 5, 26, 38 | syl2anc 585 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
ββ¦πΌ / πβ¦π) β π΅) |
40 | 1, 11 | latjcl 18336 |
. . . . . 6
β’ ((πΎ β Lat β§
(β¦πΊ / πβ¦πβπ) β π΅ β§ (π
ββ¦πΌ / πβ¦π) β π΅) β ((β¦πΊ / πβ¦πβπ) β¨ (π
ββ¦πΌ / πβ¦π)) β π΅) |
41 | 4, 37, 39, 40 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦πβπ) β¨ (π
ββ¦πΌ / πβ¦π)) β π΅) |
42 | 2, 13, 14, 15 | ltrnat 38653 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ β¦πΌ / πβ¦π β π β§ π β π΄) β (β¦πΌ / πβ¦πβπ) β π΄) |
43 | 5, 26, 29, 42 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦πΌ / πβ¦πβπ) β π΄) |
44 | 1, 13 | atbase 37801 |
. . . . . . 7
β’
((β¦πΌ /
πβ¦πβπ) β π΄ β (β¦πΌ / πβ¦πβπ) β π΅) |
45 | 43, 44 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦πΌ / πβ¦πβπ) β π΅) |
46 | 1, 14, 15, 16 | trlcl 38677 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ β¦πΊ / πβ¦π β π) β (π
ββ¦πΊ / πβ¦π) β π΅) |
47 | 5, 21, 46 | syl2anc 585 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
ββ¦πΊ / πβ¦π) β π΅) |
48 | 1, 11 | latjcl 18336 |
. . . . . 6
β’ ((πΎ β Lat β§
(β¦πΌ / πβ¦πβπ) β π΅ β§ (π
ββ¦πΊ / πβ¦π) β π΅) β ((β¦πΌ / πβ¦πβπ) β¨ (π
ββ¦πΊ / πβ¦π)) β π΅) |
49 | 4, 45, 47, 48 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΌ / πβ¦πβπ) β¨ (π
ββ¦πΊ / πβ¦π)) β π΅) |
50 | 1, 12 | latmcl 18337 |
. . . . 5
β’ ((πΎ β Lat β§
((β¦πΊ / πβ¦πβπ) β¨ (π
ββ¦πΌ / πβ¦π)) β π΅ β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
ββ¦πΊ / πβ¦π)) β π΅) β (((β¦πΊ / πβ¦πβπ) β¨ (π
ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
ββ¦πΊ / πβ¦π))) β π΅) |
51 | 4, 41, 49, 50 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (((β¦πΊ / πβ¦πβπ) β¨ (π
ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
ββ¦πΊ / πβ¦π))) β π΅) |
52 | | simp11r 1286 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β π β π») |
53 | 1, 13, 14, 15, 16 | trlnidat 38686 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΌ β π β§ πΌ β ( I βΎ π΅)) β (π
βπΌ) β π΄) |
54 | 3, 52, 22, 23, 53 | syl211anc 1377 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΌ) β π΄) |
55 | 1, 11, 13 | hlatjcl 37879 |
. . . . . 6
β’ ((πΎ β HL β§
(β¦πΊ / πβ¦πβπ) β π΄ β§ (π
βπΌ) β π΄) β ((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β π΅) |
56 | 3, 35, 54, 55 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β π΅) |
57 | | simp13l 1289 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΊ β π) |
58 | | simp13r 1290 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΊ β ( I βΎ π΅)) |
59 | 1, 13, 14, 15, 16 | trlnidat 38686 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΊ β ( I βΎ π΅)) β (π
βπΊ) β π΄) |
60 | 3, 52, 57, 58, 59 | syl211anc 1377 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΊ) β π΄) |
61 | 1, 11, 13 | hlatjcl 37879 |
. . . . . 6
β’ ((πΎ β HL β§
(β¦πΌ / πβ¦πβπ) β π΄ β§ (π
βπΊ) β π΄) β ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)) β π΅) |
62 | 3, 43, 60, 61 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)) β π΅) |
63 | 1, 12 | latmcl 18337 |
. . . . 5
β’ ((πΎ β Lat β§
((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β π΅ β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)) β π΅) β (((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ))) β π΅) |
64 | 4, 56, 62, 63 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ))) β π΅) |
65 | 1, 2, 11, 12, 13, 14, 15, 16, 17, 18, 19 | cdlemk50 39465 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π
ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
ββ¦πΊ / πβ¦π)))) |
66 | 24, 65 | syld3an3 1410 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π
ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
ββ¦πΊ / πβ¦π)))) |
67 | 1, 2, 11, 12, 13, 14, 15, 16, 17, 18, 19 | cdlemk51 39466 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β (((β¦πΊ / πβ¦πβπ) β¨ (π
ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
ββ¦πΊ / πβ¦π))) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)))) |
68 | 24, 67 | syld3an3 1410 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (((β¦πΊ / πβ¦πβπ) β¨ (π
ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
ββ¦πΊ / πβ¦π))) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)))) |
69 | 1, 2, 4, 33, 51, 64, 66, 68 | lattrd 18343 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)))) |
70 | 1, 2, 11, 12, 13, 14, 15, 16, 17, 18, 19 | cdlemk47 39462 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦(πΊ β πΌ) / πβ¦πβπ) = (((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)))) |
71 | 69, 70 | breqtrrd 5137 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (β¦(πΊ β πΌ) / πβ¦πβπ)) |
72 | | hlatl 37872 |
. . . 4
β’ (πΎ β HL β πΎ β AtLat) |
73 | 3, 72 | syl 17 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΎ β AtLat) |
74 | 14, 15 | ltrnco 39232 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΌ β π) β (πΊ β πΌ) β π) |
75 | 5, 57, 22, 74 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΊ β πΌ) β π) |
76 | 57, 22 | jca 513 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΊ β π β§ πΌ β π)) |
77 | | simp33 1212 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΊ) β (π
βπΌ)) |
78 | 1, 14, 15, 16 | trlconid 39238 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ πΌ β π) β§ (π
βπΊ) β (π
βπΌ)) β (πΊ β πΌ) β ( I βΎ π΅)) |
79 | 5, 76, 77, 78 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΊ β πΌ) β ( I βΎ π΅)) |
80 | 75, 79 | jca 513 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((πΊ β πΌ) β π β§ (πΊ β πΌ) β ( I βΎ π΅))) |
81 | 1, 2, 11, 12, 13, 14, 15, 16, 17, 18, 19 | cdlemk35s 39450 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ ((πΊ β πΌ) β π β§ (πΊ β πΌ) β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β β¦(πΊ β πΌ) / πβ¦π β π) |
82 | 5, 6, 80, 8, 9, 10, 81 | syl132anc 1389 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β β¦(πΊ β πΌ) / πβ¦π β π) |
83 | 2, 13, 14, 15 | ltrnat 38653 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ β¦(πΊ β πΌ) / πβ¦π β π β§ π β π΄) β (β¦(πΊ β πΌ) / πβ¦πβπ) β π΄) |
84 | 5, 82, 29, 83 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β π΄) |
85 | 2, 13 | atcmp 37823 |
. . 3
β’ ((πΎ β AtLat β§
((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β π΄ β§ (β¦(πΊ β πΌ) / πβ¦πβπ) β π΄) β (((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (β¦(πΊ β πΌ) / πβ¦πβπ) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) = (β¦(πΊ β πΌ) / πβ¦πβπ))) |
86 | 73, 31, 84, 85 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (β¦(πΊ β πΌ) / πβ¦πβπ) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) = (β¦(πΊ β πΌ) / πβ¦πβπ))) |
87 | 71, 86 | mpbid 231 |
1
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) = (β¦(πΊ β πΌ) / πβ¦πβπ)) |