Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (πΎ β HL β§ π β π»)) |
2 | | simp21 1207 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β π β πΈ) |
3 | | simp23 1209 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β π β π) |
4 | | eqid 2733 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
5 | | cdleml1.h |
. . . . 5
β’ π» = (LHypβπΎ) |
6 | | cdleml1.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
7 | | cdleml1.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
8 | | cdleml1.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
9 | 4, 5, 6, 7, 8 | tendotp 39274 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (π
β(πβπ))(leβπΎ)(π
βπ)) |
10 | 1, 2, 3, 9 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π
β(πβπ))(leβπΎ)(π
βπ)) |
11 | | simp1l 1198 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β πΎ β HL) |
12 | | hlatl 37872 |
. . . . 5
β’ (πΎ β HL β πΎ β AtLat) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β πΎ β AtLat) |
14 | 5, 6, 8 | tendocl 39280 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
15 | 1, 2, 3, 14 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (πβπ) β π) |
16 | | simp32 1211 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (πβπ) β ( I βΎ π΅)) |
17 | | cdleml1.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
18 | | eqid 2733 |
. . . . . 6
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
19 | 17, 18, 5, 6, 7 | trlnidat 38686 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπ) β π β§ (πβπ) β ( I βΎ π΅)) β (π
β(πβπ)) β (AtomsβπΎ)) |
20 | 1, 15, 16, 19 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π
β(πβπ)) β (AtomsβπΎ)) |
21 | | simp31 1210 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β π β ( I βΎ π΅)) |
22 | 17, 18, 5, 6, 7 | trlnidat 38686 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β ( I βΎ π΅)) β (π
βπ) β (AtomsβπΎ)) |
23 | 1, 3, 21, 22 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π
βπ) β (AtomsβπΎ)) |
24 | 4, 18 | atcmp 37823 |
. . . 4
β’ ((πΎ β AtLat β§ (π
β(πβπ)) β (AtomsβπΎ) β§ (π
βπ) β (AtomsβπΎ)) β ((π
β(πβπ))(leβπΎ)(π
βπ) β (π
β(πβπ)) = (π
βπ))) |
25 | 13, 20, 23, 24 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β ((π
β(πβπ))(leβπΎ)(π
βπ) β (π
β(πβπ)) = (π
βπ))) |
26 | 10, 25 | mpbid 231 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π
β(πβπ)) = (π
βπ)) |
27 | | simp22 1208 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β π β πΈ) |
28 | 4, 5, 6, 7, 8 | tendotp 39274 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (π
β(πβπ))(leβπΎ)(π
βπ)) |
29 | 1, 27, 3, 28 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π
β(πβπ))(leβπΎ)(π
βπ)) |
30 | 5, 6, 8 | tendocl 39280 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
31 | 1, 27, 3, 30 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (πβπ) β π) |
32 | | simp33 1212 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (πβπ) β ( I βΎ π΅)) |
33 | 17, 18, 5, 6, 7 | trlnidat 38686 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπ) β π β§ (πβπ) β ( I βΎ π΅)) β (π
β(πβπ)) β (AtomsβπΎ)) |
34 | 1, 31, 32, 33 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π
β(πβπ)) β (AtomsβπΎ)) |
35 | 4, 18 | atcmp 37823 |
. . . 4
β’ ((πΎ β AtLat β§ (π
β(πβπ)) β (AtomsβπΎ) β§ (π
βπ) β (AtomsβπΎ)) β ((π
β(πβπ))(leβπΎ)(π
βπ) β (π
β(πβπ)) = (π
βπ))) |
36 | 13, 34, 23, 35 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β ((π
β(πβπ))(leβπΎ)(π
βπ) β (π
β(πβπ)) = (π
βπ))) |
37 | 29, 36 | mpbid 231 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π
β(πβπ)) = (π
βπ)) |
38 | 26, 37 | eqtr4d 2776 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π
β(πβπ)) = (π
β(πβπ))) |