Step | Hyp | Ref
| Expression |
1 | | simp3 1138 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β (πΉβ(πΊβπ)) = π) |
2 | 1 | oveq2d 7427 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β ((πΊβπ)(joinβπΎ)(πΉβ(πΊβπ))) = ((πΊβπ)(joinβπΎ)π)) |
3 | | simp1l 1197 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β πΎ β HL) |
4 | | simp1 1136 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β (πΎ β HL β§ π β π»)) |
5 | | simp23 1208 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β πΊ β π) |
6 | | simp21 1206 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β (π β π΄ β§ Β¬ π β€ π)) |
7 | | cdlemg4.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
8 | | cdlemg4.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
9 | | cdlemg4.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
10 | | cdlemg4.t |
. . . . . . . 8
β’ π = ((LTrnβπΎ)βπ) |
11 | 7, 8, 9, 10 | ltrnel 39313 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
12 | 11 | simpld 495 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊβπ) β π΄) |
13 | 4, 5, 6, 12 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β (πΊβπ) β π΄) |
14 | | simp21l 1290 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β π β π΄) |
15 | | eqid 2732 |
. . . . . 6
β’
(joinβπΎ) =
(joinβπΎ) |
16 | 15, 8 | hlatjcom 38541 |
. . . . 5
β’ ((πΎ β HL β§ (πΊβπ) β π΄ β§ π β π΄) β ((πΊβπ)(joinβπΎ)π) = (π(joinβπΎ)(πΊβπ))) |
17 | 3, 13, 14, 16 | syl3anc 1371 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β ((πΊβπ)(joinβπΎ)π) = (π(joinβπΎ)(πΊβπ))) |
18 | 2, 17 | eqtrd 2772 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β ((πΊβπ)(joinβπΎ)(πΉβ(πΊβπ))) = (π(joinβπΎ)(πΊβπ))) |
19 | 18 | oveq1d 7426 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β (((πΊβπ)(joinβπΎ)(πΉβ(πΊβπ)))(meetβπΎ)π) = ((π(joinβπΎ)(πΊβπ))(meetβπΎ)π)) |
20 | | simp22 1207 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β πΉ β π) |
21 | 4, 5, 6, 11 | syl3anc 1371 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
22 | | eqid 2732 |
. . . 4
β’
(meetβπΎ) =
(meetβπΎ) |
23 | | cdlemg4.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
24 | 7, 15, 22, 8, 9, 10, 23 | trlval2 39337 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) β (π
βπΉ) = (((πΊβπ)(joinβπΎ)(πΉβ(πΊβπ)))(meetβπΎ)π)) |
25 | 4, 20, 21, 24 | syl3anc 1371 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β (π
βπΉ) = (((πΊβπ)(joinβπΎ)(πΉβ(πΊβπ)))(meetβπΎ)π)) |
26 | 7, 15, 22, 8, 9, 10, 23 | trlval2 39337 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΊ) = ((π(joinβπΎ)(πΊβπ))(meetβπΎ)π)) |
27 | 4, 5, 6, 26 | syl3anc 1371 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β (π
βπΊ) = ((π(joinβπΎ)(πΊβπ))(meetβπΎ)π)) |
28 | 19, 25, 27 | 3eqtr4d 2782 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β (π
βπΉ) = (π
βπΊ)) |