Step | Hyp | Ref
| Expression |
1 | | simp111 1301 |
. . . 4
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β πΎ β HL) |
2 | | simp112 1302 |
. . . 4
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β π β π») |
3 | | simp12 1203 |
. . . 4
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β (π β π΄ β§ Β¬ π β€ π)) |
4 | | simp13 1204 |
. . . 4
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β (π β π΄ β§ Β¬ π β€ π)) |
5 | | simp113 1303 |
. . . 4
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β πΉ β π) |
6 | | simp2l 1198 |
. . . 4
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β (πΉβπ) = π) |
7 | | cdlemg2id.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
8 | | cdlemg2id.l |
. . . . 5
β’ β€ =
(leβπΎ) |
9 | | eqid 2731 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
10 | | eqid 2731 |
. . . . 5
β’
(meetβπΎ) =
(meetβπΎ) |
11 | | cdlemg2id.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
12 | | cdlemg2id.h |
. . . . 5
β’ π» = (LHypβπΎ) |
13 | | cdlemg2id.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
14 | | eqid 2731 |
. . . . 5
β’ ((π(joinβπΎ)π)(meetβπΎ)π) = ((π(joinβπΎ)π)(meetβπΎ)π) |
15 | | eqid 2731 |
. . . . 5
β’ ((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))) = ((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))) |
16 | | eqid 2731 |
. . . . 5
β’ ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))) = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))) |
17 | | eqid 2731 |
. . . . 5
β’ (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯)) = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯)) |
18 | 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 | cdlemg2dN 39765 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π)) β πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯))) |
19 | 1, 2, 3, 4, 5, 6, 18 | syl222anc 1385 |
. . 3
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯))) |
20 | 19 | fveq1d 6894 |
. 2
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β (πΉβπ) = ((π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯))βπ)) |
21 | | simp2r 1199 |
. . 3
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β π β π΅) |
22 | | simp3 1137 |
. . 3
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β π = π) |
23 | 17 | cdleme31id 39569 |
. . 3
β’ ((π β π΅ β§ π = π) β ((π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯))βπ) = π) |
24 | 21, 22, 23 | syl2anc 583 |
. 2
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β ((π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯))βπ) = π) |
25 | 20, 24 | eqtrd 2771 |
1
β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β (πΉβπ) = π) |