Step | Hyp | Ref
| Expression |
1 | | lincvalsc0.s |
. . . . . 6
β’ π = (Scalarβπ) |
2 | | lcoc0.r |
. . . . . 6
β’ π
= (Baseβπ) |
3 | | lincvalsc0.0 |
. . . . . 6
β’ 0 =
(0gβπ) |
4 | 1, 2, 3 | lmod0cl 20392 |
. . . . 5
β’ (π β LMod β 0 β π
) |
5 | 4 | ad2antrr 725 |
. . . 4
β’ (((π β LMod β§ π β π« π΅) β§ π₯ β π) β 0 β π
) |
6 | | lincvalsc0.f |
. . . 4
β’ πΉ = (π₯ β π β¦ 0 ) |
7 | 5, 6 | fmptd 7066 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β πΉ:πβΆπ
) |
8 | 2 | fvexi 6860 |
. . . . 5
β’ π
β V |
9 | 8 | a1i 11 |
. . . 4
β’ (π β LMod β π
β V) |
10 | | elmapg 8784 |
. . . 4
β’ ((π
β V β§ π β π« π΅) β (πΉ β (π
βm π) β πΉ:πβΆπ
)) |
11 | 9, 10 | sylan 581 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β (πΉ β (π
βm π) β πΉ:πβΆπ
)) |
12 | 7, 11 | mpbird 257 |
. 2
β’ ((π β LMod β§ π β π« π΅) β πΉ β (π
βm π)) |
13 | | eqidd 2734 |
. . . . . . 7
β’ (π₯ = π£ β 0 = 0 ) |
14 | 13 | cbvmptv 5222 |
. . . . . 6
β’ (π₯ β π β¦ 0 ) = (π£ β π β¦ 0 ) |
15 | 6, 14 | eqtri 2761 |
. . . . 5
β’ πΉ = (π£ β π β¦ 0 ) |
16 | | simpr 486 |
. . . . 5
β’ ((π β LMod β§ π β π« π΅) β π β π« π΅) |
17 | 3 | fvexi 6860 |
. . . . . 6
β’ 0 β
V |
18 | 17 | a1i 11 |
. . . . 5
β’ ((π β LMod β§ π β π« π΅) β 0 β V) |
19 | 17 | a1i 11 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β 0 β V) |
20 | 15, 16, 18, 19 | mptsuppd 8122 |
. . . 4
β’ ((π β LMod β§ π β π« π΅) β (πΉ supp 0 ) = {π£ β π β£ 0 β 0 }) |
21 | | neirr 2949 |
. . . . . . . 8
β’ Β¬
0 β
0 |
22 | 21 | a1i 11 |
. . . . . . 7
β’ ((π β LMod β§ π β π« π΅) β Β¬ 0 β 0
) |
23 | 22 | ralrimivw 3144 |
. . . . . 6
β’ ((π β LMod β§ π β π« π΅) β βπ£ β π Β¬ 0 β 0 ) |
24 | | rabeq0 4348 |
. . . . . 6
β’ ({π£ β π β£ 0 β 0 } = β
β
βπ£ β π Β¬ 0 β 0 ) |
25 | 23, 24 | sylibr 233 |
. . . . 5
β’ ((π β LMod β§ π β π« π΅) β {π£ β π β£ 0 β 0 } =
β
) |
26 | | 0fin 9121 |
. . . . . 6
β’ β
β Fin |
27 | 26 | a1i 11 |
. . . . 5
β’ ((π β LMod β§ π β π« π΅) β β
β
Fin) |
28 | 25, 27 | eqeltrd 2834 |
. . . 4
β’ ((π β LMod β§ π β π« π΅) β {π£ β π β£ 0 β 0 } β
Fin) |
29 | 20, 28 | eqeltrd 2834 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β (πΉ supp 0 ) β
Fin) |
30 | 6 | funmpt2 6544 |
. . . . 5
β’ Fun πΉ |
31 | 30 | a1i 11 |
. . . 4
β’ ((π β LMod β§ π β π« π΅) β Fun πΉ) |
32 | | funisfsupp 9317 |
. . . 4
β’ ((Fun
πΉ β§ πΉ β (π
βm π) β§ 0 β V) β (πΉ finSupp 0 β (πΉ supp 0 ) β
Fin)) |
33 | 31, 12, 18, 32 | syl3anc 1372 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β (πΉ finSupp 0 β (πΉ supp 0 ) β
Fin)) |
34 | 29, 33 | mpbird 257 |
. 2
β’ ((π β LMod β§ π β π« π΅) β πΉ finSupp 0 ) |
35 | | lincvalsc0.b |
. . 3
β’ π΅ = (Baseβπ) |
36 | | lincvalsc0.z |
. . 3
β’ π = (0gβπ) |
37 | 35, 1, 3, 36, 6 | lincvalsc0 46592 |
. 2
β’ ((π β LMod β§ π β π« π΅) β (πΉ( linC βπ)π) = π) |
38 | 12, 34, 37 | 3jca 1129 |
1
β’ ((π β LMod β§ π β π« π΅) β (πΉ β (π
βm π) β§ πΉ finSupp 0 β§ (πΉ( linC βπ)π) = π)) |