Step | Hyp | Ref
| Expression |
1 | | idltrn.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | idltrn.h |
. . 3
β’ π» = (LHypβπΎ) |
3 | | eqid 2731 |
. . 3
β’
((LDilβπΎ)βπ) = ((LDilβπΎ)βπ) |
4 | 1, 2, 3 | idldil 38683 |
. 2
β’ ((πΎ β HL β§ π β π») β ( I βΎ π΅) β ((LDilβπΎ)βπ)) |
5 | | simpll 765 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (πΎ β HL β§ π β π»)) |
6 | | simplrr 776 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β π β (AtomsβπΎ)) |
7 | | simprr 771 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β Β¬ π(leβπΎ)π) |
8 | | eqid 2731 |
. . . . . . 7
β’
(leβπΎ) =
(leβπΎ) |
9 | | eqid 2731 |
. . . . . . 7
β’
(meetβπΎ) =
(meetβπΎ) |
10 | | eqid 2731 |
. . . . . . 7
β’
(0.βπΎ) =
(0.βπΎ) |
11 | | eqid 2731 |
. . . . . . 7
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
12 | 8, 9, 10, 11, 2 | lhpmat 38599 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (π(meetβπΎ)π) = (0.βπΎ)) |
13 | 5, 6, 7, 12 | syl12anc 835 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (π(meetβπΎ)π) = (0.βπΎ)) |
14 | 1, 11 | atbase 37857 |
. . . . . . . . 9
β’ (π β (AtomsβπΎ) β π β π΅) |
15 | | fvresi 7139 |
. . . . . . . . 9
β’ (π β π΅ β (( I βΎ π΅)βπ) = π) |
16 | 6, 14, 15 | 3syl 18 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (( I βΎ π΅)βπ) = π) |
17 | 16 | oveq2d 7393 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (π(joinβπΎ)(( I βΎ π΅)βπ)) = (π(joinβπΎ)π)) |
18 | | simplll 773 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β πΎ β HL) |
19 | | eqid 2731 |
. . . . . . . . 9
β’
(joinβπΎ) =
(joinβπΎ) |
20 | 19, 11 | hlatjidm 37937 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β (π(joinβπΎ)π) = π) |
21 | 18, 6, 20 | syl2anc 584 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (π(joinβπΎ)π) = π) |
22 | 17, 21 | eqtrd 2771 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (π(joinβπΎ)(( I βΎ π΅)βπ)) = π) |
23 | 22 | oveq1d 7392 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π) = (π(meetβπΎ)π)) |
24 | | simplrl 775 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β π β (AtomsβπΎ)) |
25 | 1, 11 | atbase 37857 |
. . . . . . . . . 10
β’ (π β (AtomsβπΎ) β π β π΅) |
26 | | fvresi 7139 |
. . . . . . . . . 10
β’ (π β π΅ β (( I βΎ π΅)βπ) = π) |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (( I βΎ π΅)βπ) = π) |
28 | 27 | oveq2d 7393 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (π(joinβπΎ)(( I βΎ π΅)βπ)) = (π(joinβπΎ)π)) |
29 | 19, 11 | hlatjidm 37937 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β (π(joinβπΎ)π) = π) |
30 | 18, 24, 29 | syl2anc 584 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (π(joinβπΎ)π) = π) |
31 | 28, 30 | eqtrd 2771 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (π(joinβπΎ)(( I βΎ π΅)βπ)) = π) |
32 | 31 | oveq1d 7392 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π) = (π(meetβπΎ)π)) |
33 | | simprl 769 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β Β¬ π(leβπΎ)π) |
34 | 8, 9, 10, 11, 2 | lhpmat 38599 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (π(meetβπΎ)π) = (0.βπΎ)) |
35 | 5, 24, 33, 34 | syl12anc 835 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (π(meetβπΎ)π) = (0.βπΎ)) |
36 | 32, 35 | eqtrd 2771 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π) = (0.βπΎ)) |
37 | 13, 23, 36 | 3eqtr4rd 2782 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π) = ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π)) |
38 | 37 | ex 413 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β ((Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π) β ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π) = ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π))) |
39 | 38 | ralrimivva 3199 |
. 2
β’ ((πΎ β HL β§ π β π») β βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)((Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π) β ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π) = ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π))) |
40 | | idltrn.t |
. . 3
β’ π = ((LTrnβπΎ)βπ) |
41 | 8, 19, 9, 11, 2, 3,
40 | isltrn 38688 |
. 2
β’ ((πΎ β HL β§ π β π») β (( I βΎ π΅) β π β (( I βΎ π΅) β ((LDilβπΎ)βπ) β§ βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)((Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π) β ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π) = ((π(joinβπΎ)(( I βΎ π΅)βπ))(meetβπΎ)π))))) |
42 | 4, 39, 41 | mpbir2and 711 |
1
β’ ((πΎ β HL β§ π β π») β ( I βΎ π΅) β π) |