Step | Hyp | Ref
| Expression |
1 | | mptscmfsupp0.d |
. . 3
β’ (π β π· β π) |
2 | 1 | mptexd 7175 |
. 2
β’ (π β (π β π· β¦ (π β π)) β V) |
3 | | funmpt 6540 |
. . 3
β’ Fun
(π β π· β¦ (π β π)) |
4 | 3 | a1i 11 |
. 2
β’ (π β Fun (π β π· β¦ (π β π))) |
5 | | mptscmfsupp0.0 |
. . . 4
β’ 0 =
(0gβπ) |
6 | 5 | fvexi 6857 |
. . 3
β’ 0 β
V |
7 | 6 | a1i 11 |
. 2
β’ (π β 0 β V) |
8 | | mptscmfsupp0.f |
. . 3
β’ (π β (π β π· β¦ π) finSupp π) |
9 | 8 | fsuppimpd 9316 |
. 2
β’ (π β ((π β π· β¦ π) supp π) β Fin) |
10 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β π·) β π β π·) |
11 | | mptscmfsupp0.s |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β π β π΅) |
12 | 11 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (π β βπ β π· π β π΅) |
13 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π·) β βπ β π· π β π΅) |
14 | | rspcsbela 4396 |
. . . . . . . . 9
β’ ((π β π· β§ βπ β π· π β π΅) β β¦π / πβ¦π β π΅) |
15 | 10, 13, 14 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β π·) β β¦π / πβ¦π β π΅) |
16 | | eqid 2733 |
. . . . . . . . 9
β’ (π β π· β¦ π) = (π β π· β¦ π) |
17 | 16 | fvmpts 6952 |
. . . . . . . 8
β’ ((π β π· β§ β¦π / πβ¦π β π΅) β ((π β π· β¦ π)βπ) = β¦π / πβ¦π) |
18 | 10, 15, 17 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β π·) β ((π β π· β¦ π)βπ) = β¦π / πβ¦π) |
19 | 18 | eqeq1d 2735 |
. . . . . 6
β’ ((π β§ π β π·) β (((π β π· β¦ π)βπ) = π β β¦π / πβ¦π = π)) |
20 | | oveq1 7365 |
. . . . . . . . 9
β’
(β¦π /
πβ¦π = π β (β¦π / πβ¦π β
β¦π / πβ¦π) = (π β
β¦π / πβ¦π)) |
21 | | mptscmfsupp0.z |
. . . . . . . . . . . 12
β’ π = (0gβπ
) |
22 | | mptscmfsupp0.r |
. . . . . . . . . . . . . 14
β’ (π β π
= (Scalarβπ)) |
23 | 22 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β π
= (Scalarβπ)) |
24 | 23 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (0gβπ
) =
(0gβ(Scalarβπ))) |
25 | 21, 24 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β π = (0gβ(Scalarβπ))) |
26 | 25 | oveq1d 7373 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (π β
β¦π / πβ¦π) =
((0gβ(Scalarβπ)) β
β¦π / πβ¦π)) |
27 | | mptscmfsupp0.q |
. . . . . . . . . . . 12
β’ (π β π β LMod) |
28 | 27 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β π β LMod) |
29 | | mptscmfsupp0.w |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π β πΎ) |
30 | 29 | ralrimiva 3140 |
. . . . . . . . . . . . 13
β’ (π β βπ β π· π β πΎ) |
31 | 30 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β βπ β π· π β πΎ) |
32 | | rspcsbela 4396 |
. . . . . . . . . . . 12
β’ ((π β π· β§ βπ β π· π β πΎ) β β¦π / πβ¦π β πΎ) |
33 | 10, 31, 32 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β β¦π / πβ¦π β πΎ) |
34 | | mptscmfsupp0.k |
. . . . . . . . . . . 12
β’ πΎ = (Baseβπ) |
35 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Scalarβπ) =
(Scalarβπ) |
36 | | mptscmfsupp0.m |
. . . . . . . . . . . 12
β’ β = (
Β·π βπ) |
37 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
38 | 34, 35, 36, 37, 5 | lmod0vs 20370 |
. . . . . . . . . . 11
β’ ((π β LMod β§
β¦π / πβ¦π β πΎ) β
((0gβ(Scalarβπ)) β
β¦π / πβ¦π) = 0 ) |
39 | 28, 33, 38 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β
((0gβ(Scalarβπ)) β
β¦π / πβ¦π) = 0 ) |
40 | 26, 39 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π β π·) β (π β
β¦π / πβ¦π) = 0 ) |
41 | 20, 40 | sylan9eqr 2795 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ β¦π / πβ¦π = π) β (β¦π / πβ¦π β
β¦π / πβ¦π) = 0 ) |
42 | | csbov12g 7402 |
. . . . . . . . . . . . . 14
β’ (π β π· β β¦π / πβ¦(π β π) = (β¦π / πβ¦π β
β¦π / πβ¦π)) |
43 | 42 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β β¦π / πβ¦(π β π) = (β¦π / πβ¦π β
β¦π / πβ¦π)) |
44 | | ovex 7391 |
. . . . . . . . . . . . 13
β’
(β¦π /
πβ¦π β
β¦π / πβ¦π) β V |
45 | 43, 44 | eqeltrdi 2842 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β β¦π / πβ¦(π β π) β V) |
46 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π β π· β¦ (π β π)) = (π β π· β¦ (π β π)) |
47 | 46 | fvmpts 6952 |
. . . . . . . . . . . 12
β’ ((π β π· β§ β¦π / πβ¦(π β π) β V) β ((π β π· β¦ (π β π))βπ) = β¦π / πβ¦(π β π)) |
48 | 10, 45, 47 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((π β π· β¦ (π β π))βπ) = β¦π / πβ¦(π β π)) |
49 | 48, 43 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β ((π β π· β¦ (π β π))βπ) = (β¦π / πβ¦π β
β¦π / πβ¦π)) |
50 | 49 | eqeq1d 2735 |
. . . . . . . . 9
β’ ((π β§ π β π·) β (((π β π· β¦ (π β π))βπ) = 0 β
(β¦π / πβ¦π β
β¦π / πβ¦π) = 0 )) |
51 | 50 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ β¦π / πβ¦π = π) β (((π β π· β¦ (π β π))βπ) = 0 β
(β¦π / πβ¦π β
β¦π / πβ¦π) = 0 )) |
52 | 41, 51 | mpbird 257 |
. . . . . . 7
β’ (((π β§ π β π·) β§ β¦π / πβ¦π = π) β ((π β π· β¦ (π β π))βπ) = 0 ) |
53 | 52 | ex 414 |
. . . . . 6
β’ ((π β§ π β π·) β (β¦π / πβ¦π = π β ((π β π· β¦ (π β π))βπ) = 0 )) |
54 | 19, 53 | sylbid 239 |
. . . . 5
β’ ((π β§ π β π·) β (((π β π· β¦ π)βπ) = π β ((π β π· β¦ (π β π))βπ) = 0 )) |
55 | 54 | necon3d 2961 |
. . . 4
β’ ((π β§ π β π·) β (((π β π· β¦ (π β π))βπ) β 0 β ((π β π· β¦ π)βπ) β π)) |
56 | 55 | ss2rabdv 4034 |
. . 3
β’ (π β {π β π· β£ ((π β π· β¦ (π β π))βπ) β 0 } β {π β π· β£ ((π β π· β¦ π)βπ) β π}) |
57 | | ovex 7391 |
. . . . . 6
β’ (π β π) β V |
58 | 57 | rgenw 3065 |
. . . . 5
β’
βπ β
π· (π β π) β V |
59 | 46 | fnmpt 6642 |
. . . . 5
β’
(βπ β
π· (π β π) β V β (π β π· β¦ (π β π)) Fn π·) |
60 | 58, 59 | mp1i 13 |
. . . 4
β’ (π β (π β π· β¦ (π β π)) Fn π·) |
61 | | suppvalfn 8101 |
. . . 4
β’ (((π β π· β¦ (π β π)) Fn π· β§ π· β π β§ 0 β V) β ((π β π· β¦ (π β π)) supp 0 ) = {π β π· β£ ((π β π· β¦ (π β π))βπ) β 0 }) |
62 | 60, 1, 7, 61 | syl3anc 1372 |
. . 3
β’ (π β ((π β π· β¦ (π β π)) supp 0 ) = {π β π· β£ ((π β π· β¦ (π β π))βπ) β 0 }) |
63 | 16 | fnmpt 6642 |
. . . . 5
β’
(βπ β
π· π β π΅ β (π β π· β¦ π) Fn π·) |
64 | 12, 63 | syl 17 |
. . . 4
β’ (π β (π β π· β¦ π) Fn π·) |
65 | 21 | fvexi 6857 |
. . . . 5
β’ π β V |
66 | 65 | a1i 11 |
. . . 4
β’ (π β π β V) |
67 | | suppvalfn 8101 |
. . . 4
β’ (((π β π· β¦ π) Fn π· β§ π· β π β§ π β V) β ((π β π· β¦ π) supp π) = {π β π· β£ ((π β π· β¦ π)βπ) β π}) |
68 | 64, 1, 66, 67 | syl3anc 1372 |
. . 3
β’ (π β ((π β π· β¦ π) supp π) = {π β π· β£ ((π β π· β¦ π)βπ) β π}) |
69 | 56, 62, 68 | 3sstr4d 3992 |
. 2
β’ (π β ((π β π· β¦ (π β π)) supp 0 ) β ((π β π· β¦ π) supp π)) |
70 | | suppssfifsupp 9325 |
. 2
β’ ((((π β π· β¦ (π β π)) β V β§ Fun (π β π· β¦ (π β π)) β§ 0 β V) β§ (((π β π· β¦ π) supp π) β Fin β§ ((π β π· β¦ (π β π)) supp 0 ) β ((π β π· β¦ π) supp π))) β (π β π· β¦ (π β π)) finSupp 0 ) |
71 | 2, 4, 7, 9, 69, 70 | syl32anc 1379 |
1
β’ (π β (π β π· β¦ (π β π)) finSupp 0 ) |