Step | Hyp | Ref
| Expression |
1 | | pjfval.k |
. 2
β’ πΎ = (projβπ) |
2 | | fveq2 6843 |
. . . . . . 7
β’ (π€ = π β (LSubSpβπ€) = (LSubSpβπ)) |
3 | | pjfval.l |
. . . . . . 7
β’ πΏ = (LSubSpβπ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . 6
β’ (π€ = π β (LSubSpβπ€) = πΏ) |
5 | | fveq2 6843 |
. . . . . . . 8
β’ (π€ = π β (proj1βπ€) =
(proj1βπ)) |
6 | | pjfval.p |
. . . . . . . 8
β’ π = (proj1βπ) |
7 | 5, 6 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β (proj1βπ€) = π) |
8 | | eqidd 2734 |
. . . . . . 7
β’ (π€ = π β π₯ = π₯) |
9 | | fveq2 6843 |
. . . . . . . . 9
β’ (π€ = π β (ocvβπ€) = (ocvβπ)) |
10 | | pjfval.o |
. . . . . . . . 9
β’ β₯ =
(ocvβπ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . . 8
β’ (π€ = π β (ocvβπ€) = β₯ ) |
12 | 11 | fveq1d 6845 |
. . . . . . 7
β’ (π€ = π β ((ocvβπ€)βπ₯) = ( β₯ βπ₯)) |
13 | 7, 8, 12 | oveq123d 7379 |
. . . . . 6
β’ (π€ = π β (π₯(proj1βπ€)((ocvβπ€)βπ₯)) = (π₯π( β₯ βπ₯))) |
14 | 4, 13 | mpteq12dv 5197 |
. . . . 5
β’ (π€ = π β (π₯ β (LSubSpβπ€) β¦ (π₯(proj1βπ€)((ocvβπ€)βπ₯))) = (π₯ β πΏ β¦ (π₯π( β₯ βπ₯)))) |
15 | | fveq2 6843 |
. . . . . . . 8
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
16 | | pjfval.v |
. . . . . . . 8
β’ π = (Baseβπ) |
17 | 15, 16 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β (Baseβπ€) = π) |
18 | 17, 17 | oveq12d 7376 |
. . . . . 6
β’ (π€ = π β ((Baseβπ€) βm (Baseβπ€)) = (π βm π)) |
19 | 18 | xpeq2d 5664 |
. . . . 5
β’ (π€ = π β (V Γ ((Baseβπ€) βm
(Baseβπ€))) = (V
Γ (π
βm π))) |
20 | 14, 19 | ineq12d 4174 |
. . . 4
β’ (π€ = π β ((π₯ β (LSubSpβπ€) β¦ (π₯(proj1βπ€)((ocvβπ€)βπ₯))) β© (V Γ ((Baseβπ€) βm
(Baseβπ€)))) = ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π)))) |
21 | | df-pj 21125 |
. . . 4
β’ proj =
(π€ β V β¦ ((π₯ β (LSubSpβπ€) β¦ (π₯(proj1βπ€)((ocvβπ€)βπ₯))) β© (V Γ ((Baseβπ€) βm
(Baseβπ€))))) |
22 | 3 | fvexi 6857 |
. . . . . . 7
β’ πΏ β V |
23 | 22 | inex1 5275 |
. . . . . 6
β’ (πΏ β© V) β
V |
24 | | ovex 7391 |
. . . . . . 7
β’ (π βm π) β V |
25 | 24 | inex2 5276 |
. . . . . 6
β’ (V β©
(π βm π)) β V |
26 | 23, 25 | xpex 7688 |
. . . . 5
β’ ((πΏ β© V) Γ (V β©
(π βm π))) β V |
27 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) = (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) |
28 | | ovexd 7393 |
. . . . . . . 8
β’ (π₯ β πΏ β (π₯π( β₯ βπ₯)) β V) |
29 | 27, 28 | fmpti 7061 |
. . . . . . 7
β’ (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))):πΏβΆV |
30 | | fssxp 6697 |
. . . . . . 7
β’ ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))):πΏβΆV β (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β (πΏ Γ V)) |
31 | | ssrin 4194 |
. . . . . . 7
β’ ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β (πΏ Γ V) β ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) β ((πΏ Γ V) β© (V Γ (π βm π)))) |
32 | 29, 30, 31 | mp2b 10 |
. . . . . 6
β’ ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) β ((πΏ Γ V) β© (V Γ (π βm π))) |
33 | | inxp 5789 |
. . . . . 6
β’ ((πΏ Γ V) β© (V Γ
(π βm π))) = ((πΏ β© V) Γ (V β© (π βm π))) |
34 | 32, 33 | sseqtri 3981 |
. . . . 5
β’ ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) β ((πΏ β© V) Γ (V β© (π βm π))) |
35 | 26, 34 | ssexi 5280 |
. . . 4
β’ ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) β V |
36 | 20, 21, 35 | fvmpt 6949 |
. . 3
β’ (π β V β
(projβπ) = ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π)))) |
37 | | fvprc 6835 |
. . . 4
β’ (Β¬
π β V β
(projβπ) =
β
) |
38 | | inss1 4189 |
. . . . 5
β’ ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) β (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) |
39 | | fvprc 6835 |
. . . . . . . 8
β’ (Β¬
π β V β
(LSubSpβπ) =
β
) |
40 | 3, 39 | eqtrid 2785 |
. . . . . . 7
β’ (Β¬
π β V β πΏ = β
) |
41 | 40 | mpteq1d 5201 |
. . . . . 6
β’ (Β¬
π β V β (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) = (π₯ β β
β¦ (π₯π( β₯ βπ₯)))) |
42 | | mpt0 6644 |
. . . . . 6
β’ (π₯ β β
β¦ (π₯π( β₯ βπ₯))) = β
|
43 | 41, 42 | eqtrdi 2789 |
. . . . 5
β’ (Β¬
π β V β (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) = β
) |
44 | | sseq0 4360 |
. . . . 5
β’ ((((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) β (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β§ (π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) = β
) β ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) = β
) |
45 | 38, 43, 44 | sylancr 588 |
. . . 4
β’ (Β¬
π β V β ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) = β
) |
46 | 37, 45 | eqtr4d 2776 |
. . 3
β’ (Β¬
π β V β
(projβπ) = ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π)))) |
47 | 36, 46 | pm2.61i 182 |
. 2
β’
(projβπ) =
((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) |
48 | 1, 47 | eqtri 2761 |
1
β’ πΎ = ((π₯ β πΏ β¦ (π₯π( β₯ βπ₯))) β© (V Γ (π βm π))) |