Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . 5
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
2 | | isdlat.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | 1, 2 | eqtr4di 2791 |
. . . 4
β’ (π = πΎ β (Baseβπ) = π΅) |
4 | | fveq2 6846 |
. . . . . 6
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
5 | | isdlat.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
6 | 4, 5 | eqtr4di 2791 |
. . . . 5
β’ (π = πΎ β (joinβπ) = β¨ ) |
7 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΎ β (meetβπ) = (meetβπΎ)) |
8 | | isdlat.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΎ β (meetβπ) = β§ ) |
10 | 9 | sbceq1d 3748 |
. . . . 5
β’ (π = πΎ β ([(meetβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β [ β§ / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)))) |
11 | 6, 10 | sbceqbid 3750 |
. . . 4
β’ (π = πΎ β ([(joinβπ) / π][(meetβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β [ β¨ / π][ β§ / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)))) |
12 | 3, 11 | sbceqbid 3750 |
. . 3
β’ (π = πΎ β ([(Baseβπ) / π][(joinβπ) / π][(meetβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β [π΅ / π][ β¨ / π][ β§ / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)))) |
13 | 2 | fvexi 6860 |
. . . 4
β’ π΅ β V |
14 | 5 | fvexi 6860 |
. . . 4
β’ β¨ β
V |
15 | 8 | fvexi 6860 |
. . . 4
β’ β§ β
V |
16 | | raleq 3308 |
. . . . . . . 8
β’ (π = π΅ β (βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β βπ§ β π΅ (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)))) |
17 | 16 | raleqbi1dv 3306 |
. . . . . . 7
β’ (π = π΅ β (βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β βπ¦ β π΅ βπ§ β π΅ (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)))) |
18 | 17 | raleqbi1dv 3306 |
. . . . . 6
β’ (π = π΅ β (βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)))) |
19 | | simpr 486 |
. . . . . . . . . 10
β’ ((π = β¨ β§ π = β§ ) β π = β§ ) |
20 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π = β¨ β§ π = β§ ) β π₯ = π₯) |
21 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π = β¨ β§ π = β§ ) β π = β¨ ) |
22 | 21 | oveqd 7378 |
. . . . . . . . . 10
β’ ((π = β¨ β§ π = β§ ) β (π¦ππ§) = (π¦ β¨ π§)) |
23 | 19, 20, 22 | oveq123d 7382 |
. . . . . . . . 9
β’ ((π = β¨ β§ π = β§ ) β (π₯π(π¦ππ§)) = (π₯ β§ (π¦ β¨ π§))) |
24 | 19 | oveqd 7378 |
. . . . . . . . . 10
β’ ((π = β¨ β§ π = β§ ) β (π₯ππ¦) = (π₯ β§ π¦)) |
25 | 19 | oveqd 7378 |
. . . . . . . . . 10
β’ ((π = β¨ β§ π = β§ ) β (π₯ππ§) = (π₯ β§ π§)) |
26 | 21, 24, 25 | oveq123d 7382 |
. . . . . . . . 9
β’ ((π = β¨ β§ π = β§ ) β ((π₯ππ¦)π(π₯ππ§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§))) |
27 | 23, 26 | eqeq12d 2749 |
. . . . . . . 8
β’ ((π = β¨ β§ π = β§ ) β ((π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) |
28 | 27 | ralbidv 3171 |
. . . . . . 7
β’ ((π = β¨ β§ π = β§ ) β
(βπ§ β π΅ (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) |
29 | 28 | 2ralbidv 3209 |
. . . . . 6
β’ ((π = β¨ β§ π = β§ ) β
(βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) |
30 | 18, 29 | sylan9bb 511 |
. . . . 5
β’ ((π = π΅ β§ (π = β¨ β§ π = β§ )) β
(βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) |
31 | 30 | 3impb 1116 |
. . . 4
β’ ((π = π΅ β§ π = β¨ β§ π = β§ ) β
(βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) |
32 | 13, 14, 15, 31 | sbc3ie 3829 |
. . 3
β’
([π΅ / π][ β¨ / π][ β§ / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§))) |
33 | 12, 32 | bitrdi 287 |
. 2
β’ (π = πΎ β ([(Baseβπ) / π][(joinβπ) / π][(meetβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) |
34 | | df-dlat 18418 |
. 2
β’ DLat =
{π β Lat β£
[(Baseβπ) /
π][(joinβπ) / π][(meetβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π (π₯π(π¦ππ§)) = ((π₯ππ¦)π(π₯ππ§))} |
35 | 33, 34 | elrab2 3652 |
1
β’ (πΎ β DLat β (πΎ β Lat β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β§ (π¦ β¨ π§)) = ((π₯ β§ π¦) β¨ (π₯ β§ π§)))) |