Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β πΎ β OML) |
2 | | omlop 38049 |
. . . . 5
β’ (πΎ β OML β πΎ β OP) |
3 | 2 | 3ad2ant1 1134 |
. . . 4
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β πΎ β OP) |
4 | | simp3 1139 |
. . . 4
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β π β π΅) |
5 | | omllaw4.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
6 | | omllaw4.o |
. . . . 5
β’ β₯ =
(ocβπΎ) |
7 | 5, 6 | opoccl 38002 |
. . . 4
β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) |
8 | 3, 4, 7 | syl2anc 585 |
. . 3
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ βπ) β π΅) |
9 | | simp2 1138 |
. . . 4
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β π β π΅) |
10 | 5, 6 | opoccl 38002 |
. . . 4
β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) |
11 | 3, 9, 10 | syl2anc 585 |
. . 3
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ βπ) β π΅) |
12 | | omllaw4.l |
. . . 4
β’ β€ =
(leβπΎ) |
13 | | eqid 2733 |
. . . 4
β’
(joinβπΎ) =
(joinβπΎ) |
14 | | omllaw4.m |
. . . 4
β’ β§ =
(meetβπΎ) |
15 | 5, 12, 13, 14, 6 | omllaw 38051 |
. . 3
β’ ((πΎ β OML β§ ( β₯
βπ) β π΅ β§ ( β₯ βπ) β π΅) β (( β₯ βπ) β€ ( β₯ βπ) β ( β₯ βπ) = (( β₯ βπ)(joinβπΎ)(( β₯ βπ) β§ ( β₯ β( β₯
βπ)))))) |
16 | 1, 8, 11, 15 | syl3anc 1372 |
. 2
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (( β₯ βπ) β€ ( β₯ βπ) β ( β₯ βπ) = (( β₯ βπ)(joinβπΎ)(( β₯ βπ) β§ ( β₯ β( β₯
βπ)))))) |
17 | 5, 12, 6 | oplecon3b 38008 |
. . 3
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) |
18 | 2, 17 | syl3an1 1164 |
. 2
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β ( β₯ βπ) β€ ( β₯ βπ))) |
19 | | omllat 38050 |
. . . . . 6
β’ (πΎ β OML β πΎ β Lat) |
20 | 19 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β πΎ β Lat) |
21 | 5, 14 | latmcl 18389 |
. . . . . . 7
β’ ((πΎ β Lat β§ ( β₯
βπ) β π΅ β§ π β π΅) β (( β₯ βπ) β§ π) β π΅) |
22 | 20, 11, 4, 21 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (( β₯ βπ) β§ π) β π΅) |
23 | 5, 6 | opoccl 38002 |
. . . . . 6
β’ ((πΎ β OP β§ (( β₯
βπ) β§ π) β π΅) β ( β₯ β(( β₯
βπ) β§ π)) β π΅) |
24 | 3, 22, 23 | syl2anc 585 |
. . . . 5
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯
βπ) β§ π)) β π΅) |
25 | 5, 14 | latmcl 18389 |
. . . . 5
β’ ((πΎ β Lat β§ ( β₯
β(( β₯ βπ) β§ π)) β π΅ β§ π β π΅) β (( β₯ β(( β₯
βπ) β§ π)) β§ π) β π΅) |
26 | 20, 24, 4, 25 | syl3anc 1372 |
. . . 4
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (( β₯ β(( β₯
βπ) β§ π)) β§ π) β π΅) |
27 | 5, 6 | opcon3b 38004 |
. . . 4
β’ ((πΎ β OP β§ (( β₯
β(( β₯ βπ) β§ π)) β§ π) β π΅ β§ π β π΅) β ((( β₯ β(( β₯
βπ) β§ π)) β§ π) = π β ( β₯ βπ) = ( β₯ β(( β₯
β(( β₯ βπ) β§ π)) β§ π)))) |
28 | 3, 26, 9, 27 | syl3anc 1372 |
. . 3
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((( β₯ β(( β₯
βπ) β§ π)) β§ π) = π β ( β₯ βπ) = ( β₯ β(( β₯
β(( β₯ βπ) β§ π)) β§ π)))) |
29 | 5, 13 | latjcom 18396 |
. . . . . 6
β’ ((πΎ β Lat β§ (( β₯
βπ) β§ π) β π΅ β§ ( β₯ βπ) β π΅) β ((( β₯ βπ) β§ π)(joinβπΎ)( β₯ βπ)) = (( β₯ βπ)(joinβπΎ)(( β₯ βπ) β§ π))) |
30 | 20, 22, 8, 29 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((( β₯ βπ) β§ π)(joinβπΎ)( β₯ βπ)) = (( β₯ βπ)(joinβπΎ)(( β₯ βπ) β§ π))) |
31 | | omlol 38048 |
. . . . . . 7
β’ (πΎ β OML β πΎ β OL) |
32 | 31 | 3ad2ant1 1134 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β πΎ β OL) |
33 | 5, 13, 14, 6 | oldmm2 38026 |
. . . . . 6
β’ ((πΎ β OL β§ (( β₯
βπ) β§ π) β π΅ β§ π β π΅) β ( β₯ β(( β₯
β(( β₯ βπ) β§ π)) β§ π)) = ((( β₯ βπ) β§ π)(joinβπΎ)( β₯ βπ))) |
34 | 32, 22, 4, 33 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯
β(( β₯ βπ) β§ π)) β§ π)) = ((( β₯ βπ) β§ π)(joinβπΎ)( β₯ βπ))) |
35 | 5, 6 | opococ 38003 |
. . . . . . . 8
β’ ((πΎ β OP β§ π β π΅) β ( β₯ β( β₯
βπ)) = π) |
36 | 3, 4, 35 | syl2anc 585 |
. . . . . . 7
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ β( β₯
βπ)) = π) |
37 | 36 | oveq2d 7420 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (( β₯ βπ) β§ ( β₯ β( β₯
βπ))) = (( β₯
βπ) β§ π)) |
38 | 37 | oveq2d 7420 |
. . . . 5
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (( β₯ βπ)(joinβπΎ)(( β₯ βπ) β§ ( β₯ β( β₯
βπ)))) = (( β₯
βπ)(joinβπΎ)(( β₯ βπ) β§ π))) |
39 | 30, 34, 38 | 3eqtr4d 2783 |
. . . 4
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ β(( β₯
β(( β₯ βπ) β§ π)) β§ π)) = (( β₯ βπ)(joinβπΎ)(( β₯ βπ) β§ ( β₯ β( β₯
βπ))))) |
40 | 39 | eqeq2d 2744 |
. . 3
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (( β₯ βπ) = ( β₯ β(( β₯
β(( β₯ βπ) β§ π)) β§ π)) β ( β₯ βπ) = (( β₯ βπ)(joinβπΎ)(( β₯ βπ) β§ ( β₯ β( β₯
βπ)))))) |
41 | 28, 40 | bitrd 279 |
. 2
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((( β₯ β(( β₯
βπ) β§ π)) β§ π) = π β ( β₯ βπ) = (( β₯ βπ)(joinβπΎ)(( β₯ βπ) β§ ( β₯ β( β₯
βπ)))))) |
42 | 16, 18, 41 | 3imtr4d 294 |
1
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β (( β₯ β(( β₯
βπ) β§ π)) β§ π) = π)) |