Step | Hyp | Ref
| Expression |
1 | | latdisd.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΎ) |
2 | | latdisd.m |
. . . . . . . . 9
β’ β§ =
(meetβπΎ) |
3 | 1, 2 | latmcl 18389 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ β§ π¦) β π΅) |
4 | 3 | 3adant3r3 1184 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ β§ π¦) β π΅) |
5 | | simpr1 1194 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β π₯ β π΅) |
6 | | simpr3 1196 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β π§ β π΅) |
7 | | oveq1 7412 |
. . . . . . . . 9
β’ (π’ = (π₯ β§ π¦) β (π’ β¨ (π£ β§ π€)) = ((π₯ β§ π¦) β¨ (π£ β§ π€))) |
8 | | oveq1 7412 |
. . . . . . . . . 10
β’ (π’ = (π₯ β§ π¦) β (π’ β¨ π£) = ((π₯ β§ π¦) β¨ π£)) |
9 | | oveq1 7412 |
. . . . . . . . . 10
β’ (π’ = (π₯ β§ π¦) β (π’ β¨ π€) = ((π₯ β§ π¦) β¨ π€)) |
10 | 8, 9 | oveq12d 7423 |
. . . . . . . . 9
β’ (π’ = (π₯ β§ π¦) β ((π’ β¨ π£) β§ (π’ β¨ π€)) = (((π₯ β§ π¦) β¨ π£) β§ ((π₯ β§ π¦) β¨ π€))) |
11 | 7, 10 | eqeq12d 2748 |
. . . . . . . 8
β’ (π’ = (π₯ β§ π¦) β ((π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€)) β ((π₯ β§ π¦) β¨ (π£ β§ π€)) = (((π₯ β§ π¦) β¨ π£) β§ ((π₯ β§ π¦) β¨ π€)))) |
12 | | oveq1 7412 |
. . . . . . . . . 10
β’ (π£ = π₯ β (π£ β§ π€) = (π₯ β§ π€)) |
13 | 12 | oveq2d 7421 |
. . . . . . . . 9
β’ (π£ = π₯ β ((π₯ β§ π¦) β¨ (π£ β§ π€)) = ((π₯ β§ π¦) β¨ (π₯ β§ π€))) |
14 | | oveq2 7413 |
. . . . . . . . . 10
β’ (π£ = π₯ β ((π₯ β§ π¦) β¨ π£) = ((π₯ β§ π¦) β¨ π₯)) |
15 | 14 | oveq1d 7420 |
. . . . . . . . 9
β’ (π£ = π₯ β (((π₯ β§ π¦) β¨ π£) β§ ((π₯ β§ π¦) β¨ π€)) = (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π€))) |
16 | 13, 15 | eqeq12d 2748 |
. . . . . . . 8
β’ (π£ = π₯ β (((π₯ β§ π¦) β¨ (π£ β§ π€)) = (((π₯ β§ π¦) β¨ π£) β§ ((π₯ β§ π¦) β¨ π€)) β ((π₯ β§ π¦) β¨ (π₯ β§ π€)) = (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π€)))) |
17 | | oveq2 7413 |
. . . . . . . . . 10
β’ (π€ = π§ β (π₯ β§ π€) = (π₯ β§ π§)) |
18 | 17 | oveq2d 7421 |
. . . . . . . . 9
β’ (π€ = π§ β ((π₯ β§ π¦) β¨ (π₯ β§ π€)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§))) |
19 | | oveq2 7413 |
. . . . . . . . . 10
β’ (π€ = π§ β ((π₯ β§ π¦) β¨ π€) = ((π₯ β§ π¦) β¨ π§)) |
20 | 19 | oveq2d 7421 |
. . . . . . . . 9
β’ (π€ = π§ β (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π€)) = (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π§))) |
21 | 18, 20 | eqeq12d 2748 |
. . . . . . . 8
β’ (π€ = π§ β (((π₯ β§ π¦) β¨ (π₯ β§ π€)) = (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π€)) β ((π₯ β§ π¦) β¨ (π₯ β§ π§)) = (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π§)))) |
22 | 11, 16, 21 | rspc3v 3626 |
. . . . . . 7
β’ (((π₯ β§ π¦) β π΅ β§ π₯ β π΅ β§ π§ β π΅) β (βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€)) β ((π₯ β§ π¦) β¨ (π₯ β§ π§)) = (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π§)))) |
23 | 4, 5, 6, 22 | syl3anc 1371 |
. . . . . 6
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€)) β ((π₯ β§ π¦) β¨ (π₯ β§ π§)) = (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π§)))) |
24 | 23 | imp 407 |
. . . . 5
β’ (((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β§ βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€))) β ((π₯ β§ π¦) β¨ (π₯ β§ π§)) = (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π§))) |
25 | | simpl 483 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β πΎ β Lat) |
26 | | latdisd.j |
. . . . . . . . . 10
β’ β¨ =
(joinβπΎ) |
27 | 1, 26 | latjcom 18396 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π₯ β§ π¦) β π΅ β§ π₯ β π΅) β ((π₯ β§ π¦) β¨ π₯) = (π₯ β¨ (π₯ β§ π¦))) |
28 | 25, 4, 5, 27 | syl3anc 1371 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ β§ π¦) β¨ π₯) = (π₯ β¨ (π₯ β§ π¦))) |
29 | 1, 26, 2 | latabs1 18424 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ β¨ (π₯ β§ π¦)) = π₯) |
30 | 29 | 3adant3r3 1184 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ β¨ (π₯ β§ π¦)) = π₯) |
31 | 28, 30 | eqtrd 2772 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ β§ π¦) β¨ π₯) = π₯) |
32 | 1, 26 | latjcom 18396 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π₯ β§ π¦) β π΅ β§ π§ β π΅) β ((π₯ β§ π¦) β¨ π§) = (π§ β¨ (π₯ β§ π¦))) |
33 | 25, 4, 6, 32 | syl3anc 1371 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ β§ π¦) β¨ π§) = (π§ β¨ (π₯ β§ π¦))) |
34 | 31, 33 | oveq12d 7423 |
. . . . . 6
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π§)) = (π₯ β§ (π§ β¨ (π₯ β§ π¦)))) |
35 | 34 | adantr 481 |
. . . . 5
β’ (((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β§ βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€))) β (((π₯ β§ π¦) β¨ π₯) β§ ((π₯ β§ π¦) β¨ π§)) = (π₯ β§ (π§ β¨ (π₯ β§ π¦)))) |
36 | | simpr2 1195 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β π¦ β π΅) |
37 | | oveq1 7412 |
. . . . . . . . . . 11
β’ (π’ = π§ β (π’ β¨ (π£ β§ π€)) = (π§ β¨ (π£ β§ π€))) |
38 | | oveq1 7412 |
. . . . . . . . . . . 12
β’ (π’ = π§ β (π’ β¨ π£) = (π§ β¨ π£)) |
39 | | oveq1 7412 |
. . . . . . . . . . . 12
β’ (π’ = π§ β (π’ β¨ π€) = (π§ β¨ π€)) |
40 | 38, 39 | oveq12d 7423 |
. . . . . . . . . . 11
β’ (π’ = π§ β ((π’ β¨ π£) β§ (π’ β¨ π€)) = ((π§ β¨ π£) β§ (π§ β¨ π€))) |
41 | 37, 40 | eqeq12d 2748 |
. . . . . . . . . 10
β’ (π’ = π§ β ((π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€)) β (π§ β¨ (π£ β§ π€)) = ((π§ β¨ π£) β§ (π§ β¨ π€)))) |
42 | 12 | oveq2d 7421 |
. . . . . . . . . . 11
β’ (π£ = π₯ β (π§ β¨ (π£ β§ π€)) = (π§ β¨ (π₯ β§ π€))) |
43 | | oveq2 7413 |
. . . . . . . . . . . 12
β’ (π£ = π₯ β (π§ β¨ π£) = (π§ β¨ π₯)) |
44 | 43 | oveq1d 7420 |
. . . . . . . . . . 11
β’ (π£ = π₯ β ((π§ β¨ π£) β§ (π§ β¨ π€)) = ((π§ β¨ π₯) β§ (π§ β¨ π€))) |
45 | 42, 44 | eqeq12d 2748 |
. . . . . . . . . 10
β’ (π£ = π₯ β ((π§ β¨ (π£ β§ π€)) = ((π§ β¨ π£) β§ (π§ β¨ π€)) β (π§ β¨ (π₯ β§ π€)) = ((π§ β¨ π₯) β§ (π§ β¨ π€)))) |
46 | | oveq2 7413 |
. . . . . . . . . . . 12
β’ (π€ = π¦ β (π₯ β§ π€) = (π₯ β§ π¦)) |
47 | 46 | oveq2d 7421 |
. . . . . . . . . . 11
β’ (π€ = π¦ β (π§ β¨ (π₯ β§ π€)) = (π§ β¨ (π₯ β§ π¦))) |
48 | | oveq2 7413 |
. . . . . . . . . . . 12
β’ (π€ = π¦ β (π§ β¨ π€) = (π§ β¨ π¦)) |
49 | 48 | oveq2d 7421 |
. . . . . . . . . . 11
β’ (π€ = π¦ β ((π§ β¨ π₯) β§ (π§ β¨ π€)) = ((π§ β¨ π₯) β§ (π§ β¨ π¦))) |
50 | 47, 49 | eqeq12d 2748 |
. . . . . . . . . 10
β’ (π€ = π¦ β ((π§ β¨ (π₯ β§ π€)) = ((π§ β¨ π₯) β§ (π§ β¨ π€)) β (π§ β¨ (π₯ β§ π¦)) = ((π§ β¨ π₯) β§ (π§ β¨ π¦)))) |
51 | 41, 45, 50 | rspc3v 3626 |
. . . . . . . . 9
β’ ((π§ β π΅ β§ π₯ β π΅ β§ π¦ β π΅) β (βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€)) β (π§ β¨ (π₯ β§ π¦)) = ((π§ β¨ π₯) β§ (π§ β¨ π¦)))) |
52 | 6, 5, 36, 51 | syl3anc 1371 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€)) β (π§ β¨ (π₯ β§ π¦)) = ((π§ β¨ π₯) β§ (π§ β¨ π¦)))) |
53 | 52 | imp 407 |
. . . . . . 7
β’ (((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β§ βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€))) β (π§ β¨ (π₯ β§ π¦)) = ((π§ β¨ π₯) β§ (π§ β¨ π¦))) |
54 | 53 | oveq2d 7421 |
. . . . . 6
β’ (((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β§ βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€))) β (π₯ β§ (π§ β¨ (π₯ β§ π¦))) = (π₯ β§ ((π§ β¨ π₯) β§ (π§ β¨ π¦)))) |
55 | 1, 26 | latjcl 18388 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π§ β π΅ β§ π₯ β π΅) β (π§ β¨ π₯) β π΅) |
56 | 25, 6, 5, 55 | syl3anc 1371 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π§ β¨ π₯) β π΅) |
57 | 1, 26 | latjcl 18388 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π§ β π΅ β§ π¦ β π΅) β (π§ β¨ π¦) β π΅) |
58 | 25, 6, 36, 57 | syl3anc 1371 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π§ β¨ π¦) β π΅) |
59 | 1, 2 | latmass 18444 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ (π§ β¨ π₯) β π΅ β§ (π§ β¨ π¦) β π΅)) β ((π₯ β§ (π§ β¨ π₯)) β§ (π§ β¨ π¦)) = (π₯ β§ ((π§ β¨ π₯) β§ (π§ β¨ π¦)))) |
60 | 25, 5, 56, 58, 59 | syl13anc 1372 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ β§ (π§ β¨ π₯)) β§ (π§ β¨ π¦)) = (π₯ β§ ((π§ β¨ π₯) β§ (π§ β¨ π¦)))) |
61 | 1, 26 | latjcom 18396 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ π§ β π΅ β§ π₯ β π΅) β (π§ β¨ π₯) = (π₯ β¨ π§)) |
62 | 25, 6, 5, 61 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π§ β¨ π₯) = (π₯ β¨ π§)) |
63 | 62 | oveq2d 7421 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ β§ (π§ β¨ π₯)) = (π₯ β§ (π₯ β¨ π§))) |
64 | 1, 26, 2 | latabs2 18425 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ π₯ β π΅ β§ π§ β π΅) β (π₯ β§ (π₯ β¨ π§)) = π₯) |
65 | 25, 5, 6, 64 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ β§ (π₯ β¨ π§)) = π₯) |
66 | 63, 65 | eqtrd 2772 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ β§ (π§ β¨ π₯)) = π₯) |
67 | 1, 26 | latjcom 18396 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π§ β π΅ β§ π¦ β π΅) β (π§ β¨ π¦) = (π¦ β¨ π§)) |
68 | 25, 6, 36, 67 | syl3anc 1371 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π§ β¨ π¦) = (π¦ β¨ π§)) |
69 | 66, 68 | oveq12d 7423 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ β§ (π§ β¨ π₯)) β§ (π§ β¨ π¦)) = (π₯ β§ (π¦ β¨ π§))) |
70 | 60, 69 | eqtr3d 2774 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ β§ ((π§ β¨ π₯) β§ (π§ β¨ π¦))) = (π₯ β§ (π¦ β¨ π§))) |
71 | 70 | adantr 481 |
. . . . . 6
β’ (((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β§ βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€))) β (π₯ β§ ((π§ β¨ π₯) β§ (π§ β¨ π¦))) = (π₯ β§ (π¦ β¨ π§))) |
72 | 54, 71 | eqtrd 2772 |
. . . . 5
β’ (((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β§ βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€))) β (π₯ β§ (π§ β¨ (π₯ β§ π¦))) = (π₯ β§ (π¦ β¨ π§))) |
73 | 24, 35, 72 | 3eqtrrd 2777 |
. . . 4
β’ (((πΎ β Lat β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β§ βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€))) β (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§))) |
74 | 73 | an32s 650 |
. . 3
β’ (((πΎ β Lat β§ βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€))) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§))) |
75 | 74 | ralrimivvva 3203 |
. 2
β’ ((πΎ β Lat β§ βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€))) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§))) |
76 | 75 | ex 413 |
1
β’ (πΎ β Lat β
(βπ’ β π΅ βπ£ β π΅ βπ€ β π΅ (π’ β¨ (π£ β§ π€)) = ((π’ β¨ π£) β§ (π’ β¨ π€)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) |