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 
|- ( ph -> D e. V )
mptscmfsupp0.q 
|- ( ph -> Q e. LMod )
mptscmfsupp0.r 
|- ( ph -> R = ( Scalar ` Q ) )
mptscmfsupp0.k 
|- K = ( Base ` Q )
mptscmfsupp0.s 
|- ( ( ph /\ k e. D ) -> S e. B )
mptscmfsupp0.w 
|- ( ( ph /\ k e. D ) -> W e. K )
mptscmfsupp0.0 
|- .0. = ( 0g ` Q )
mptscmfsupp0.z 
|- Z = ( 0g ` R )
mptscmfsupp0.m 
|- .* = ( .s ` Q )
mptscmfsupp0.f 
|- ( ph -> ( k e. D |-> S ) finSupp Z )
Assertion mptscmfsupp0 
|- ( ph -> ( k e. D |-> ( S .* W ) ) finSupp .0. )

Proof

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