Step | Hyp | Ref
| Expression |
1 | | dihjatcclem.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
2 | | dihjatcclem.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
3 | | dihjatcclem.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
4 | | dihjatcclem.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
5 | | dihjatcc.w |
. . . . . . 7
β’ πΆ = ((ocβπΎ)βπ) |
6 | 2, 3, 4, 5 | lhpocnel2 38890 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β (πΆ β π΄ β§ Β¬ πΆ β€ π)) |
7 | 1, 6 | syl 17 |
. . . . 5
β’ (π β (πΆ β π΄ β§ Β¬ πΆ β€ π)) |
8 | | dihjatcclem.p |
. . . . 5
β’ (π β (π β π΄ β§ Β¬ π β€ π)) |
9 | | dihjatcc.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
10 | | dihjatcc.g |
. . . . . 6
β’ πΊ = (β©π β π (πβπΆ) = π) |
11 | 2, 3, 4, 9, 10 | ltrniotacl 39450 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΆ β π΄ β§ Β¬ πΆ β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ β π) |
12 | 1, 7, 8, 11 | syl3anc 1372 |
. . . 4
β’ (π β πΊ β π) |
13 | | dihjatcclem.q |
. . . . . 6
β’ (π β (π β π΄ β§ Β¬ π β€ π)) |
14 | | dihjatcc.dd |
. . . . . . 7
β’ π· = (β©π β π (πβπΆ) = π) |
15 | 2, 3, 4, 9, 14 | ltrniotacl 39450 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΆ β π΄ β§ Β¬ πΆ β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β π· β π) |
16 | 1, 7, 13, 15 | syl3anc 1372 |
. . . . 5
β’ (π β π· β π) |
17 | 4, 9 | ltrncnv 39017 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π· β π) β β‘π· β π) |
18 | 1, 16, 17 | syl2anc 585 |
. . . 4
β’ (π β β‘π· β π) |
19 | 4, 9 | ltrnco 39590 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ β‘π· β π) β (πΊ β β‘π·) β π) |
20 | 1, 12, 18, 19 | syl3anc 1372 |
. . 3
β’ (π β (πΊ β β‘π·) β π) |
21 | | dihjatcclem.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
22 | | dihjatcclem.m |
. . . 4
β’ β§ =
(meetβπΎ) |
23 | | dihjatcc.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
24 | 2, 21, 22, 3, 4, 9,
23 | trlval2 39034 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΊ β β‘π·) β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πΊ β β‘π·)) = ((π β¨ ((πΊ β β‘π·)βπ)) β§ π)) |
25 | 1, 20, 13, 24 | syl3anc 1372 |
. 2
β’ (π β (π
β(πΊ β β‘π·)) = ((π β¨ ((πΊ β β‘π·)βπ)) β§ π)) |
26 | 13 | simpld 496 |
. . . . . . . 8
β’ (π β π β π΄) |
27 | 2, 3, 4, 9 | ltrncoval 39016 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ β‘π· β π) β§ π β π΄) β ((πΊ β β‘π·)βπ) = (πΊβ(β‘π·βπ))) |
28 | 1, 12, 18, 26, 27 | syl121anc 1376 |
. . . . . . 7
β’ (π β ((πΊ β β‘π·)βπ) = (πΊβ(β‘π·βπ))) |
29 | 2, 3, 4, 9, 14 | ltrniotacnvval 39453 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (πΆ β π΄ β§ Β¬ πΆ β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (β‘π·βπ) = πΆ) |
30 | 1, 7, 13, 29 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (β‘π·βπ) = πΆ) |
31 | 30 | fveq2d 6896 |
. . . . . . . 8
β’ (π β (πΊβ(β‘π·βπ)) = (πΊβπΆ)) |
32 | 2, 3, 4, 9, 10 | ltrniotaval 39452 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΆ β π΄ β§ Β¬ πΆ β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊβπΆ) = π) |
33 | 1, 7, 8, 32 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (πΊβπΆ) = π) |
34 | 31, 33 | eqtrd 2773 |
. . . . . . 7
β’ (π β (πΊβ(β‘π·βπ)) = π) |
35 | 28, 34 | eqtrd 2773 |
. . . . . 6
β’ (π β ((πΊ β β‘π·)βπ) = π) |
36 | 35 | oveq2d 7425 |
. . . . 5
β’ (π β (π β¨ ((πΊ β β‘π·)βπ)) = (π β¨ π)) |
37 | 1 | simpld 496 |
. . . . . 6
β’ (π β πΎ β HL) |
38 | 8 | simpld 496 |
. . . . . 6
β’ (π β π β π΄) |
39 | 21, 3 | hlatjcom 38238 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
40 | 37, 38, 26, 39 | syl3anc 1372 |
. . . . 5
β’ (π β (π β¨ π) = (π β¨ π)) |
41 | 36, 40 | eqtr4d 2776 |
. . . 4
β’ (π β (π β¨ ((πΊ β β‘π·)βπ)) = (π β¨ π)) |
42 | 41 | oveq1d 7424 |
. . 3
β’ (π β ((π β¨ ((πΊ β β‘π·)βπ)) β§ π) = ((π β¨ π) β§ π)) |
43 | | dihjatcclem.v |
. . 3
β’ π = ((π β¨ π) β§ π) |
44 | 42, 43 | eqtr4di 2791 |
. 2
β’ (π β ((π β¨ ((πΊ β β‘π·)βπ)) β§ π) = π) |
45 | 25, 44 | eqtrd 2773 |
1
β’ (π β (π
β(πΊ β β‘π·)) = π) |