Step | Hyp | Ref
| Expression |
1 | | latjass.b |
. 2
β’ π΅ = (BaseβπΎ) |
2 | | eqid 2733 |
. 2
β’
(leβπΎ) =
(leβπΎ) |
3 | | simpl 484 |
. 2
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β Lat) |
4 | | latjass.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
5 | 1, 4 | latjcl 18333 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
6 | 5 | 3adant3r3 1185 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ π) β π΅) |
7 | | simpr3 1197 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
8 | 1, 4 | latjcl 18333 |
. . 3
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ π β π΅) β ((π β¨ π) β¨ π) β π΅) |
9 | 3, 6, 7, 8 | syl3anc 1372 |
. 2
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ π) β π΅) |
10 | | simpr1 1195 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
11 | 1, 4 | latjcl 18333 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
12 | 11 | 3adant3r1 1183 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ π) β π΅) |
13 | 1, 4 | latjcl 18333 |
. . 3
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π β¨ (π β¨ π)) β π΅) |
14 | 3, 10, 12, 13 | syl3anc 1372 |
. 2
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ (π β¨ π)) β π΅) |
15 | 1, 2, 4 | latlej1 18342 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β π(leβπΎ)(π β¨ (π β¨ π))) |
16 | 3, 10, 12, 15 | syl3anc 1372 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)(π β¨ (π β¨ π))) |
17 | | simpr2 1196 |
. . . . 5
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
18 | 1, 2, 4 | latlej1 18342 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π(leβπΎ)(π β¨ π)) |
19 | 18 | 3adant3r1 1183 |
. . . . 5
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)(π β¨ π)) |
20 | 1, 2, 4 | latlej2 18343 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π β¨ π)(leβπΎ)(π β¨ (π β¨ π))) |
21 | 3, 10, 12, 20 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ π)(leβπΎ)(π β¨ (π β¨ π))) |
22 | 1, 2, 3, 17, 12, 14, 19, 21 | lattrd 18340 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)(π β¨ (π β¨ π))) |
23 | 1, 2, 4 | latjle12 18344 |
. . . . 5
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ (π β¨ (π β¨ π)) β π΅)) β ((π(leβπΎ)(π β¨ (π β¨ π)) β§ π(leβπΎ)(π β¨ (π β¨ π))) β (π β¨ π)(leβπΎ)(π β¨ (π β¨ π)))) |
24 | 3, 10, 17, 14, 23 | syl13anc 1373 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(leβπΎ)(π β¨ (π β¨ π)) β§ π(leβπΎ)(π β¨ (π β¨ π))) β (π β¨ π)(leβπΎ)(π β¨ (π β¨ π)))) |
25 | 16, 22, 24 | mpbi2and 711 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ π)(leβπΎ)(π β¨ (π β¨ π))) |
26 | 1, 2, 4 | latlej2 18343 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π(leβπΎ)(π β¨ π)) |
27 | 26 | 3adant3r1 1183 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)(π β¨ π)) |
28 | 1, 2, 3, 7, 12, 14, 27, 21 | lattrd 18340 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)(π β¨ (π β¨ π))) |
29 | 1, 2, 4 | latjle12 18344 |
. . . 4
β’ ((πΎ β Lat β§ ((π β¨ π) β π΅ β§ π β π΅ β§ (π β¨ (π β¨ π)) β π΅)) β (((π β¨ π)(leβπΎ)(π β¨ (π β¨ π)) β§ π(leβπΎ)(π β¨ (π β¨ π))) β ((π β¨ π) β¨ π)(leβπΎ)(π β¨ (π β¨ π)))) |
30 | 3, 6, 7, 14, 29 | syl13anc 1373 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((π β¨ π)(leβπΎ)(π β¨ (π β¨ π)) β§ π(leβπΎ)(π β¨ (π β¨ π))) β ((π β¨ π) β¨ π)(leβπΎ)(π β¨ (π β¨ π)))) |
31 | 25, 28, 30 | mpbi2and 711 |
. 2
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ π)(leβπΎ)(π β¨ (π β¨ π))) |
32 | 1, 2, 4 | latlej1 18342 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π(leβπΎ)(π β¨ π)) |
33 | 32 | 3adant3r3 1185 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)(π β¨ π)) |
34 | 1, 2, 4 | latlej1 18342 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ π β π΅) β (π β¨ π)(leβπΎ)((π β¨ π) β¨ π)) |
35 | 3, 6, 7, 34 | syl3anc 1372 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ π)(leβπΎ)((π β¨ π) β¨ π)) |
36 | 1, 2, 3, 10, 6, 9,
33, 35 | lattrd 18340 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)((π β¨ π) β¨ π)) |
37 | 1, 2, 4 | latlej2 18343 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π(leβπΎ)(π β¨ π)) |
38 | 37 | 3adant3r3 1185 |
. . . . 5
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)(π β¨ π)) |
39 | 1, 2, 3, 17, 6, 9,
38, 35 | lattrd 18340 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)((π β¨ π) β¨ π)) |
40 | 1, 2, 4 | latlej2 18343 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ π β π΅) β π(leβπΎ)((π β¨ π) β¨ π)) |
41 | 3, 6, 7, 40 | syl3anc 1372 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π(leβπΎ)((π β¨ π) β¨ π)) |
42 | 1, 2, 4 | latjle12 18344 |
. . . . 5
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ ((π β¨ π) β¨ π) β π΅)) β ((π(leβπΎ)((π β¨ π) β¨ π) β§ π(leβπΎ)((π β¨ π) β¨ π)) β (π β¨ π)(leβπΎ)((π β¨ π) β¨ π))) |
43 | 3, 17, 7, 9, 42 | syl13anc 1373 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(leβπΎ)((π β¨ π) β¨ π) β§ π(leβπΎ)((π β¨ π) β¨ π)) β (π β¨ π)(leβπΎ)((π β¨ π) β¨ π))) |
44 | 39, 41, 43 | mpbi2and 711 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ π)(leβπΎ)((π β¨ π) β¨ π)) |
45 | 1, 2, 4 | latjle12 18344 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΅ β§ (π β¨ π) β π΅ β§ ((π β¨ π) β¨ π) β π΅)) β ((π(leβπΎ)((π β¨ π) β¨ π) β§ (π β¨ π)(leβπΎ)((π β¨ π) β¨ π)) β (π β¨ (π β¨ π))(leβπΎ)((π β¨ π) β¨ π))) |
46 | 3, 10, 12, 9, 45 | syl13anc 1373 |
. . 3
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(leβπΎ)((π β¨ π) β¨ π) β§ (π β¨ π)(leβπΎ)((π β¨ π) β¨ π)) β (π β¨ (π β¨ π))(leβπΎ)((π β¨ π) β¨ π))) |
47 | 36, 44, 46 | mpbi2and 711 |
. 2
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ (π β¨ π))(leβπΎ)((π β¨ π) β¨ π)) |
48 | 1, 2, 3, 9, 14, 31, 47 | latasymd 18339 |
1
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ π) = (π β¨ (π β¨ π))) |