Step | Hyp | Ref
| Expression |
1 | | cmtbr2.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | cmtbr2.c |
. . . . 5
β’ πΆ = (cmβπΎ) |
3 | 1, 2 | cmtcomN 38422 |
. . . 4
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆπ)) |
4 | | cmtbr2.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
5 | | cmtbr2.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
6 | | cmtbr2.o |
. . . . . 6
β’ β₯ =
(ocβπΎ) |
7 | 1, 4, 5, 6, 2 | cmtbr2N 38426 |
. . . . 5
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β π = ((π β¨ π) β§ (π β¨ ( β₯ βπ))))) |
8 | 7 | 3com23 1126 |
. . . 4
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β π = ((π β¨ π) β§ (π β¨ ( β₯ βπ))))) |
9 | 3, 8 | bitrd 278 |
. . 3
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β π = ((π β¨ π) β§ (π β¨ ( β₯ βπ))))) |
10 | | oveq2 7419 |
. . . . . 6
β’ (π = ((π β¨ π) β§ (π β¨ ( β₯ βπ))) β (π β§ π) = (π β§ ((π β¨ π) β§ (π β¨ ( β₯ βπ))))) |
11 | 10 | adantl 482 |
. . . . 5
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ π = ((π β¨ π) β§ (π β¨ ( β₯ βπ)))) β (π β§ π) = (π β§ ((π β¨ π) β§ (π β¨ ( β₯ βπ))))) |
12 | | omlol 38413 |
. . . . . . . . 9
β’ (πΎ β OML β πΎ β OL) |
13 | 12 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β πΎ β OL) |
14 | | simp2 1137 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β π β π΅) |
15 | | omllat 38415 |
. . . . . . . . . 10
β’ (πΎ β OML β πΎ β Lat) |
16 | 15 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β πΎ β Lat) |
17 | | simp3 1138 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β π β π΅) |
18 | 1, 4 | latjcl 18396 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
19 | 16, 17, 14, 18 | syl3anc 1371 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
20 | | omlop 38414 |
. . . . . . . . . . 11
β’ (πΎ β OML β πΎ β OP) |
21 | 20 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β πΎ β OP) |
22 | 1, 6 | opoccl 38367 |
. . . . . . . . . 10
β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) |
23 | 21, 14, 22 | syl2anc 584 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ βπ) β π΅) |
24 | 1, 4 | latjcl 18396 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ ( β₯ βπ) β π΅) β (π β¨ ( β₯ βπ)) β π΅) |
25 | 16, 17, 23, 24 | syl3anc 1371 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β¨ ( β₯ βπ)) β π΅) |
26 | 1, 5 | latmassOLD 38402 |
. . . . . . . 8
β’ ((πΎ β OL β§ (π β π΅ β§ (π β¨ π) β π΅ β§ (π β¨ ( β₯ βπ)) β π΅)) β ((π β§ (π β¨ π)) β§ (π β¨ ( β₯ βπ))) = (π β§ ((π β¨ π) β§ (π β¨ ( β₯ βπ))))) |
27 | 13, 14, 19, 25, 26 | syl13anc 1372 |
. . . . . . 7
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β§ (π β¨ π)) β§ (π β¨ ( β₯ βπ))) = (π β§ ((π β¨ π) β§ (π β¨ ( β₯ βπ))))) |
28 | 1, 4 | latjcom 18404 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) |
29 | 16, 17, 14, 28 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) |
30 | 29 | oveq2d 7427 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β§ (π β¨ π)) = (π β§ (π β¨ π))) |
31 | 1, 4, 5 | latabs2 18433 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ (π β¨ π)) = π) |
32 | 15, 31 | syl3an1 1163 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β§ (π β¨ π)) = π) |
33 | 30, 32 | eqtrd 2772 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β§ (π β¨ π)) = π) |
34 | 1, 4 | latjcom 18404 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ ( β₯ βπ) β π΅) β (π β¨ ( β₯ βπ)) = (( β₯ βπ) β¨ π)) |
35 | 16, 17, 23, 34 | syl3anc 1371 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β¨ ( β₯ βπ)) = (( β₯ βπ) β¨ π)) |
36 | 33, 35 | oveq12d 7429 |
. . . . . . 7
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β§ (π β¨ π)) β§ (π β¨ ( β₯ βπ))) = (π β§ (( β₯ βπ) β¨ π))) |
37 | 27, 36 | eqtr3d 2774 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β§ ((π β¨ π) β§ (π β¨ ( β₯ βπ)))) = (π β§ (( β₯ βπ) β¨ π))) |
38 | 37 | adantr 481 |
. . . . 5
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ π = ((π β¨ π) β§ (π β¨ ( β₯ βπ)))) β (π β§ ((π β¨ π) β§ (π β¨ ( β₯ βπ)))) = (π β§ (( β₯ βπ) β¨ π))) |
39 | 11, 38 | eqtr2d 2773 |
. . . 4
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ π = ((π β¨ π) β§ (π β¨ ( β₯ βπ)))) β (π β§ (( β₯ βπ) β¨ π)) = (π β§ π)) |
40 | 39 | ex 413 |
. . 3
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π = ((π β¨ π) β§ (π β¨ ( β₯ βπ))) β (π β§ (( β₯ βπ) β¨ π)) = (π β§ π))) |
41 | 9, 40 | sylbid 239 |
. 2
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β (π β§ (( β₯ βπ) β¨ π)) = (π β§ π))) |
42 | | simp1 1136 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β πΎ β OML) |
43 | 1, 6 | opoccl 38367 |
. . . . . . . . . . 11
β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) |
44 | 21, 17, 43 | syl2anc 584 |
. . . . . . . . . 10
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ βπ) β π΅) |
45 | 1, 5 | latmcl 18397 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β π΅ β§ ( β₯ βπ) β π΅) β (π β§ ( β₯ βπ)) β π΅) |
46 | 16, 14, 44, 45 | syl3anc 1371 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β§ ( β₯ βπ)) β π΅) |
47 | 42, 46, 14 | 3jca 1128 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (πΎ β OML β§ (π β§ ( β₯ βπ)) β π΅ β§ π β π΅)) |
48 | | eqid 2732 |
. . . . . . . . . 10
β’
(leβπΎ) =
(leβπΎ) |
49 | 1, 48, 5 | latmle1 18421 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ ( β₯ βπ) β π΅) β (π β§ ( β₯ βπ))(leβπΎ)π) |
50 | 16, 14, 44, 49 | syl3anc 1371 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β§ ( β₯ βπ))(leβπΎ)π) |
51 | 1, 48, 4, 5, 6 | omllaw2N 38417 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β§ ( β₯ βπ)) β π΅ β§ π β π΅) β ((π β§ ( β₯ βπ))(leβπΎ)π β ((π β§ ( β₯ βπ)) β¨ (( β₯ β(π β§ ( β₯ βπ))) β§ π)) = π)) |
52 | 47, 50, 51 | sylc 65 |
. . . . . . 7
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β§ ( β₯ βπ)) β¨ (( β₯ β(π β§ ( β₯ βπ))) β§ π)) = π) |
53 | 1, 6 | opoccl 38367 |
. . . . . . . . . 10
β’ ((πΎ β OP β§ (π β§ ( β₯ βπ)) β π΅) β ( β₯ β(π β§ ( β₯ βπ))) β π΅) |
54 | 21, 46, 53 | syl2anc 584 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ β(π β§ ( β₯ βπ))) β π΅) |
55 | 1, 5 | latmcl 18397 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ ( β₯
β(π β§ ( β₯
βπ))) β π΅ β§ π β π΅) β (( β₯ β(π β§ ( β₯ βπ))) β§ π) β π΅) |
56 | 16, 54, 14, 55 | syl3anc 1371 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (( β₯ β(π β§ ( β₯ βπ))) β§ π) β π΅) |
57 | 1, 4 | latjcom 18404 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β§ ( β₯ βπ)) β π΅ β§ (( β₯ β(π β§ ( β₯ βπ))) β§ π) β π΅) β ((π β§ ( β₯ βπ)) β¨ (( β₯ β(π β§ ( β₯ βπ))) β§ π)) = ((( β₯ β(π β§ ( β₯ βπ))) β§ π) β¨ (π β§ ( β₯ βπ)))) |
58 | 16, 46, 56, 57 | syl3anc 1371 |
. . . . . . 7
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β§ ( β₯ βπ)) β¨ (( β₯ β(π β§ ( β₯ βπ))) β§ π)) = ((( β₯ β(π β§ ( β₯ βπ))) β§ π) β¨ (π β§ ( β₯ βπ)))) |
59 | 52, 58 | eqtr3d 2774 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β π = ((( β₯ β(π β§ ( β₯ βπ))) β§ π) β¨ (π β§ ( β₯ βπ)))) |
60 | 59 | adantr 481 |
. . . . 5
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ (π β§ (( β₯ βπ) β¨ π)) = (π β§ π)) β π = ((( β₯ β(π β§ ( β₯ βπ))) β§ π) β¨ (π β§ ( β₯ βπ)))) |
61 | 1, 4, 5, 6 | oldmm3N 38392 |
. . . . . . . . . . 11
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ( β₯ β(π β§ ( β₯ βπ))) = (( β₯ βπ) β¨ π)) |
62 | 12, 61 | syl3an1 1163 |
. . . . . . . . . 10
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ( β₯ β(π β§ ( β₯ βπ))) = (( β₯ βπ) β¨ π)) |
63 | 62 | oveq2d 7427 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β§ ( β₯ β(π β§ ( β₯ βπ)))) = (π β§ (( β₯ βπ) β¨ π))) |
64 | 1, 5 | latmcom 18420 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β π΅ β§ ( β₯ β(π β§ ( β₯ βπ))) β π΅) β (π β§ ( β₯ β(π β§ ( β₯ βπ)))) = (( β₯ β(π β§ ( β₯ βπ))) β§ π)) |
65 | 16, 14, 54, 64 | syl3anc 1371 |
. . . . . . . . 9
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β§ ( β₯ β(π β§ ( β₯ βπ)))) = (( β₯ β(π β§ ( β₯ βπ))) β§ π)) |
66 | 63, 65 | eqtr3d 2774 |
. . . . . . . 8
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β§ (( β₯ βπ) β¨ π)) = (( β₯ β(π β§ ( β₯ βπ))) β§ π)) |
67 | 66 | eqeq1d 2734 |
. . . . . . 7
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β§ (( β₯ βπ) β¨ π)) = (π β§ π) β (( β₯ β(π β§ ( β₯ βπ))) β§ π) = (π β§ π))) |
68 | | oveq1 7418 |
. . . . . . 7
β’ ((( β₯
β(π β§ ( β₯
βπ))) β§ π) = (π β§ π) β ((( β₯ β(π β§ ( β₯ βπ))) β§ π) β¨ (π β§ ( β₯ βπ))) = ((π β§ π) β¨ (π β§ ( β₯ βπ)))) |
69 | 67, 68 | syl6bi 252 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β§ (( β₯ βπ) β¨ π)) = (π β§ π) β ((( β₯ β(π β§ ( β₯ βπ))) β§ π) β¨ (π β§ ( β₯ βπ))) = ((π β§ π) β¨ (π β§ ( β₯ βπ))))) |
70 | 69 | imp 407 |
. . . . 5
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ (π β§ (( β₯ βπ) β¨ π)) = (π β§ π)) β ((( β₯ β(π β§ ( β₯ βπ))) β§ π) β¨ (π β§ ( β₯ βπ))) = ((π β§ π) β¨ (π β§ ( β₯ βπ)))) |
71 | 60, 70 | eqtrd 2772 |
. . . 4
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ (π β§ (( β₯ βπ) β¨ π)) = (π β§ π)) β π = ((π β§ π) β¨ (π β§ ( β₯ βπ)))) |
72 | 71 | ex 413 |
. . 3
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β§ (( β₯ βπ) β¨ π)) = (π β§ π) β π = ((π β§ π) β¨ (π β§ ( β₯ βπ))))) |
73 | 1, 4, 5, 6, 2 | cmtvalN 38384 |
. . 3
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β π = ((π β§ π) β¨ (π β§ ( β₯ βπ))))) |
74 | 72, 73 | sylibrd 258 |
. 2
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β§ (( β₯ βπ) β¨ π)) = (π β§ π) β ππΆπ)) |
75 | 41, 74 | impbid 211 |
1
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β (π β§ (( β₯ βπ) β¨ π)) = (π β§ π))) |