Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . 5
β’ (π₯ = π β π₯ = π) |
2 | | fveq2 6843 |
. . . . 5
β’ (π₯ = π β ( β₯ βπ₯) = ( β₯ βπ)) |
3 | 1, 2 | oveq12d 7376 |
. . . 4
β’ (π₯ = π β (π₯π( β₯ βπ₯)) = (ππ( β₯ βπ))) |
4 | 3 | eleq1d 2819 |
. . 3
β’ (π₯ = π β ((π₯π( β₯ βπ₯)) β (π βm π) β (ππ( β₯ βπ)) β (π βm π))) |
5 | | pjfval.v |
. . . . 5
β’ π = (Baseβπ) |
6 | 5 | fvexi 6857 |
. . . 4
β’ π β V |
7 | 6, 6 | elmap 8812 |
. . 3
β’ ((ππ( β₯ βπ)) β (π βm π) β (ππ( β₯ βπ)):πβΆπ) |
8 | 4, 7 | bitrdi 287 |
. 2
β’ (π₯ = π β ((π₯π( β₯ βπ₯)) β (π βm π) β (ππ( β₯ βπ)):πβΆπ)) |
9 | | cnvin 6098 |
. . . . . . 7
β’ β‘((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) = (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© β‘(V Γ (π βm π))) |
10 | | cnvxp 6110 |
. . . . . . . 8
β’ β‘(V Γ (π βm π)) = ((π βm π) Γ V) |
11 | 10 | ineq2i 4170 |
. . . . . . 7
β’ (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© β‘(V Γ (π βm π))) = (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© ((π βm π) Γ V)) |
12 | 9, 11 | eqtri 2761 |
. . . . . 6
β’ β‘((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) = (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© ((π βm π) Γ V)) |
13 | | pjfval.l |
. . . . . . . 8
β’ πΏ = (LSubSpβπ) |
14 | | pjfval.o |
. . . . . . . 8
β’ β₯ =
(ocvβπ) |
15 | | pjfval.p |
. . . . . . . 8
β’ π = (proj1βπ) |
16 | | pjfval.k |
. . . . . . . 8
β’ πΎ = (projβπ) |
17 | 5, 13, 14, 15, 16 | pjfval 21128 |
. . . . . . 7
β’ πΎ = ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) |
18 | 17 | cnveqi 5831 |
. . . . . 6
β’ β‘πΎ = β‘((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) |
19 | | df-res 5646 |
. . . . . 6
β’ (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) βΎ (π βm π)) = (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© ((π βm π) Γ V)) |
20 | 12, 18, 19 | 3eqtr4i 2771 |
. . . . 5
β’ β‘πΎ = (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) βΎ (π βm π)) |
21 | 20 | rneqi 5893 |
. . . 4
β’ ran β‘πΎ = ran (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) βΎ (π βm π)) |
22 | | dfdm4 5852 |
. . . 4
β’ dom πΎ = ran β‘πΎ |
23 | | df-ima 5647 |
. . . 4
β’ (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β (π βm π)) = ran (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) βΎ (π βm π)) |
24 | 21, 22, 23 | 3eqtr4i 2771 |
. . 3
β’ dom πΎ = (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β (π βm π)) |
25 | | eqid 2733 |
. . . 4
β’ (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) = (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) |
26 | 25 | mptpreima 6191 |
. . 3
β’ (β‘(π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β (π βm π)) = {π₯ β πΏ β£ (π₯π( β₯ βπ₯)) β (π βm π)} |
27 | 24, 26 | eqtri 2761 |
. 2
β’ dom πΎ = {π₯ β πΏ β£ (π₯π( β₯ βπ₯)) β (π βm π)} |
28 | 8, 27 | elrab2 3649 |
1
β’ (π β dom πΎ β (π β πΏ β§ (ππ( β₯ βπ)):πβΆπ)) |