Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | eqid 2733 |
. . 3
β’
(joinβπΎ) =
(joinβπΎ) |
3 | | eqid 2733 |
. . 3
β’
(meetβπΎ) =
(meetβπΎ) |
4 | | eqid 2733 |
. . 3
β’
(ocβπΎ) =
(ocβπΎ) |
5 | | eqid 2733 |
. . 3
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
6 | | cdlemk7.h |
. . 3
β’ π» = (LHypβπΎ) |
7 | | cdlemk7.t |
. . 3
β’ π = ((LTrnβπΎ)βπ) |
8 | | cdlemk7.r |
. . 3
β’ π
= ((trLβπΎ)βπ) |
9 | | eqid 2733 |
. . 3
β’
((ocβπΎ)βπ) = ((ocβπΎ)βπ) |
10 | | eqid 2733 |
. . 3
β’
((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ)))) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ)))) |
11 | | eqid 2733 |
. . 3
β’
((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))) |
12 | | eqid 2733 |
. . 3
β’
(β©π§
β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))))) = (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))))) |
13 | | eqid 2733 |
. . 3
β’ (π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))))))) = (π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))))))) |
14 | | cdlemk7.e |
. . 3
β’ πΈ = ((TEndoβπΎ)βπ) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | cdlemk56w 39486 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π
βπΉ) = (π
βπ)) β ((π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))))))) β πΈ β§ ((π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π))))))))βπΉ) = π)) |
16 | | fveq1 6845 |
. . . 4
β’ (π’ = (π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))))))) β (π’βπΉ) = ((π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π))))))))βπΉ)) |
17 | 16 | eqeq1d 2735 |
. . 3
β’ (π’ = (π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))))))) β ((π’βπΉ) = π β ((π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π))))))))βπΉ) = π)) |
18 | 17 | rspcev 3583 |
. 2
β’ (((π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π)))))))) β πΈ β§ ((π β π β¦ if(πΉ = π, π, (β©π§ β π βπ β π ((π β ( I βΎ (BaseβπΎ)) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(π
βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(π
β(π β β‘πΉ))))(joinβπΎ)(π
β(π β β‘π))))))))βπΉ) = π) β βπ’ β πΈ (π’βπΉ) = π) |
19 | 15, 18 | syl 17 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π
βπΉ) = (π
βπ)) β βπ’ β πΈ (π’βπΉ) = π) |