Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’
(leβπΎ) =
(leβπΎ) |
2 | | eqid 2737 |
. . . 4
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
3 | | cdlemg44.h |
. . . 4
β’ π» = (LHypβπΎ) |
4 | 1, 2, 3 | lhpexnle 38498 |
. . 3
β’ ((πΎ β HL β§ π β π») β βπ β (AtomsβπΎ) Β¬ π(leβπΎ)π) |
5 | 4 | 3ad2ant1 1134 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β βπ β (AtomsβπΎ) Β¬ π(leβπΎ)π) |
6 | | simp11 1204 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β (πΎ β HL β§ π β π»)) |
7 | | simp12l 1287 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β πΉ β π) |
8 | | simp12r 1288 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β πΊ β π) |
9 | | cdlemg44.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
10 | 3, 9 | ltrnco 39211 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (πΉ β πΊ) β π) |
11 | 6, 7, 8, 10 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β (πΉ β πΊ) β π) |
12 | 3, 9 | ltrnco 39211 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΉ β π) β (πΊ β πΉ) β π) |
13 | 6, 8, 7, 12 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β (πΊ β πΉ) β π) |
14 | | 3simpc 1151 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) |
15 | | simp13 1206 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β (π
βπΉ) β (π
βπΊ)) |
16 | | cdlemg44.r |
. . . . . . 7
β’ π
= ((trLβπΎ)βπ) |
17 | 3, 9, 16, 1, 2 | cdlemg44b 39224 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β§ (π
βπΉ) β (π
βπΊ)) β (πΉβ(πΊβπ)) = (πΊβ(πΉβπ))) |
18 | 6, 7, 8, 14, 15, 17 | syl131anc 1384 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β (πΉβ(πΊβπ)) = (πΊβ(πΉβπ))) |
19 | | simp12 1205 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β (πΉ β π β§ πΊ β π)) |
20 | | simp2 1138 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β π β (AtomsβπΎ)) |
21 | 1, 2, 3, 9 | ltrncoval 38637 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β (AtomsβπΎ)) β ((πΉ β πΊ)βπ) = (πΉβ(πΊβπ))) |
22 | 6, 19, 20, 21 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β ((πΉ β πΊ)βπ) = (πΉβ(πΊβπ))) |
23 | 1, 2, 3, 9 | ltrncoval 38637 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ πΉ β π) β§ π β (AtomsβπΎ)) β ((πΊ β πΉ)βπ) = (πΊβ(πΉβπ))) |
24 | 6, 8, 7, 20, 23 | syl121anc 1376 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β ((πΊ β πΉ)βπ) = (πΊβ(πΉβπ))) |
25 | 18, 22, 24 | 3eqtr4d 2787 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β ((πΉ β πΊ)βπ) = ((πΊ β πΉ)βπ)) |
26 | 1, 2, 3, 9 | cdlemd 38699 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β πΊ) β π β§ (πΊ β πΉ) β π) β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β§ ((πΉ β πΊ)βπ) = ((πΊ β πΉ)βπ)) β (πΉ β πΊ) = (πΊ β πΉ)) |
27 | 6, 11, 13, 14, 25, 26 | syl311anc 1385 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β§ π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π) β (πΉ β πΊ) = (πΊ β πΉ)) |
28 | 27 | rexlimdv3a 3157 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β (βπ β (AtomsβπΎ) Β¬ π(leβπΎ)π β (πΉ β πΊ) = (πΊ β πΉ))) |
29 | 5, 28 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β (πΉ β πΊ) = (πΊ β πΉ)) |