Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β (πΎ β HL β§ π β π»)) |
2 | | eqid 2737 |
. . . 4
β’
(leβπΎ) =
(leβπΎ) |
3 | | eqid 2737 |
. . . 4
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
4 | | cdlemj.h |
. . . 4
β’ π» = (LHypβπΎ) |
5 | 2, 3, 4 | lhpexle2 38476 |
. . 3
β’ ((πΎ β HL β§ π β π») β βπ’ β (AtomsβπΎ)(π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) |
6 | 1, 5 | syl 17 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β βπ’ β (AtomsβπΎ)(π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) |
7 | | simpl1l 1225 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β πΎ β HL) |
8 | 7 | adantr 482 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ)))) β πΎ β HL) |
9 | | simpl1r 1226 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β π β π») |
10 | 9 | adantr 482 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ)))) β π β π») |
11 | | simprl 770 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ)))) β π’ β (AtomsβπΎ)) |
12 | | simprr1 1222 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ)))) β π’(leβπΎ)π) |
13 | | cdlemj.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
14 | | cdlemj.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
15 | | cdlemj.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
16 | 13, 2, 3, 4, 14, 15 | cdlemfnid 39030 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π’ β (AtomsβπΎ) β§ π’(leβπΎ)π)) β βπ β π ((π
βπ) = π’ β§ π β ( I βΎ π΅))) |
17 | 8, 10, 11, 12, 16 | syl22anc 838 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ)))) β βπ β π ((π
βπ) = π’ β§ π β ( I βΎ π΅))) |
18 | | simp1l 1198 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β ((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π))) |
19 | | simp1r 1199 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β β β ( I βΎ π΅)) |
20 | | simp3l 1202 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β π β π) |
21 | | simp3rr 1248 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β π β ( I βΎ π΅)) |
22 | | simp2r2 1277 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β π’ β (π
βπΉ)) |
23 | 22 | necomd 3000 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β (π
βπΉ) β π’) |
24 | | simp3rl 1247 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β (π
βπ) = π’) |
25 | 23, 24 | neeqtrrd 3019 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β (π
βπΉ) β (π
βπ)) |
26 | | simp2r3 1278 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β π’ β (π
ββ)) |
27 | 24, 26 | eqnetrd 3012 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β (π
βπ) β (π
ββ)) |
28 | | cdlemj.e |
. . . . . . . 8
β’ πΈ = ((TEndoβπΎ)βπ) |
29 | 13, 4, 14, 15, 28 | cdlemj2 39288 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ (β β ( I βΎ π΅) β§ π β π β§ π β ( I βΎ π΅)) β§ ((π
βπΉ) β (π
βπ) β§ (π
βπ) β (π
ββ))) β (πββ) = (πββ)) |
30 | 18, 19, 20, 21, 25, 27, 29 | syl132anc 1389 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ))) β§ (π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅)))) β (πββ) = (πββ)) |
31 | 30 | 3expia 1122 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ)))) β ((π β π β§ ((π
βπ) = π’ β§ π β ( I βΎ π΅))) β (πββ) = (πββ))) |
32 | 31 | expd 417 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ)))) β (π β π β (((π
βπ) = π’ β§ π β ( I βΎ π΅)) β (πββ) = (πββ)))) |
33 | 32 | rexlimdv 3151 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ)))) β (βπ β π ((π
βπ) = π’ β§ π β ( I βΎ π΅)) β (πββ) = (πββ))) |
34 | 17, 33 | mpd 15 |
. 2
β’
(((((πΎ β HL
β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β§ (π’ β (AtomsβπΎ) β§ (π’(leβπΎ)π β§ π’ β (π
βπΉ) β§ π’ β (π
ββ)))) β (πββ) = (πββ)) |
35 | 6, 34 | rexlimddv 3159 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β (πββ) = (πββ)) |