Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . 6
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
2 | | ishlat.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
3 | 1, 2 | eqtr4di 2791 |
. . . . 5
β’ (π = πΎ β (Atomsβπ) = π΄) |
4 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
5 | | ishlat.l |
. . . . . . . . . . . 12
β’ β€ =
(leβπΎ) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = πΎ β (leβπ) = β€ ) |
7 | 6 | breqd 5117 |
. . . . . . . . . 10
β’ (π = πΎ β (π§(leβπ)(π₯(joinβπ)π¦) β π§ β€ (π₯(joinβπ)π¦))) |
8 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
9 | | ishlat.j |
. . . . . . . . . . . . 13
β’ β¨ =
(joinβπΎ) |
10 | 8, 9 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (π = πΎ β (joinβπ) = β¨ ) |
11 | 10 | oveqd 7375 |
. . . . . . . . . . 11
β’ (π = πΎ β (π₯(joinβπ)π¦) = (π₯ β¨ π¦)) |
12 | 11 | breq2d 5118 |
. . . . . . . . . 10
β’ (π = πΎ β (π§ β€ (π₯(joinβπ)π¦) β π§ β€ (π₯ β¨ π¦))) |
13 | 7, 12 | bitrd 279 |
. . . . . . . . 9
β’ (π = πΎ β (π§(leβπ)(π₯(joinβπ)π¦) β π§ β€ (π₯ β¨ π¦))) |
14 | 13 | 3anbi3d 1443 |
. . . . . . . 8
β’ (π = πΎ β ((π§ β π₯ β§ π§ β π¦ β§ π§(leβπ)(π₯(joinβπ)π¦)) β (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦)))) |
15 | 3, 14 | rexeqbidv 3319 |
. . . . . . 7
β’ (π = πΎ β (βπ§ β (Atomsβπ)(π§ β π₯ β§ π§ β π¦ β§ π§(leβπ)(π₯(joinβπ)π¦)) β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦)))) |
16 | 15 | imbi2d 341 |
. . . . . 6
β’ (π = πΎ β ((π₯ β π¦ β βπ§ β (Atomsβπ)(π§ β π₯ β§ π§ β π¦ β§ π§(leβπ)(π₯(joinβπ)π¦))) β (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))))) |
17 | 3, 16 | raleqbidv 3318 |
. . . . 5
β’ (π = πΎ β (βπ¦ β (Atomsβπ)(π₯ β π¦ β βπ§ β (Atomsβπ)(π§ β π₯ β§ π§ β π¦ β§ π§(leβπ)(π₯(joinβπ)π¦))) β βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))))) |
18 | 3, 17 | raleqbidv 3318 |
. . . 4
β’ (π = πΎ β (βπ₯ β (Atomsβπ)βπ¦ β (Atomsβπ)(π₯ β π¦ β βπ§ β (Atomsβπ)(π§ β π₯ β§ π§ β π¦ β§ π§(leβπ)(π₯(joinβπ)π¦))) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))))) |
19 | | fveq2 6843 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
20 | | ishlat.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
21 | 19, 20 | eqtr4di 2791 |
. . . . 5
β’ (π = πΎ β (Baseβπ) = π΅) |
22 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΎ β (ltβπ) = (ltβπΎ)) |
23 | | ishlat.s |
. . . . . . . . . . . 12
β’ < =
(ltβπΎ) |
24 | 22, 23 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = πΎ β (ltβπ) = < ) |
25 | 24 | breqd 5117 |
. . . . . . . . . 10
β’ (π = πΎ β ((0.βπ)(ltβπ)π₯ β (0.βπ) < π₯)) |
26 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΎ β (0.βπ) = (0.βπΎ)) |
27 | | ishlat.z |
. . . . . . . . . . . 12
β’ 0 =
(0.βπΎ) |
28 | 26, 27 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = πΎ β (0.βπ) = 0 ) |
29 | 28 | breq1d 5116 |
. . . . . . . . . 10
β’ (π = πΎ β ((0.βπ) < π₯ β 0 < π₯)) |
30 | 25, 29 | bitrd 279 |
. . . . . . . . 9
β’ (π = πΎ β ((0.βπ)(ltβπ)π₯ β 0 < π₯)) |
31 | 24 | breqd 5117 |
. . . . . . . . 9
β’ (π = πΎ β (π₯(ltβπ)π¦ β π₯ < π¦)) |
32 | 30, 31 | anbi12d 632 |
. . . . . . . 8
β’ (π = πΎ β (((0.βπ)(ltβπ)π₯ β§ π₯(ltβπ)π¦) β ( 0 < π₯ β§ π₯ < π¦))) |
33 | 24 | breqd 5117 |
. . . . . . . . 9
β’ (π = πΎ β (π¦(ltβπ)π§ β π¦ < π§)) |
34 | 24 | breqd 5117 |
. . . . . . . . . 10
β’ (π = πΎ β (π§(ltβπ)(1.βπ) β π§ < (1.βπ))) |
35 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΎ β (1.βπ) = (1.βπΎ)) |
36 | | ishlat.u |
. . . . . . . . . . . 12
β’ 1 =
(1.βπΎ) |
37 | 35, 36 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = πΎ β (1.βπ) = 1 ) |
38 | 37 | breq2d 5118 |
. . . . . . . . . 10
β’ (π = πΎ β (π§ < (1.βπ) β π§ < 1 )) |
39 | 34, 38 | bitrd 279 |
. . . . . . . . 9
β’ (π = πΎ β (π§(ltβπ)(1.βπ) β π§ < 1 )) |
40 | 33, 39 | anbi12d 632 |
. . . . . . . 8
β’ (π = πΎ β ((π¦(ltβπ)π§ β§ π§(ltβπ)(1.βπ)) β (π¦ < π§ β§ π§ < 1 ))) |
41 | 32, 40 | anbi12d 632 |
. . . . . . 7
β’ (π = πΎ β ((((0.βπ)(ltβπ)π₯ β§ π₯(ltβπ)π¦) β§ (π¦(ltβπ)π§ β§ π§(ltβπ)(1.βπ))) β (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 )))) |
42 | 21, 41 | rexeqbidv 3319 |
. . . . . 6
β’ (π = πΎ β (βπ§ β (Baseβπ)(((0.βπ)(ltβπ)π₯ β§ π₯(ltβπ)π¦) β§ (π¦(ltβπ)π§ β§ π§(ltβπ)(1.βπ))) β βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 )))) |
43 | 21, 42 | rexeqbidv 3319 |
. . . . 5
β’ (π = πΎ β (βπ¦ β (Baseβπ)βπ§ β (Baseβπ)(((0.βπ)(ltβπ)π₯ β§ π₯(ltβπ)π¦) β§ (π¦(ltβπ)π§ β§ π§(ltβπ)(1.βπ))) β βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 )))) |
44 | 21, 43 | rexeqbidv 3319 |
. . . 4
β’ (π = πΎ β (βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)βπ§ β (Baseβπ)(((0.βπ)(ltβπ)π₯ β§ π₯(ltβπ)π¦) β§ (π¦(ltβπ)π§ β§ π§(ltβπ)(1.βπ))) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 )))) |
45 | 18, 44 | anbi12d 632 |
. . 3
β’ (π = πΎ β ((βπ₯ β (Atomsβπ)βπ¦ β (Atomsβπ)(π₯ β π¦ β βπ§ β (Atomsβπ)(π§ β π₯ β§ π§ β π¦ β§ π§(leβπ)(π₯(joinβπ)π¦))) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)βπ§ β (Baseβπ)(((0.βπ)(ltβπ)π₯ β§ π₯(ltβπ)π¦) β§ (π¦(ltβπ)π§ β§ π§(ltβπ)(1.βπ)))) β (βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |
46 | | df-hlat 37859 |
. . 3
β’ HL =
{π β ((OML β© CLat)
β© CvLat) β£ (βπ₯ β (Atomsβπ)βπ¦ β (Atomsβπ)(π₯ β π¦ β βπ§ β (Atomsβπ)(π§ β π₯ β§ π§ β π¦ β§ π§(leβπ)(π₯(joinβπ)π¦))) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)βπ§ β (Baseβπ)(((0.βπ)(ltβπ)π₯ β§ π₯(ltβπ)π¦) β§ (π¦(ltβπ)π§ β§ π§(ltβπ)(1.βπ))))} |
47 | 45, 46 | elrab2 3649 |
. 2
β’ (πΎ β HL β (πΎ β ((OML β© CLat) β©
CvLat) β§ (βπ₯
β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |
48 | | elin 3927 |
. . . . 5
β’ (πΎ β (OML β© CLat) β
(πΎ β OML β§ πΎ β CLat)) |
49 | 48 | anbi1i 625 |
. . . 4
β’ ((πΎ β (OML β© CLat) β§
πΎ β CvLat) β
((πΎ β OML β§ πΎ β CLat) β§ πΎ β CvLat)) |
50 | | elin 3927 |
. . . 4
β’ (πΎ β ((OML β© CLat) β©
CvLat) β (πΎ β
(OML β© CLat) β§ πΎ
β CvLat)) |
51 | | df-3an 1090 |
. . . 4
β’ ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β ((πΎ β OML β§ πΎ β CLat) β§ πΎ β CvLat)) |
52 | 49, 50, 51 | 3bitr4ri 304 |
. . 3
β’ ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β πΎ β ((OML β© CLat) β©
CvLat)) |
53 | 52 | anbi1i 625 |
. 2
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§
(βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 )))) β (πΎ β ((OML β© CLat) β©
CvLat) β§ (βπ₯
β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |
54 | 47, 53 | bitr4i 278 |
1
β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§
(βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |