Metamath Proof Explorer

Theorem rmfsupp2

Description: A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by Thierry Arnoux, 3-Jun-2023)

Ref Expression
Hypotheses rmfsuppf2.r 
|- R = ( Base ` M )
rmfsupp2.m 
|- ( ph -> M e. Ring )
rmfsupp2.v 
|- ( ph -> V e. X )
rmfsupp2.c 
|- ( ( ph /\ v e. V ) -> C e. R )
rmfsupp2.a 
|- ( ph -> A : V --> R )
rmfsupp2.1 
|- ( ph -> A finSupp ( 0g ` M ) )
Assertion rmfsupp2 
|- ( ph -> ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) finSupp ( 0g ` M ) )

Proof

Step Hyp Ref Expression
1 rmfsuppf2.r 
 |-  R = ( Base ` M )
2 rmfsupp2.m 
 |-  ( ph -> M e. Ring )
3 rmfsupp2.v 
 |-  ( ph -> V e. X )
4 rmfsupp2.c 
 |-  ( ( ph /\ v e. V ) -> C e. R )
5 rmfsupp2.a 
 |-  ( ph -> A : V --> R )
6 rmfsupp2.1 
 |-  ( ph -> A finSupp ( 0g ` M ) )
7 funmpt 
 |-  Fun ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) )
8 7 a1i 
 |-  ( ph -> Fun ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) )
9 3 mptexd 
 |-  ( ph -> ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) e. _V )
10 ringgrp 
 |-  ( M e. Ring -> M e. Grp )
11 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
12 1 11 grpidcl 
 |-  ( M e. Grp -> ( 0g ` M ) e. R )
13 2 10 12 3syl 
 |-  ( ph -> ( 0g ` M ) e. R )
14 suppval1 
 |-  ( ( Fun ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) /\ ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) e. _V /\ ( 0g ` M ) e. R ) -> ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) supp ( 0g ` M ) ) = { u e. dom ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) | ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ` u ) =/= ( 0g ` M ) } )
15 8 9 13 14 syl3anc 
 |-  ( ph -> ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) supp ( 0g ` M ) ) = { u e. dom ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) | ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ` u ) =/= ( 0g ` M ) } )
16 ovex 
 |-  ( ( A ` v ) ( .r ` M ) C ) e. _V
17 eqid 
 |-  ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) = ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) )
18 16 17 dmmpti 
 |-  dom ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) = V
19 18 a1i 
 |-  ( ph -> dom ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) = V )
20 ovex 
 |-  ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) e. _V
21 nfcv 
 |-  F/_ v u
22 nfcv 
 |-  F/_ v ( A ` u )
23 nfcv 
 |-  F/_ v ( .r ` M )
24 nfcsb1v 
 |-  F/_ v [_ u / v ]_ C
25 22 23 24 nfov 
 |-  F/_ v ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C )
26 fveq2 
 |-  ( v = u -> ( A ` v ) = ( A ` u ) )
27 csbeq1a 
 |-  ( v = u -> C = [_ u / v ]_ C )
28 26 27 oveq12d 
 |-  ( v = u -> ( ( A ` v ) ( .r ` M ) C ) = ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) )
29 21 25 28 17 fvmptf 
 |-  ( ( u e. V /\ ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) e. _V ) -> ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ` u ) = ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) )
30 20 29 mpan2 
 |-  ( u e. V -> ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ` u ) = ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) )
31 30 18 eleq2s 
 |-  ( u e. dom ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ` u ) = ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) )
32 31 adantl 
 |-  ( ( ph /\ u e. dom ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ` u ) = ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) )
33 32 neeq1d 
 |-  ( ( ph /\ u e. dom ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ) -> ( ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ` u ) =/= ( 0g ` M ) <-> ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) =/= ( 0g ` M ) ) )
34 19 33 rabeqbidva 
 |-  ( ph -> { u e. dom ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) | ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ` u ) =/= ( 0g ` M ) } = { u e. V | ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) =/= ( 0g ` M ) } )
35 5 fdmd 
 |-  ( ph -> dom A = V )
36 35 rabeqdv 
 |-  ( ph -> { u e. dom A | ( A ` u ) =/= ( 0g ` M ) } = { u e. V | ( A ` u ) =/= ( 0g ` M ) } )
37 5 ffund 
 |-  ( ph -> Fun A )
38 1 fvexi 
 |-  R e. _V
39 38 a1i 
 |-  ( ph -> R e. _V )
40 39 3 elmapd 
 |-  ( ph -> ( A e. ( R ^m V ) <-> A : V --> R ) )
41 5 40 mpbird 
 |-  ( ph -> A e. ( R ^m V ) )
42 suppval1 
 |-  ( ( Fun A /\ A e. ( R ^m V ) /\ ( 0g ` M ) e. R ) -> ( A supp ( 0g ` M ) ) = { u e. dom A | ( A ` u ) =/= ( 0g ` M ) } )
43 37 41 13 42 syl3anc 
 |-  ( ph -> ( A supp ( 0g ` M ) ) = { u e. dom A | ( A ` u ) =/= ( 0g ` M ) } )
44 6 fsuppimpd 
 |-  ( ph -> ( A supp ( 0g ` M ) ) e. Fin )
45 43 44 eqeltrrd 
 |-  ( ph -> { u e. dom A | ( A ` u ) =/= ( 0g ` M ) } e. Fin )
46 36 45 eqeltrrd 
 |-  ( ph -> { u e. V | ( A ` u ) =/= ( 0g ` M ) } e. Fin )
47 simpr 
 |-  ( ( ( ph /\ u e. V ) /\ ( A ` u ) = ( 0g ` M ) ) -> ( A ` u ) = ( 0g ` M ) )
48 47 oveq1d 
 |-  ( ( ( ph /\ u e. V ) /\ ( A ` u ) = ( 0g ` M ) ) -> ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) = ( ( 0g ` M ) ( .r ` M ) [_ u / v ]_ C ) )
49 2 ad2antrr 
 |-  ( ( ( ph /\ u e. V ) /\ ( A ` u ) = ( 0g ` M ) ) -> M e. Ring )
50 simplr 
 |-  ( ( ( ph /\ u e. V ) /\ ( A ` u ) = ( 0g ` M ) ) -> u e. V )
51 4 ralrimiva 
 |-  ( ph -> A. v e. V C e. R )
52 51 ad2antrr 
 |-  ( ( ( ph /\ u e. V ) /\ ( A ` u ) = ( 0g ` M ) ) -> A. v e. V C e. R )
53 rspcsbela 
 |-  ( ( u e. V /\ A. v e. V C e. R ) -> [_ u / v ]_ C e. R )
54 50 52 53 syl2anc 
 |-  ( ( ( ph /\ u e. V ) /\ ( A ` u ) = ( 0g ` M ) ) -> [_ u / v ]_ C e. R )
55 eqid 
 |-  ( .r ` M ) = ( .r ` M )
56 1 55 11 ringlz 
 |-  ( ( M e. Ring /\ [_ u / v ]_ C e. R ) -> ( ( 0g ` M ) ( .r ` M ) [_ u / v ]_ C ) = ( 0g ` M ) )
57 49 54 56 syl2anc 
 |-  ( ( ( ph /\ u e. V ) /\ ( A ` u ) = ( 0g ` M ) ) -> ( ( 0g ` M ) ( .r ` M ) [_ u / v ]_ C ) = ( 0g ` M ) )
58 48 57 eqtrd 
 |-  ( ( ( ph /\ u e. V ) /\ ( A ` u ) = ( 0g ` M ) ) -> ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) = ( 0g ` M ) )
59 58 ex 
 |-  ( ( ph /\ u e. V ) -> ( ( A ` u ) = ( 0g ` M ) -> ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) = ( 0g ` M ) ) )
60 59 necon3d 
 |-  ( ( ph /\ u e. V ) -> ( ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) =/= ( 0g ` M ) -> ( A ` u ) =/= ( 0g ` M ) ) )
61 60 ss2rabdv 
 |-  ( ph -> { u e. V | ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) =/= ( 0g ` M ) } C_ { u e. V | ( A ` u ) =/= ( 0g ` M ) } )
62 ssfi 
 |-  ( ( { u e. V | ( A ` u ) =/= ( 0g ` M ) } e. Fin /\ { u e. V | ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) =/= ( 0g ` M ) } C_ { u e. V | ( A ` u ) =/= ( 0g ` M ) } ) -> { u e. V | ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) =/= ( 0g ` M ) } e. Fin )
63 46 61 62 syl2anc 
 |-  ( ph -> { u e. V | ( ( A ` u ) ( .r ` M ) [_ u / v ]_ C ) =/= ( 0g ` M ) } e. Fin )
64 34 63 eqeltrd 
 |-  ( ph -> { u e. dom ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) | ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) ` u ) =/= ( 0g ` M ) } e. Fin )
65 15 64 eqeltrd 
 |-  ( ph -> ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) supp ( 0g ` M ) ) e. Fin )
66 isfsupp 
 |-  ( ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) e. _V /\ ( 0g ` M ) e. R ) -> ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) finSupp ( 0g ` M ) <-> ( Fun ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) /\ ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) supp ( 0g ` M ) ) e. Fin ) ) )
67 9 13 66 syl2anc 
 |-  ( ph -> ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) finSupp ( 0g ` M ) <-> ( Fun ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) /\ ( ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) supp ( 0g ` M ) ) e. Fin ) ) )
68 8 65 67 mpbir2and 
 |-  ( ph -> ( v e. V |-> ( ( A ` v ) ( .r ` M ) C ) ) finSupp ( 0g ` M ) )