Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β π΅ β πΎ β V) |
2 | | dilset.l |
. . 3
β’ πΏ = (DilβπΎ) |
3 | | fveq2 6843 |
. . . . . 6
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
4 | | dilset.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
β’ (π = πΎ β (Atomsβπ) = π΄) |
6 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΎ β (PAutβπ) = (PAutβπΎ)) |
7 | | dilset.m |
. . . . . . 7
β’ π = (PAutβπΎ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . 6
β’ (π = πΎ β (PAutβπ) = π) |
9 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (PSubSpβπ) = (PSubSpβπΎ)) |
10 | | dilset.s |
. . . . . . . 8
β’ π = (PSubSpβπΎ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (PSubSpβπ) = π) |
12 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = πΎ β (WAtomsβπ) = (WAtomsβπΎ)) |
13 | | dilset.w |
. . . . . . . . . . 11
β’ π = (WAtomsβπΎ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = πΎ β (WAtomsβπ) = π) |
15 | 14 | fveq1d 6845 |
. . . . . . . . 9
β’ (π = πΎ β ((WAtomsβπ)βπ) = (πβπ)) |
16 | 15 | sseq2d 3977 |
. . . . . . . 8
β’ (π = πΎ β (π₯ β ((WAtomsβπ)βπ) β π₯ β (πβπ))) |
17 | 16 | imbi1d 342 |
. . . . . . 7
β’ (π = πΎ β ((π₯ β ((WAtomsβπ)βπ) β (πβπ₯) = π₯) β (π₯ β (πβπ) β (πβπ₯) = π₯))) |
18 | 11, 17 | raleqbidv 3320 |
. . . . . 6
β’ (π = πΎ β (βπ₯ β (PSubSpβπ)(π₯ β ((WAtomsβπ)βπ) β (πβπ₯) = π₯) β βπ₯ β π (π₯ β (πβπ) β (πβπ₯) = π₯))) |
19 | 8, 18 | rabeqbidv 3425 |
. . . . 5
β’ (π = πΎ β {π β (PAutβπ) β£ βπ₯ β (PSubSpβπ)(π₯ β ((WAtomsβπ)βπ) β (πβπ₯) = π₯)} = {π β π β£ βπ₯ β π (π₯ β (πβπ) β (πβπ₯) = π₯)}) |
20 | 5, 19 | mpteq12dv 5197 |
. . . 4
β’ (π = πΎ β (π β (Atomsβπ) β¦ {π β (PAutβπ) β£ βπ₯ β (PSubSpβπ)(π₯ β ((WAtomsβπ)βπ) β (πβπ₯) = π₯)}) = (π β π΄ β¦ {π β π β£ βπ₯ β π (π₯ β (πβπ) β (πβπ₯) = π₯)})) |
21 | | df-dilN 38572 |
. . . 4
β’ Dil =
(π β V β¦ (π β (Atomsβπ) β¦ {π β (PAutβπ) β£ βπ₯ β (PSubSpβπ)(π₯ β ((WAtomsβπ)βπ) β (πβπ₯) = π₯)})) |
22 | 20, 21, 4 | mptfvmpt 7179 |
. . 3
β’ (πΎ β V β
(DilβπΎ) = (π β π΄ β¦ {π β π β£ βπ₯ β π (π₯ β (πβπ) β (πβπ₯) = π₯)})) |
23 | 2, 22 | eqtrid 2789 |
. 2
β’ (πΎ β V β πΏ = (π β π΄ β¦ {π β π β£ βπ₯ β π (π₯ β (πβπ) β (πβπ₯) = π₯)})) |
24 | 1, 23 | syl 17 |
1
β’ (πΎ β π΅ β πΏ = (π β π΄ β¦ {π β π β£ βπ₯ β π (π₯ β (πβπ) β (πβπ₯) = π₯)})) |