Step | Hyp | Ref
| Expression |
1 | | mapdval.k |
. . . 4
β’ (π β (πΎ β π β§ π β π»)) |
2 | | mapdval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
3 | | mapdval.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
4 | | mapdval.s |
. . . . 5
β’ π = (LSubSpβπ) |
5 | | mapdval.f |
. . . . 5
β’ πΉ = (LFnlβπ) |
6 | | mapdval.l |
. . . . 5
β’ πΏ = (LKerβπ) |
7 | | mapdval.o |
. . . . 5
β’ π = ((ocHβπΎ)βπ) |
8 | | mapdval.m |
. . . . 5
β’ π = ((mapdβπΎ)βπ) |
9 | 2, 3, 4, 5, 6, 7, 8 | mapdfval 40119 |
. . . 4
β’ ((πΎ β π β§ π β π») β π = (π β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )})) |
10 | 1, 9 | syl 17 |
. . 3
β’ (π β π = (π β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )})) |
11 | 10 | fveq1d 6849 |
. 2
β’ (π β (πβπ) = ((π β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )})βπ)) |
12 | | mapdval.t |
. . 3
β’ (π β π β π) |
13 | 5 | fvexi 6861 |
. . . 4
β’ πΉ β V |
14 | 13 | rabex 5294 |
. . 3
β’ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β V |
15 | | sseq2 3975 |
. . . . . 6
β’ (π = π β ((πβ(πΏβπ)) β π β (πβ(πΏβπ)) β π)) |
16 | 15 | anbi2d 630 |
. . . . 5
β’ (π = π β (((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π ) β ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π))) |
17 | 16 | rabbidv 3418 |
. . . 4
β’ (π = π β {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )} = {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)}) |
18 | | eqid 2737 |
. . . 4
β’ (π β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )}) = (π β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )}) |
19 | 17, 18 | fvmptg 6951 |
. . 3
β’ ((π β π β§ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β V) β ((π β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )})βπ) = {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)}) |
20 | 12, 14, 19 | sylancl 587 |
. 2
β’ (π β ((π β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )})βπ) = {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)}) |
21 | 11, 20 | eqtrd 2777 |
1
β’ (π β (πβπ) = {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)}) |