Step | Hyp | Ref
| Expression |
1 | | cdlemef47.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | cdlemef47.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | cdlemef47.j |
. . 3
β’ β¨ =
(joinβπΎ) |
4 | | cdlemef47.m |
. . 3
β’ β§ =
(meetβπΎ) |
5 | | cdlemef47.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
6 | | cdlemef47.h |
. . 3
β’ π» = (LHypβπΎ) |
7 | | cdlemef47.v |
. . 3
β’ π = ((π β¨ π) β§ π) |
8 | | cdlemef47.n |
. . 3
β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) |
9 | | cdlemefs47.o |
. . 3
β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) |
10 | | cdlemef47.g |
. . 3
β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cdlemeg47rv 39906 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΊβπ
) = β¦π
/ π’β¦β¦π / π£β¦π) |
12 | | simp22l 1290 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π
β π΄) |
13 | | nfcvd 2899 |
. . . . 5
β’ (π
β π΄ β β²π’((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π
β¨ π) β§ π)))) |
14 | | oveq1 7421 |
. . . . . . . 8
β’ (π’ = π
β (π’ β¨ π) = (π
β¨ π)) |
15 | 14 | oveq1d 7429 |
. . . . . . 7
β’ (π’ = π
β ((π’ β¨ π) β§ π) = ((π
β¨ π) β§ π)) |
16 | 15 | oveq2d 7430 |
. . . . . 6
β’ (π’ = π
β (β¦π / π£β¦π β¨ ((π’ β¨ π) β§ π)) = (β¦π / π£β¦π β¨ ((π
β¨ π) β§ π))) |
17 | 16 | oveq2d 7430 |
. . . . 5
β’ (π’ = π
β ((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π’ β¨ π) β§ π))) = ((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π
β¨ π) β§ π)))) |
18 | 13, 17 | csbiegf 3923 |
. . . 4
β’ (π
β π΄ β β¦π
/ π’β¦((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π’ β¨ π) β§ π))) = ((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π
β¨ π) β§ π)))) |
19 | 12, 18 | syl 17 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π
/ π’β¦((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π’ β¨ π) β§ π))) = ((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π
β¨ π) β§ π)))) |
20 | | simp23l 1292 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
21 | | eqid 2727 |
. . . . . 6
β’ ((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π’ β¨ π) β§ π))) = ((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π’ β¨ π) β§ π))) |
22 | 9, 21 | cdleme31se2 39780 |
. . . . 5
β’ (π β π΄ β β¦π / π£β¦π = ((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π’ β¨ π) β§ π)))) |
23 | 20, 22 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π / π£β¦π = ((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π’ β¨ π) β§ π)))) |
24 | 23 | csbeq2dv 3896 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π
/ π’β¦β¦π / π£β¦π = β¦π
/ π’β¦((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π’ β¨ π) β§ π)))) |
25 | | simp1 1134 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) |
26 | | simp21 1204 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π) |
27 | | simp23 1206 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
28 | | simp3r 1200 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) |
29 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cdlemeg47b 39905 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΊβπ) = β¦π / π£β¦π) |
30 | 25, 26, 27, 28, 29 | syl121anc 1373 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΊβπ) = β¦π / π£β¦π) |
31 | 30 | oveq1d 7429 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((πΊβπ) β¨ ((π
β¨ π) β§ π)) = (β¦π / π£β¦π β¨ ((π
β¨ π) β§ π))) |
32 | 31 | oveq2d 7430 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ ((πΊβπ) β¨ ((π
β¨ π) β§ π))) = ((π β¨ π) β§ (β¦π / π£β¦π β¨ ((π
β¨ π) β§ π)))) |
33 | 19, 24, 32 | 3eqtr4d 2777 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π
/ π’β¦β¦π / π£β¦π = ((π β¨ π) β§ ((πΊβπ) β¨ ((π
β¨ π) β§ π)))) |
34 | 11, 33 | eqtrd 2767 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΊβπ
) = ((π β¨ π) β§ ((πΊβπ) β¨ ((π
β¨ π) β§ π)))) |