Step | Hyp | Ref
| Expression |
1 | | simp11l 1285 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β πΎ β HL) |
2 | | simp22l 1293 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β π β π΄) |
3 | | simp11 1204 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (πΎ β HL β§ π β π»)) |
4 | | simp13 1206 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β πΊ β π) |
5 | | cdlemk.l |
. . . 4
β’ β€ =
(leβπΎ) |
6 | | cdlemk.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
7 | | cdlemk.h |
. . . 4
β’ π» = (LHypβπΎ) |
8 | | cdlemk.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
9 | 5, 6, 7, 8 | ltrnat 38949 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
10 | 3, 4, 2, 9 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (πΊβπ) β π΄) |
11 | | simp12 1205 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β πΉ β π) |
12 | | simp21r 1292 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β π β π) |
13 | 3, 11, 12 | 3jca 1129 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π)) |
14 | | simp21l 1291 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β π β π) |
15 | | simp22 1208 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π β π΄ β§ Β¬ π β€ π)) |
16 | | simp23 1209 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
βπΉ) = (π
βπ)) |
17 | 14, 15, 16 | 3jca 1129 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) |
18 | | simp311 1321 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β πΉ β ( I βΎ π΅)) |
19 | | simp313 1323 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β π β ( I βΎ π΅)) |
20 | | simp32r 1300 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
βπ) β (π
βπΉ)) |
21 | | cdlemk.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
22 | | cdlemk.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
23 | | cdlemk.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
24 | | cdlemk.m |
. . . 4
β’ β§ =
(meetβπΎ) |
25 | | cdlemk.s |
. . . 4
β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))))) |
26 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksat 39655 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ))) β ((πβπ)βπ) β π΄) |
27 | 13, 17, 18, 19, 20, 26 | syl113anc 1383 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πβπ)βπ) β π΄) |
28 | | simp33 1212 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
βπΊ) β (π
βπ)) |
29 | 28 | necomd 2997 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
βπ) β (π
βπΊ)) |
30 | 6, 7, 8, 23 | trlcocnvat 39533 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ πΊ β π) β§ (π
βπ) β (π
βπΊ)) β (π
β(π β β‘πΊ)) β π΄) |
31 | 3, 12, 4, 29, 30 | syl121anc 1376 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
β(π β β‘πΊ)) β π΄) |
32 | | simp1 1137 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π)) |
33 | | simp312 1322 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β πΊ β ( I βΎ π΅)) |
34 | | simp32l 1299 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
βπΊ) β (π
βπΉ)) |
35 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksat 39655 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΉ))) β ((πβπΊ)βπ) β π΄) |
36 | 32, 17, 18, 33, 34, 35 | syl113anc 1383 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πβπΊ)βπ) β π΄) |
37 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksv2 39656 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΉ))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘πΉ))))) |
38 | 32, 17, 18, 33, 34, 37 | syl113anc 1383 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘πΉ))))) |
39 | 1 | hllatd 38172 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β πΎ β Lat) |
40 | 21, 6, 7, 8, 23 | trlnidat 38982 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΊ β ( I βΎ π΅)) β (π
βπΊ) β π΄) |
41 | 3, 4, 33, 40 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
βπΊ) β π΄) |
42 | 21, 22, 6 | hlatjcl 38175 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπΊ) β π΄) β (π β¨ (π
βπΊ)) β π΅) |
43 | 1, 2, 41, 42 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π β¨ (π
βπΊ)) β π΅) |
44 | 5, 6, 7, 8 | ltrnat 38949 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π΄) β (πβπ) β π΄) |
45 | 3, 14, 2, 44 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (πβπ) β π΄) |
46 | 6, 7, 8, 23 | trlcocnvat 39533 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ πΉ β π) β§ (π
βπΊ) β (π
βπΉ)) β (π
β(πΊ β β‘πΉ)) β π΄) |
47 | 3, 4, 11, 34, 46 | syl121anc 1376 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
β(πΊ β β‘πΉ)) β π΄) |
48 | 21, 22, 6 | hlatjcl 38175 |
. . . . . 6
β’ ((πΎ β HL β§ (πβπ) β π΄ β§ (π
β(πΊ β β‘πΉ)) β π΄) β ((πβπ) β¨ (π
β(πΊ β β‘πΉ))) β π΅) |
49 | 1, 45, 47, 48 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πβπ) β¨ (π
β(πΊ β β‘πΉ))) β π΅) |
50 | 21, 5, 24 | latmle1 18413 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ (π
βπΊ)) β π΅ β§ ((πβπ) β¨ (π
β(πΊ β β‘πΉ))) β π΅) β ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘πΉ)))) β€ (π β¨ (π
βπΊ))) |
51 | 39, 43, 49, 50 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘πΉ)))) β€ (π β¨ (π
βπΊ))) |
52 | 38, 51 | eqbrtrd 5169 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πβπΊ)βπ) β€ (π β¨ (π
βπΊ))) |
53 | 5, 22, 6, 7, 8, 23 | trljat1 38975 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
βπΊ)) = (π β¨ (πΊβπ))) |
54 | 3, 4, 15, 53 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π β¨ (π
βπΊ)) = (π β¨ (πΊβπ))) |
55 | 52, 54 | breqtrd 5173 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πβπΊ)βπ) β€ (π β¨ (πΊβπ))) |
56 | | simp2 1138 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) |
57 | | simp31 1210 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅))) |
58 | | eqid 2733 |
. . . 4
β’ (((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘πΉ)) β¨ (π
β(π β β‘πΉ)))) = (((πΊβπ) β¨ (πβπ)) β§ ((π
β(πΊ β β‘πΉ)) β¨ (π
β(π β β‘πΉ)))) |
59 | 21, 5, 22, 6, 7, 8,
23, 24, 25, 58 | cdlemk11 39658 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ (π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
60 | 32, 56, 57, 34, 20, 59 | syl113anc 1383 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
61 | 5, 22, 6 | hlatlej2 38184 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπΊ) β π΄) β (π
βπΊ) β€ (π β¨ (π
βπΊ))) |
62 | 1, 2, 41, 61 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
βπΊ) β€ (π β¨ (π
βπΊ))) |
63 | 62, 54 | breqtrd 5173 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
βπΊ) β€ (π β¨ (πΊβπ))) |
64 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksel 39654 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ))) β (πβπ) β π) |
65 | 13, 17, 18, 19, 20, 64 | syl113anc 1383 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (πβπ) β π) |
66 | 5, 6, 7, 8 | ltrnel 38948 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπ) β π β§ (π β π΄ β§ Β¬ π β€ π)) β (((πβπ)βπ) β π΄ β§ Β¬ ((πβπ)βπ) β€ π)) |
67 | 3, 65, 15, 66 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (((πβπ)βπ) β π΄ β§ Β¬ ((πβπ)βπ) β€ π)) |
68 | 7, 8 | ltrncnv 38955 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β β‘πΊ β π) |
69 | 3, 4, 68 | syl2anc 585 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β β‘πΊ β π) |
70 | 7, 8, 23 | trlcnv 38974 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
ββ‘πΊ) = (π
βπΊ)) |
71 | 3, 4, 70 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
ββ‘πΊ) = (π
βπΊ)) |
72 | 71, 28 | eqnetrd 3009 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
ββ‘πΊ) β (π
βπ)) |
73 | 21, 7, 8, 23 | trlcone 39537 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (β‘πΊ β π β§ π β π) β§ ((π
ββ‘πΊ) β (π
βπ) β§ π β ( I βΎ π΅))) β (π
ββ‘πΊ) β (π
β(β‘πΊ β π))) |
74 | 3, 69, 12, 72, 19, 73 | syl122anc 1380 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
ββ‘πΊ) β (π
β(β‘πΊ β π))) |
75 | 74 | necomd 2997 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
β(β‘πΊ β π)) β (π
ββ‘πΊ)) |
76 | 7, 8 | ltrncom 39547 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ β‘πΊ β π β§ π β π) β (β‘πΊ β π) = (π β β‘πΊ)) |
77 | 3, 69, 12, 76 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (β‘πΊ β π) = (π β β‘πΊ)) |
78 | 77 | fveq2d 6892 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
β(β‘πΊ β π)) = (π
β(π β β‘πΊ))) |
79 | 75, 78, 71 | 3netr3d 3018 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
β(π β β‘πΊ)) β (π
βπΊ)) |
80 | 7, 8 | ltrnco 39528 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π β§ β‘πΊ β π) β (π β β‘πΊ) β π) |
81 | 3, 12, 69, 80 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π β β‘πΊ) β π) |
82 | 5, 7, 8, 23 | trlle 38993 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β β‘πΊ) β π) β (π
β(π β β‘πΊ)) β€ π) |
83 | 3, 81, 82 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
β(π β β‘πΊ)) β€ π) |
84 | 5, 7, 8, 23 | trlle 38993 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β€ π) |
85 | 3, 4, 84 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π
βπΊ) β€ π) |
86 | 5, 22, 6, 7 | lhp2atnle 38842 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (((πβπ)βπ) β π΄ β§ Β¬ ((πβπ)βπ) β€ π) β§ (π
β(π β β‘πΊ)) β (π
βπΊ)) β§ ((π
β(π β β‘πΊ)) β π΄ β§ (π
β(π β β‘πΊ)) β€ π) β§ ((π
βπΊ) β π΄ β§ (π
βπΊ) β€ π)) β Β¬ (π
βπΊ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
87 | 3, 67, 79, 31, 83, 41, 85, 86 | syl322anc 1399 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β Β¬ (π
βπΊ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
88 | | nbrne1 5166 |
. . 3
β’ (((π
βπΊ) β€ (π β¨ (πΊβπ)) β§ Β¬ (π
βπΊ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) β (π β¨ (πΊβπ)) β (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
89 | 63, 87, 88 | syl2anc 585 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β (π β¨ (πΊβπ)) β (((πβπ)βπ) β¨ (π
β(π β β‘πΊ)))) |
90 | 5, 22, 24, 6 | 2atm 38336 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ (πΊβπ) β π΄) β§ (((πβπ)βπ) β π΄ β§ (π
β(π β β‘πΊ)) β π΄ β§ ((πβπΊ)βπ) β π΄) β§ (((πβπΊ)βπ) β€ (π β¨ (πΊβπ)) β§ ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))) β§ (π β¨ (πΊβπ)) β (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))))) |
91 | 1, 2, 10, 27, 31, 36, 55, 60, 89, 90 | syl333anc 1403 |
1
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π
βπΊ) β (π
βπΉ) β§ (π
βπ) β (π
βπΉ)) β§ (π
βπΊ) β (π
βπ))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘πΊ))))) |