Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. 2
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | ltrniotaval.l |
. 2
β’ β€ =
(leβπΎ) |
3 | | eqid 2736 |
. 2
β’
(joinβπΎ) =
(joinβπΎ) |
4 | | eqid 2736 |
. 2
β’
(meetβπΎ) =
(meetβπΎ) |
5 | | ltrniotaval.a |
. 2
β’ π΄ = (AtomsβπΎ) |
6 | | ltrniotaval.h |
. 2
β’ π» = (LHypβπΎ) |
7 | | eqid 2736 |
. 2
β’ ((π(joinβπΎ)π)(meetβπΎ)π) = ((π(joinβπΎ)π)(meetβπΎ)π) |
8 | | eqid 2736 |
. 2
β’ ((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))) = ((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))) |
9 | | eqid 2736 |
. 2
β’ ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))) = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))) |
10 | | eqid 2736 |
. 2
β’ (π₯ β (BaseβπΎ) β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β (BaseβπΎ)βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β (BaseβπΎ)βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯)) = (π₯ β (BaseβπΎ) β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β (BaseβπΎ)βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β (BaseβπΎ)βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯)) |
11 | | ltrniotaval.t |
. 2
β’ π = ((LTrnβπΎ)βπ) |
12 | | ltrniotaval.f |
. 2
β’ πΉ = (β©π β π (πβπ) = π) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cdlemg1finvtrlemN 38851 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β β‘πΉ β π) |