Step | Hyp | Ref
| Expression |
1 | | coass 6221 |
. . 3
β’ ((πΊ β πΌ) β π) = (πΊ β (πΌ β π)) |
2 | | csbeq1 3862 |
. . 3
β’ (((πΊ β πΌ) β π) = (πΊ β (πΌ β π)) β β¦((πΊ β πΌ) β π) / πβ¦π = β¦(πΊ β (πΌ β π)) / πβ¦π) |
3 | 1, 2 | ax-mp 5 |
. 2
β’
β¦((πΊ
β πΌ) β π) / πβ¦π = β¦(πΊ β (πΌ β π)) / πβ¦π |
4 | | simp1 1137 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β ((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ))) |
5 | | simp21 1207 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π)) |
6 | | simp1l 1198 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (πΎ β HL β§ π β π»)) |
7 | | simp22 1208 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β πΊ β π) |
8 | | simp31l 1297 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β πΌ β π) |
9 | | cdlemk5.h |
. . . . 5
β’ π» = (LHypβπΎ) |
10 | | cdlemk5.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
11 | 9, 10 | ltrnco 39232 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΌ β π) β (πΊ β πΌ) β π) |
12 | 6, 7, 8, 11 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (πΊ β πΌ) β π) |
13 | | simp23 1209 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (π β π΄ β§ Β¬ π β€ π)) |
14 | | simp32 1211 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β π β π) |
15 | | simp333 1329 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (π
βπ) β (π
β(πΊ β πΌ))) |
16 | 15 | necomd 2996 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (π
β(πΊ β πΌ)) β (π
βπ)) |
17 | | cdlemk5.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
18 | | cdlemk5.l |
. . . 4
β’ β€ =
(leβπΎ) |
19 | | cdlemk5.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
20 | | cdlemk5.m |
. . . 4
β’ β§ =
(meetβπΎ) |
21 | | cdlemk5.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
22 | | cdlemk5.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
23 | | cdlemk5.z |
. . . 4
β’ π = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) |
24 | | cdlemk5.y |
. . . 4
β’ π = ((π β¨ (π
βπ)) β§ (π β¨ (π
β(π β β‘π)))) |
25 | | cdlemk5.x |
. . . 4
β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§βπ) = π)) |
26 | 17, 18, 19, 20, 21, 9, 10, 22, 23, 24, 25 | cdlemk53 39470 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (πΊ β πΌ) β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β(πΊ β πΌ)) β (π
βπ))) β β¦((πΊ β πΌ) β π) / πβ¦π = (β¦(πΊ β πΌ) / πβ¦π β β¦π / πβ¦π)) |
27 | 4, 5, 12, 13, 14, 16, 26 | syl132anc 1389 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β β¦((πΊ β πΌ) β π) / πβ¦π = (β¦(πΊ β πΌ) / πβ¦π β β¦π / πβ¦π)) |
28 | | simp2 1138 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π))) |
29 | 9, 10 | ltrnco 39232 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΌ β π β§ π β π) β (πΌ β π) β π) |
30 | 6, 8, 14, 29 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (πΌ β π) β π) |
31 | | simp31r 1298 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (π
βπΊ) = (π
βπΌ)) |
32 | | simp332 1328 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (π
βπ) β (π
βπΊ)) |
33 | 32, 31 | neeqtrd 3010 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (π
βπ) β (π
βπΌ)) |
34 | 33 | necomd 2996 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (π
βπΌ) β (π
βπ)) |
35 | | simp331 1327 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β π β ( I βΎ π΅)) |
36 | 17, 9, 10, 22 | trlcone 39241 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΌ β π β§ π β π) β§ ((π
βπΌ) β (π
βπ) β§ π β ( I βΎ π΅))) β (π
βπΌ) β (π
β(πΌ β π))) |
37 | 6, 8, 14, 34, 35, 36 | syl122anc 1380 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (π
βπΌ) β (π
β(πΌ β π))) |
38 | 31, 37 | eqnetrd 3008 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (π
βπΊ) β (π
β(πΌ β π))) |
39 | 17, 18, 19, 20, 21, 9, 10, 22, 23, 24, 25 | cdlemk53 39470 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π) β π β§ (π
βπΊ) β (π
β(πΌ β π)))) β β¦(πΊ β (πΌ β π)) / πβ¦π = (β¦πΊ / πβ¦π β β¦(πΌ β π) / πβ¦π)) |
40 | 4, 28, 30, 38, 39 | syl112anc 1375 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β β¦(πΊ β (πΌ β π)) / πβ¦π = (β¦πΊ / πβ¦π β β¦(πΌ β π) / πβ¦π)) |
41 | 17, 18, 19, 20, 21, 9, 10, 22, 23, 24, 25 | cdlemk53 39470 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΌ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
βπΌ) β (π
βπ))) β β¦(πΌ β π) / πβ¦π = (β¦πΌ / πβ¦π β β¦π / πβ¦π)) |
42 | 4, 5, 8, 13, 14, 34, 41 | syl132anc 1389 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β β¦(πΌ β π) / πβ¦π = (β¦πΌ / πβ¦π β β¦π / πβ¦π)) |
43 | 42 | coeq2d 5822 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (β¦πΊ / πβ¦π β β¦(πΌ β π) / πβ¦π) = (β¦πΊ / πβ¦π β (β¦πΌ / πβ¦π β β¦π / πβ¦π))) |
44 | | coass 6221 |
. . . 4
β’
((β¦πΊ /
πβ¦π β β¦πΌ / πβ¦π) β β¦π / πβ¦π) = (β¦πΊ / πβ¦π β (β¦πΌ / πβ¦π β β¦π / πβ¦π)) |
45 | 43, 44 | eqtr4di 2791 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (β¦πΊ / πβ¦π β β¦(πΌ β π) / πβ¦π) = ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π) β β¦π / πβ¦π)) |
46 | 40, 45 | eqtrd 2773 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β β¦(πΊ β (πΌ β π)) / πβ¦π = ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π) β β¦π / πβ¦π)) |
47 | 3, 27, 46 | 3eqtr3a 2797 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π
βπΊ) = (π
βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΊ) β§ (π
βπ) β (π
β(πΊ β πΌ))))) β (β¦(πΊ β πΌ) / πβ¦π β β¦π / πβ¦π) = ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π) β β¦π / πβ¦π)) |