Step | Hyp | Ref
| Expression |
1 | | cdlemefrs27.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | cdlemefrs27.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | cdlemefrs27.j |
. . 3
β’ β¨ =
(joinβπΎ) |
4 | | cdlemefrs27.m |
. . 3
β’ β§ =
(meetβπΎ) |
5 | | cdlemefrs27.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
6 | | cdlemefrs27.h |
. . 3
β’ π» = (LHypβπΎ) |
7 | | cdlemefrs27.eq |
. . 3
β’ (π = π
β (π β π)) |
8 | | cdlemefrs27.nb |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) |
9 | | cdlemefrs27.rnb |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β β¦π
/ π β¦π β π΅) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cdlemefrs29bpre1 38889 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β βπ§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π)))) |
11 | | simp11 1204 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β (πΎ β HL β§ π β π»)) |
12 | | simp2rl 1243 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β π
β π΄) |
13 | 1, 5 | atbase 37780 |
. . . . . 6
β’ (π
β π΄ β π
β π΅) |
14 | 12, 13 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β π
β π΅) |
15 | | simp2rr 1244 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β Β¬ π
β€ π) |
16 | 1, 2, 3, 4, 5, 6 | lhpmcvr2 38516 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π
β π΅ β§ Β¬ π
β€ π)) β βπ β π΄ (Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
)) |
17 | 11, 14, 15, 16 | syl12anc 836 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β βπ β π΄ (Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
)) |
18 | | simpl3 1194 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β π) |
19 | 7 | pm5.32ri 577 |
. . . . . . . . . 10
β’ ((π β§ π = π
) β (π β§ π = π
)) |
20 | 19 | baibr 538 |
. . . . . . . . 9
β’ (π β (π = π
β (π β§ π = π
))) |
21 | 18, 20 | syl 17 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β (π = π
β (π β§ π = π
))) |
22 | | simp2r 1201 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β (π
β π΄ β§ Β¬ π
β€ π)) |
23 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(0.βπΎ) =
(0.βπΎ) |
24 | 2, 4, 23, 5, 6 | lhpmat 38522 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ (π
β π΄ β§ Β¬ π
β€ π)) β (π
β§ π) = (0.βπΎ)) |
25 | 11, 22, 24 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β (π
β§ π) = (0.βπΎ)) |
26 | 25 | adantr 482 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β (π
β§ π) = (0.βπΎ)) |
27 | 26 | oveq2d 7378 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β (π β¨ (π
β§ π)) = (π β¨ (0.βπΎ))) |
28 | | simp11l 1285 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β πΎ β HL) |
29 | | hlol 37852 |
. . . . . . . . . . . 12
β’ (πΎ β HL β πΎ β OL) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β πΎ β OL) |
31 | 1, 5 | atbase 37780 |
. . . . . . . . . . 11
β’ (π β π΄ β π β π΅) |
32 | 1, 3, 23 | olj01 37716 |
. . . . . . . . . . 11
β’ ((πΎ β OL β§ π β π΅) β (π β¨ (0.βπΎ)) = π ) |
33 | 30, 31, 32 | syl2an 597 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β (π β¨ (0.βπΎ)) = π ) |
34 | 27, 33 | eqtrd 2777 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β (π β¨ (π
β§ π)) = π ) |
35 | 34 | eqeq1d 2739 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β ((π β¨ (π
β§ π)) = π
β π = π
)) |
36 | 35 | anbi2d 630 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β ((π β§ (π β¨ (π
β§ π)) = π
) β (π β§ π = π
))) |
37 | 21, 35, 36 | 3bitr4d 311 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β ((π β¨ (π
β§ π)) = π
β (π β§ (π β¨ (π
β§ π)) = π
))) |
38 | 37 | anbi2d 630 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β (Β¬ π β€ π β§ (π β§ (π β¨ (π
β§ π)) = π
)))) |
39 | | anass 470 |
. . . . . 6
β’ (((Β¬
π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
) β (Β¬ π β€ π β§ (π β§ (π β¨ (π
β§ π)) = π
))) |
40 | 38, 39 | bitr4di 289 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β§ π β π΄) β ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β ((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
))) |
41 | 40 | rexbidva 3174 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β (βπ β π΄ (Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β βπ β π΄ ((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
))) |
42 | 17, 41 | mpbid 231 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β βπ β π΄ ((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
)) |
43 | | reusv1 5357 |
. . 3
β’
(βπ β
π΄ ((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
) β (β!π§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))) β βπ§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))))) |
44 | 42, 43 | syl 17 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β (β!π§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))) β βπ§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))))) |
45 | 10, 44 | mpbird 257 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ π) β β!π§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π)))) |