Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β πΎ β OML) |
2 | | simp23 1209 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β π β π΅) |
3 | | simp21 1207 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β π β π΅) |
4 | | simp22 1208 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β π β π΅) |
5 | | simp3l 1202 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β π β€ π) |
6 | | omlmod.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
7 | | omlmod.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
8 | | omlmod.c |
. . . . . . 7
β’ πΆ = (cmβπΎ) |
9 | 6, 7, 8 | lecmtN 37764 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β ππΆπ)) |
10 | 1, 3, 2, 9 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β€ π β ππΆπ)) |
11 | 5, 10 | mpd 15 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β ππΆπ) |
12 | 6, 8 | cmtcomN 37757 |
. . . . 5
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆπ)) |
13 | 1, 3, 2, 12 | syl3anc 1372 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (ππΆπ β ππΆπ)) |
14 | 11, 13 | mpbid 231 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β ππΆπ) |
15 | | simp3r 1203 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β ππΆπ) |
16 | 6, 8 | cmtcomN 37757 |
. . . . 5
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆπ)) |
17 | 1, 4, 2, 16 | syl3anc 1372 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (ππΆπ β ππΆπ)) |
18 | 15, 17 | mpbid 231 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β ππΆπ) |
19 | | omlmod.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
20 | | omlmod.m |
. . . 4
β’ β§ =
(meetβπΎ) |
21 | 6, 19, 20, 8 | omlfh1N 37766 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π))) |
22 | 1, 2, 3, 4, 14, 18, 21 | syl132anc 1389 |
. 2
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π))) |
23 | | omllat 37750 |
. . . 4
β’ (πΎ β OML β πΎ β Lat) |
24 | 23 | 3ad2ant1 1134 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β πΎ β Lat) |
25 | 6, 19 | latjcl 18333 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
26 | 24, 3, 4, 25 | syl3anc 1372 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β¨ π) β π΅) |
27 | 6, 20 | latmcom 18357 |
. . 3
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π β§ (π β¨ π)) = ((π β¨ π) β§ π)) |
28 | 24, 2, 26, 27 | syl3anc 1372 |
. 2
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β§ (π β¨ π)) = ((π β¨ π) β§ π)) |
29 | 6, 7, 20 | latleeqm2 18362 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β€ π β (π β§ π) = π)) |
30 | 24, 3, 2, 29 | syl3anc 1372 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β€ π β (π β§ π) = π)) |
31 | 5, 30 | mpbid 231 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β§ π) = π) |
32 | 6, 20 | latmcom 18357 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) = (π β§ π)) |
33 | 24, 2, 4, 32 | syl3anc 1372 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β§ π) = (π β§ π)) |
34 | 31, 33 | oveq12d 7376 |
. 2
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β ((π β§ π) β¨ (π β§ π)) = (π β¨ (π β§ π))) |
35 | 22, 28, 34 | 3eqtr3rd 2782 |
1
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ ππΆπ)) β (π β¨ (π β§ π)) = ((π β¨ π) β§ π)) |