Step | Hyp | Ref
| Expression |
1 | | ellspd.f |
. . . . . 6
β’ (π β πΉ:πΌβΆπ΅) |
2 | | ffn 6669 |
. . . . . 6
β’ (πΉ:πΌβΆπ΅ β πΉ Fn πΌ) |
3 | | fnima 6632 |
. . . . . 6
β’ (πΉ Fn πΌ β (πΉ β πΌ) = ran πΉ) |
4 | 1, 2, 3 | 3syl 18 |
. . . . 5
β’ (π β (πΉ β πΌ) = ran πΉ) |
5 | 4 | fveq2d 6847 |
. . . 4
β’ (π β (πβ(πΉ β πΌ)) = (πβran πΉ)) |
6 | | eqid 2733 |
. . . . . 6
β’ (π β (Baseβ(π freeLMod πΌ)) β¦ (π Ξ£g (π βf Β· πΉ))) = (π β (Baseβ(π freeLMod πΌ)) β¦ (π Ξ£g (π βf Β· πΉ))) |
7 | 6 | rnmpt 5911 |
. . . . 5
β’ ran
(π β
(Baseβ(π freeLMod
πΌ)) β¦ (π Ξ£g
(π βf
Β·
πΉ))) = {π β£ βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ))} |
8 | | eqid 2733 |
. . . . . 6
β’ (π freeLMod πΌ) = (π freeLMod πΌ) |
9 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(π
freeLMod πΌ)) =
(Baseβ(π freeLMod
πΌ)) |
10 | | ellspd.v |
. . . . . 6
β’ π΅ = (Baseβπ) |
11 | | ellspd.t |
. . . . . 6
β’ Β· = (
Β·π βπ) |
12 | | ellspd.m |
. . . . . 6
β’ (π β π β LMod) |
13 | | ellspd.i |
. . . . . 6
β’ (π β πΌ β π) |
14 | | ellspd.s |
. . . . . . 7
β’ π = (Scalarβπ) |
15 | 14 | a1i 11 |
. . . . . 6
β’ (π β π = (Scalarβπ)) |
16 | | ellspd.n |
. . . . . 6
β’ π = (LSpanβπ) |
17 | 8, 9, 10, 11, 6, 12, 13, 15, 1, 16 | frlmup3 21222 |
. . . . 5
β’ (π β ran (π β (Baseβ(π freeLMod πΌ)) β¦ (π Ξ£g (π βf Β· πΉ))) = (πβran πΉ)) |
18 | 7, 17 | eqtr3id 2787 |
. . . 4
β’ (π β {π β£ βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ))} = (πβran πΉ)) |
19 | 5, 18 | eqtr4d 2776 |
. . 3
β’ (π β (πβ(πΉ β πΌ)) = {π β£ βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ))}) |
20 | 19 | eleq2d 2820 |
. 2
β’ (π β (π β (πβ(πΉ β πΌ)) β π β {π β£ βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ))})) |
21 | | ovex 7391 |
. . . . . 6
β’ (π Ξ£g
(π βf
Β·
πΉ)) β
V |
22 | | eleq1 2822 |
. . . . . 6
β’ (π = (π Ξ£g (π βf Β· πΉ)) β (π β V β (π Ξ£g (π βf Β· πΉ)) β V)) |
23 | 21, 22 | mpbiri 258 |
. . . . 5
β’ (π = (π Ξ£g (π βf Β· πΉ)) β π β V) |
24 | 23 | rexlimivw 3145 |
. . . 4
β’
(βπ β
(Baseβ(π freeLMod
πΌ))π = (π Ξ£g (π βf Β· πΉ)) β π β V) |
25 | | eqeq1 2737 |
. . . . 5
β’ (π = π β (π = (π Ξ£g (π βf Β· πΉ)) β π = (π Ξ£g (π βf Β· πΉ)))) |
26 | 25 | rexbidv 3172 |
. . . 4
β’ (π = π β (βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ)) β βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ)))) |
27 | 24, 26 | elab3 3639 |
. . 3
β’ (π β {π β£ βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ))} β βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ))) |
28 | 14 | fvexi 6857 |
. . . . . . 7
β’ π β V |
29 | | ellspd.k |
. . . . . . . 8
β’ πΎ = (Baseβπ) |
30 | | ellspd.z |
. . . . . . . 8
β’ 0 =
(0gβπ) |
31 | | eqid 2733 |
. . . . . . . 8
β’ {π β (πΎ βm πΌ) β£ π finSupp 0 } = {π β (πΎ βm πΌ) β£ π finSupp 0 } |
32 | 8, 29, 30, 31 | frlmbas 21177 |
. . . . . . 7
β’ ((π β V β§ πΌ β π) β {π β (πΎ βm πΌ) β£ π finSupp 0 } = (Baseβ(π freeLMod πΌ))) |
33 | 28, 13, 32 | sylancr 588 |
. . . . . 6
β’ (π β {π β (πΎ βm πΌ) β£ π finSupp 0 } = (Baseβ(π freeLMod πΌ))) |
34 | 33 | eqcomd 2739 |
. . . . 5
β’ (π β (Baseβ(π freeLMod πΌ)) = {π β (πΎ βm πΌ) β£ π finSupp 0 }) |
35 | 34 | rexeqdv 3313 |
. . . 4
β’ (π β (βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ)) β βπ β {π β (πΎ βm πΌ) β£ π finSupp 0 }π = (π Ξ£g (π βf Β· πΉ)))) |
36 | | breq1 5109 |
. . . . 5
β’ (π = π β (π finSupp 0 β π finSupp 0 )) |
37 | 36 | rexrab 3655 |
. . . 4
β’
(βπ β
{π β (πΎ βm πΌ) β£ π finSupp 0 }π = (π Ξ£g (π βf Β· πΉ)) β βπ β (πΎ βm πΌ)(π finSupp 0 β§ π = (π Ξ£g (π βf Β· πΉ)))) |
38 | 35, 37 | bitrdi 287 |
. . 3
β’ (π β (βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ)) β βπ β (πΎ βm πΌ)(π finSupp 0 β§ π = (π Ξ£g (π βf Β· πΉ))))) |
39 | 27, 38 | bitrid 283 |
. 2
β’ (π β (π β {π β£ βπ β (Baseβ(π freeLMod πΌ))π = (π Ξ£g (π βf Β· πΉ))} β βπ β (πΎ βm πΌ)(π finSupp 0 β§ π = (π Ξ£g (π βf Β· πΉ))))) |
40 | 20, 39 | bitrd 279 |
1
β’ (π β (π β (πβ(πΉ β πΌ)) β βπ β (πΎ βm πΌ)(π finSupp 0 β§ π = (π Ξ£g (π βf Β· πΉ))))) |