# Metamath Proof Explorer

## Theorem mptscmfsupp0

Description: A mapping to a scalar product is finitely supported if the mapping to the scalar is finitely supported. (Contributed by AV, 5-Oct-2019)

Ref Expression
Hypotheses mptscmfsupp0.d ${⊢}{\phi }\to {D}\in {V}$
mptscmfsupp0.q ${⊢}{\phi }\to {Q}\in \mathrm{LMod}$
mptscmfsupp0.r ${⊢}{\phi }\to {R}=\mathrm{Scalar}\left({Q}\right)$
mptscmfsupp0.k ${⊢}{K}={\mathrm{Base}}_{{Q}}$
mptscmfsupp0.s ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to {S}\in {B}$
mptscmfsupp0.w ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to {W}\in {K}$
mptscmfsupp0.0
mptscmfsupp0.z ${⊢}{Z}={0}_{{R}}$
mptscmfsupp0.m
mptscmfsupp0.f ${⊢}{\phi }\to {finSupp}_{{Z}}\left(\left({k}\in {D}⟼{S}\right)\right)$
Assertion mptscmfsupp0

### Proof

Step Hyp Ref Expression
1 mptscmfsupp0.d ${⊢}{\phi }\to {D}\in {V}$
2 mptscmfsupp0.q ${⊢}{\phi }\to {Q}\in \mathrm{LMod}$
3 mptscmfsupp0.r ${⊢}{\phi }\to {R}=\mathrm{Scalar}\left({Q}\right)$
4 mptscmfsupp0.k ${⊢}{K}={\mathrm{Base}}_{{Q}}$
5 mptscmfsupp0.s ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to {S}\in {B}$
6 mptscmfsupp0.w ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to {W}\in {K}$
7 mptscmfsupp0.0
8 mptscmfsupp0.z ${⊢}{Z}={0}_{{R}}$
9 mptscmfsupp0.m
10 mptscmfsupp0.f ${⊢}{\phi }\to {finSupp}_{{Z}}\left(\left({k}\in {D}⟼{S}\right)\right)$
11 1 mptexd
12 funmpt
13 12 a1i
14 7 fvexi
15 14 a1i
16 10 fsuppimpd ${⊢}{\phi }\to \left({k}\in {D}⟼{S}\right)\mathrm{supp}{Z}\in \mathrm{Fin}$
17 simpr ${⊢}\left({\phi }\wedge {d}\in {D}\right)\to {d}\in {D}$
18 5 ralrimiva ${⊢}{\phi }\to \forall {k}\in {D}\phantom{\rule{.4em}{0ex}}{S}\in {B}$
19 18 adantr ${⊢}\left({\phi }\wedge {d}\in {D}\right)\to \forall {k}\in {D}\phantom{\rule{.4em}{0ex}}{S}\in {B}$
20 rspcsbela
21 17 19 20 syl2anc
22 eqid ${⊢}\left({k}\in {D}⟼{S}\right)=\left({k}\in {D}⟼{S}\right)$
23 22 fvmpts
24 17 21 23 syl2anc
25 24 eqeq1d
26 oveq1
27 3 adantr ${⊢}\left({\phi }\wedge {d}\in {D}\right)\to {R}=\mathrm{Scalar}\left({Q}\right)$
28 27 fveq2d ${⊢}\left({\phi }\wedge {d}\in {D}\right)\to {0}_{{R}}={0}_{\mathrm{Scalar}\left({Q}\right)}$
29 8 28 syl5eq ${⊢}\left({\phi }\wedge {d}\in {D}\right)\to {Z}={0}_{\mathrm{Scalar}\left({Q}\right)}$
30 29 oveq1d
31 2 adantr ${⊢}\left({\phi }\wedge {d}\in {D}\right)\to {Q}\in \mathrm{LMod}$
32 6 ralrimiva ${⊢}{\phi }\to \forall {k}\in {D}\phantom{\rule{.4em}{0ex}}{W}\in {K}$
33 32 adantr ${⊢}\left({\phi }\wedge {d}\in {D}\right)\to \forall {k}\in {D}\phantom{\rule{.4em}{0ex}}{W}\in {K}$
34 rspcsbela
35 17 33 34 syl2anc
36 eqid ${⊢}\mathrm{Scalar}\left({Q}\right)=\mathrm{Scalar}\left({Q}\right)$
37 eqid ${⊢}{0}_{\mathrm{Scalar}\left({Q}\right)}={0}_{\mathrm{Scalar}\left({Q}\right)}$
38 4 36 9 37 7 lmod0vs
39 31 35 38 syl2anc
40 30 39 eqtrd
41 26 40 sylan9eqr
42 csbov12g
43 42 adantl
44 ovex
45 43 44 eqeltrdi
46 eqid
47 46 fvmpts
48 17 45 47 syl2anc
49 48 43 eqtrd
50 49 eqeq1d
51 50 adantr
52 41 51 mpbird
53 52 ex
54 25 53 sylbid
55 54 necon3d
56 55 ss2rabdv
57 ovex
58 57 rgenw
59 46 fnmpt
60 58 59 mp1i
61 suppvalfn
62 60 1 15 61 syl3anc
63 22 fnmpt ${⊢}\forall {k}\in {D}\phantom{\rule{.4em}{0ex}}{S}\in {B}\to \left({k}\in {D}⟼{S}\right)Fn{D}$
64 18 63 syl ${⊢}{\phi }\to \left({k}\in {D}⟼{S}\right)Fn{D}$
65 8 fvexi ${⊢}{Z}\in \mathrm{V}$
66 65 a1i ${⊢}{\phi }\to {Z}\in \mathrm{V}$
67 suppvalfn ${⊢}\left(\left({k}\in {D}⟼{S}\right)Fn{D}\wedge {D}\in {V}\wedge {Z}\in \mathrm{V}\right)\to \left({k}\in {D}⟼{S}\right)\mathrm{supp}{Z}=\left\{{d}\in {D}|\left({k}\in {D}⟼{S}\right)\left({d}\right)\ne {Z}\right\}$
68 64 1 66 67 syl3anc ${⊢}{\phi }\to \left({k}\in {D}⟼{S}\right)\mathrm{supp}{Z}=\left\{{d}\in {D}|\left({k}\in {D}⟼{S}\right)\left({d}\right)\ne {Z}\right\}$
69 56 62 68 3sstr4d
70 suppssfifsupp
71 11 13 15 16 69 70 syl32anc