Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (π½βπ) β ((π½βπ) β (πΌβπ))) β (πΎ β HL β§ π β π»)) |
2 | | cdlemn11a.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
3 | | cdlemn11a.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
4 | | cdlemn11a.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
5 | | cdlemn11a.p |
. . . . . . 7
β’ π = ((ocβπΎ)βπ) |
6 | 2, 3, 4, 5 | lhpocnel2 38532 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β (π β π΄ β§ Β¬ π β€ π)) |
7 | 6 | 3ad2ant1 1134 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (π½βπ) β ((π½βπ) β (πΌβπ))) β (π β π΄ β§ Β¬ π β€ π)) |
8 | | simp22 1208 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (π½βπ) β ((π½βπ) β (πΌβπ))) β (π β π΄ β§ Β¬ π β€ π)) |
9 | | cdlemn11a.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
10 | | cdlemn11a.g |
. . . . . 6
β’ πΊ = (β©β β π (ββπ) = π) |
11 | 2, 3, 4, 9, 10 | ltrniotacl 39092 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ β π) |
12 | 1, 7, 8, 11 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (π½βπ) β ((π½βπ) β (πΌβπ))) β πΊ β π) |
13 | | fvresi 7123 |
. . . 4
β’ (πΊ β π β (( I βΎ π)βπΊ) = πΊ) |
14 | 12, 13 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (π½βπ) β ((π½βπ) β (πΌβπ))) β (( I βΎ π)βπΊ) = πΊ) |
15 | 14 | eqcomd 2739 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (π½βπ) β ((π½βπ) β (πΌβπ))) β πΊ = (( I βΎ π)βπΊ)) |
16 | | cdlemn11a.e |
. . . 4
β’ πΈ = ((TEndoβπΎ)βπ) |
17 | 4, 9, 16 | tendoidcl 39282 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) |
18 | 17 | 3ad2ant1 1134 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (π½βπ) β ((π½βπ) β (πΌβπ))) β ( I βΎ π) β πΈ) |
19 | | cdlemn11a.J |
. . . 4
β’ π½ = ((DIsoCβπΎ)βπ) |
20 | | riotaex 7321 |
. . . . 5
β’
(β©β
β π (ββπ) = π) β V |
21 | 10, 20 | eqeltri 2830 |
. . . 4
β’ πΊ β V |
22 | 9 | fvexi 6860 |
. . . . 5
β’ π β V |
23 | | resiexg 7855 |
. . . . 5
β’ (π β V β ( I βΎ
π) β
V) |
24 | 22, 23 | ax-mp 5 |
. . . 4
β’ ( I
βΎ π) β
V |
25 | 2, 3, 4, 5, 9, 16,
19, 10, 21, 24 | dicopelval2 39694 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (β¨πΊ, ( I βΎ π)β© β (π½βπ) β (πΊ = (( I βΎ π)βπΊ) β§ ( I βΎ π) β πΈ))) |
26 | 1, 8, 25 | syl2anc 585 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (π½βπ) β ((π½βπ) β (πΌβπ))) β (β¨πΊ, ( I βΎ π)β© β (π½βπ) β (πΊ = (( I βΎ π)βπΊ) β§ ( I βΎ π) β πΈ))) |
27 | 15, 18, 26 | mpbir2and 712 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (π½βπ) β ((π½βπ) β (πΌβπ))) β β¨πΊ, ( I βΎ π)β© β (π½βπ)) |