Step | Hyp | Ref
| Expression |
1 | | dalem.ph |
. . . . 5
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π
) β§ Β¬ πΆ β€ (π
β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π
β¨ π))))) |
2 | | dalem.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | dalem.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
4 | | dalem.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
5 | | dalem58.y |
. . . . 5
β’ π = ((π β¨ π) β¨ π
) |
6 | | dalem58.z |
. . . . 5
β’ π = ((π β¨ π) β¨ π) |
7 | 1, 2, 3, 4, 5, 6 | dalemrot 37933 |
. . . 4
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π
β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (((π β¨ π
) β¨ π) β π β§ ((π β¨ π) β¨ π) β π) β§ ((Β¬ πΆ β€ (π β¨ π
) β§ Β¬ πΆ β€ (π
β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π
β¨ π) β§ πΆ β€ (π β¨ π))))) |
8 | 7 | 3ad2ant1 1132 |
. . 3
β’ ((π β§ π = π β§ π) β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π
β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (((π β¨ π
) β¨ π) β π β§ ((π β¨ π) β¨ π) β π) β§ ((Β¬ πΆ β€ (π β¨ π
) β§ Β¬ πΆ β€ (π
β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π
β¨ π) β§ πΆ β€ (π β¨ π))))) |
9 | 1, 2, 3, 4, 5, 6 | dalemrotyz 37934 |
. . . 4
β’ ((π β§ π = π) β ((π β¨ π
) β¨ π) = ((π β¨ π) β¨ π)) |
10 | 9 | 3adant3 1131 |
. . 3
β’ ((π β§ π = π β§ π) β ((π β¨ π
) β¨ π) = ((π β¨ π) β¨ π)) |
11 | | dalem.ps |
. . . . 5
β’ (π β ((π β π΄ β§ π β π΄) β§ Β¬ π β€ π β§ (π β π β§ Β¬ π β€ π β§ πΆ β€ (π β¨ π)))) |
12 | 1, 2, 3, 4, 11, 5 | dalemrotps 37967 |
. . . 4
β’ ((π β§ π) β ((π β π΄ β§ π β π΄) β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ (π β π β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ πΆ β€ (π β¨ π)))) |
13 | 12 | 3adant2 1130 |
. . 3
β’ ((π β§ π = π β§ π) β ((π β π΄ β§ π β π΄) β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ (π β π β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ πΆ β€ (π β¨ π)))) |
14 | | biid 260 |
. . . 4
β’ ((((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π
β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (((π β¨ π
) β¨ π) β π β§ ((π β¨ π) β¨ π) β π) β§ ((Β¬ πΆ β€ (π β¨ π
) β§ Β¬ πΆ β€ (π
β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π
β¨ π) β§ πΆ β€ (π β¨ π)))) β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π
β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (((π β¨ π
) β¨ π) β π β§ ((π β¨ π) β¨ π) β π) β§ ((Β¬ πΆ β€ (π β¨ π
) β§ Β¬ πΆ β€ (π
β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π
β¨ π) β§ πΆ β€ (π β¨ π))))) |
15 | | biid 260 |
. . . 4
β’ (((π β π΄ β§ π β π΄) β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ (π β π β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ πΆ β€ (π β¨ π))) β ((π β π΄ β§ π β π΄) β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ (π β π β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ πΆ β€ (π β¨ π)))) |
16 | | dalem58.m |
. . . 4
β’ β§ =
(meetβπΎ) |
17 | | dalem58.o |
. . . 4
β’ π = (LPlanesβπΎ) |
18 | | eqid 2736 |
. . . 4
β’ ((π β¨ π
) β¨ π) = ((π β¨ π
) β¨ π) |
19 | | eqid 2736 |
. . . 4
β’ ((π β¨ π) β¨ π) = ((π β¨ π) β¨ π) |
20 | | dalem58.e |
. . . 4
β’ πΈ = ((π β¨ π
) β§ (π β¨ π)) |
21 | | dalem58.h |
. . . 4
β’ π» = ((π β¨ π) β§ (π β¨ π)) |
22 | | dalem58.i |
. . . 4
β’ πΌ = ((π β¨ π
) β§ (π β¨ π)) |
23 | | dalem58.g |
. . . 4
β’ πΊ = ((π β¨ π) β§ (π β¨ π)) |
24 | | eqid 2736 |
. . . 4
β’ (((π» β¨ πΌ) β¨ πΊ) β§ ((π β¨ π
) β¨ π)) = (((π» β¨ πΌ) β¨ πΊ) β§ ((π β¨ π
) β¨ π)) |
25 | 14, 2, 3, 4, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24 | dalem57 38005 |
. . 3
β’
(((((πΎ β HL
β§ πΆ β
(BaseβπΎ)) β§
(π β π΄ β§ π
β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (((π β¨ π
) β¨ π) β π β§ ((π β¨ π) β¨ π) β π) β§ ((Β¬ πΆ β€ (π β¨ π
) β§ Β¬ πΆ β€ (π
β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π
β¨ π) β§ πΆ β€ (π β¨ π)))) β§ ((π β¨ π
) β¨ π) = ((π β¨ π) β¨ π) β§ ((π β π΄ β§ π β π΄) β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ (π β π β§ Β¬ π β€ ((π β¨ π
) β¨ π) β§ πΆ β€ (π β¨ π)))) β πΈ β€ (((π» β¨ πΌ) β¨ πΊ) β§ ((π β¨ π
) β¨ π))) |
26 | 8, 10, 13, 25 | syl3anc 1370 |
. 2
β’ ((π β§ π = π β§ π) β πΈ β€ (((π» β¨ πΌ) β¨ πΊ) β§ ((π β¨ π
) β¨ π))) |
27 | 1 | dalemkehl 37899 |
. . . . . 6
β’ (π β πΎ β HL) |
28 | 27 | 3ad2ant1 1132 |
. . . . 5
β’ ((π β§ π = π β§ π) β πΎ β HL) |
29 | 1, 2, 3, 4, 11, 16, 17, 5, 6, 21 | dalem29 37977 |
. . . . 5
β’ ((π β§ π = π β§ π) β π» β π΄) |
30 | 1, 2, 3, 4, 11, 16, 17, 5, 6, 22 | dalem34 37982 |
. . . . 5
β’ ((π β§ π = π β§ π) β πΌ β π΄) |
31 | 1, 2, 3, 4, 11, 16, 17, 5, 6, 23 | dalem23 37972 |
. . . . 5
β’ ((π β§ π = π β§ π) β πΊ β π΄) |
32 | 3, 4 | hlatjrot 37648 |
. . . . 5
β’ ((πΎ β HL β§ (π» β π΄ β§ πΌ β π΄ β§ πΊ β π΄)) β ((π» β¨ πΌ) β¨ πΊ) = ((πΊ β¨ π») β¨ πΌ)) |
33 | 28, 29, 30, 31, 32 | syl13anc 1371 |
. . . 4
β’ ((π β§ π = π β§ π) β ((π» β¨ πΌ) β¨ πΊ) = ((πΊ β¨ π») β¨ πΌ)) |
34 | 1, 3, 4 | dalemqrprot 37924 |
. . . . . 6
β’ (π β ((π β¨ π
) β¨ π) = ((π β¨ π) β¨ π
)) |
35 | 34, 5 | eqtr4di 2794 |
. . . . 5
β’ (π β ((π β¨ π
) β¨ π) = π) |
36 | 35 | 3ad2ant1 1132 |
. . . 4
β’ ((π β§ π = π β§ π) β ((π β¨ π
) β¨ π) = π) |
37 | 33, 36 | oveq12d 7355 |
. . 3
β’ ((π β§ π = π β§ π) β (((π» β¨ πΌ) β¨ πΊ) β§ ((π β¨ π
) β¨ π)) = (((πΊ β¨ π») β¨ πΌ) β§ π)) |
38 | | dalem58.b1 |
. . 3
β’ π΅ = (((πΊ β¨ π») β¨ πΌ) β§ π) |
39 | 37, 38 | eqtr4di 2794 |
. 2
β’ ((π β§ π = π β§ π) β (((π» β¨ πΌ) β¨ πΊ) β§ ((π β¨ π
) β¨ π)) = π΅) |
40 | 26, 39 | breqtrd 5118 |
1
β’ ((π β§ π = π β§ π) β πΈ β€ π΅) |