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 𝑅 = ( Base ‘ 𝑀 )
rmfsupp2.m ( 𝜑𝑀 ∈ Ring )
rmfsupp2.v ( 𝜑𝑉𝑋 )
rmfsupp2.c ( ( 𝜑𝑣𝑉 ) → 𝐶𝑅 )
rmfsupp2.a ( 𝜑𝐴 : 𝑉𝑅 )
rmfsupp2.1 ( 𝜑𝐴 finSupp ( 0g𝑀 ) )
Assertion rmfsupp2 ( 𝜑 → ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) finSupp ( 0g𝑀 ) )

Proof

Step Hyp Ref Expression
1 rmfsuppf2.r 𝑅 = ( Base ‘ 𝑀 )
2 rmfsupp2.m ( 𝜑𝑀 ∈ Ring )
3 rmfsupp2.v ( 𝜑𝑉𝑋 )
4 rmfsupp2.c ( ( 𝜑𝑣𝑉 ) → 𝐶𝑅 )
5 rmfsupp2.a ( 𝜑𝐴 : 𝑉𝑅 )
6 rmfsupp2.1 ( 𝜑𝐴 finSupp ( 0g𝑀 ) )
7 funmpt Fun ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) )
8 7 a1i ( 𝜑 → Fun ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) )
9 3 mptexd ( 𝜑 → ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∈ V )
10 ringgrp ( 𝑀 ∈ Ring → 𝑀 ∈ Grp )
11 eqid ( 0g𝑀 ) = ( 0g𝑀 )
12 1 11 grpidcl ( 𝑀 ∈ Grp → ( 0g𝑀 ) ∈ 𝑅 )
13 2 10 12 3syl ( 𝜑 → ( 0g𝑀 ) ∈ 𝑅 )
14 suppval1 ( ( Fun ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∧ ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∈ V ∧ ( 0g𝑀 ) ∈ 𝑅 ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) supp ( 0g𝑀 ) ) = { 𝑢 ∈ dom ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∣ ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g𝑀 ) } )
15 8 9 13 14 syl3anc ( 𝜑 → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) supp ( 0g𝑀 ) ) = { 𝑢 ∈ dom ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∣ ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g𝑀 ) } )
16 ovex ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ∈ V
17 eqid ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) = ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) )
18 16 17 dmmpti dom ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) = 𝑉
19 18 a1i ( 𝜑 → dom ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) = 𝑉 )
20 ovex ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) ∈ V
21 nfcv 𝑣 𝑢
22 nfcv 𝑣 ( 𝐴𝑢 )
23 nfcv 𝑣 ( .r𝑀 )
24 nfcsb1v 𝑣 𝑢 / 𝑣 𝐶
25 22 23 24 nfov 𝑣 ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 )
26 fveq2 ( 𝑣 = 𝑢 → ( 𝐴𝑣 ) = ( 𝐴𝑢 ) )
27 csbeq1a ( 𝑣 = 𝑢𝐶 = 𝑢 / 𝑣 𝐶 )
28 26 27 oveq12d ( 𝑣 = 𝑢 → ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) = ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) )
29 21 25 28 17 fvmptf ( ( 𝑢𝑉 ∧ ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) ∈ V ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ‘ 𝑢 ) = ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) )
30 20 29 mpan2 ( 𝑢𝑉 → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ‘ 𝑢 ) = ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) )
31 30 18 eleq2s ( 𝑢 ∈ dom ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ‘ 𝑢 ) = ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) )
32 31 adantl ( ( 𝜑𝑢 ∈ dom ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ‘ 𝑢 ) = ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) )
33 32 neeq1d ( ( 𝜑𝑢 ∈ dom ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ) → ( ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g𝑀 ) ↔ ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) ≠ ( 0g𝑀 ) ) )
34 19 33 rabeqbidva ( 𝜑 → { 𝑢 ∈ dom ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∣ ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g𝑀 ) } = { 𝑢𝑉 ∣ ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) ≠ ( 0g𝑀 ) } )
35 5 fdmd ( 𝜑 → dom 𝐴 = 𝑉 )
36 35 rabeqdv ( 𝜑 → { 𝑢 ∈ dom 𝐴 ∣ ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) } = { 𝑢𝑉 ∣ ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) } )
37 5 ffund ( 𝜑 → Fun 𝐴 )
38 1 fvexi 𝑅 ∈ V
39 38 a1i ( 𝜑𝑅 ∈ V )
40 39 3 elmapd ( 𝜑 → ( 𝐴 ∈ ( 𝑅m 𝑉 ) ↔ 𝐴 : 𝑉𝑅 ) )
41 5 40 mpbird ( 𝜑𝐴 ∈ ( 𝑅m 𝑉 ) )
42 suppval1 ( ( Fun 𝐴𝐴 ∈ ( 𝑅m 𝑉 ) ∧ ( 0g𝑀 ) ∈ 𝑅 ) → ( 𝐴 supp ( 0g𝑀 ) ) = { 𝑢 ∈ dom 𝐴 ∣ ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) } )
43 37 41 13 42 syl3anc ( 𝜑 → ( 𝐴 supp ( 0g𝑀 ) ) = { 𝑢 ∈ dom 𝐴 ∣ ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) } )
44 6 fsuppimpd ( 𝜑 → ( 𝐴 supp ( 0g𝑀 ) ) ∈ Fin )
45 43 44 eqeltrrd ( 𝜑 → { 𝑢 ∈ dom 𝐴 ∣ ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) } ∈ Fin )
46 36 45 eqeltrrd ( 𝜑 → { 𝑢𝑉 ∣ ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) } ∈ Fin )
47 simpr ( ( ( 𝜑𝑢𝑉 ) ∧ ( 𝐴𝑢 ) = ( 0g𝑀 ) ) → ( 𝐴𝑢 ) = ( 0g𝑀 ) )
48 47 oveq1d ( ( ( 𝜑𝑢𝑉 ) ∧ ( 𝐴𝑢 ) = ( 0g𝑀 ) ) → ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) = ( ( 0g𝑀 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) )
49 2 ad2antrr ( ( ( 𝜑𝑢𝑉 ) ∧ ( 𝐴𝑢 ) = ( 0g𝑀 ) ) → 𝑀 ∈ Ring )
50 simplr ( ( ( 𝜑𝑢𝑉 ) ∧ ( 𝐴𝑢 ) = ( 0g𝑀 ) ) → 𝑢𝑉 )
51 4 ralrimiva ( 𝜑 → ∀ 𝑣𝑉 𝐶𝑅 )
52 51 ad2antrr ( ( ( 𝜑𝑢𝑉 ) ∧ ( 𝐴𝑢 ) = ( 0g𝑀 ) ) → ∀ 𝑣𝑉 𝐶𝑅 )
53 rspcsbela ( ( 𝑢𝑉 ∧ ∀ 𝑣𝑉 𝐶𝑅 ) → 𝑢 / 𝑣 𝐶𝑅 )
54 50 52 53 syl2anc ( ( ( 𝜑𝑢𝑉 ) ∧ ( 𝐴𝑢 ) = ( 0g𝑀 ) ) → 𝑢 / 𝑣 𝐶𝑅 )
55 eqid ( .r𝑀 ) = ( .r𝑀 )
56 1 55 11 ringlz ( ( 𝑀 ∈ Ring ∧ 𝑢 / 𝑣 𝐶𝑅 ) → ( ( 0g𝑀 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) = ( 0g𝑀 ) )
57 49 54 56 syl2anc ( ( ( 𝜑𝑢𝑉 ) ∧ ( 𝐴𝑢 ) = ( 0g𝑀 ) ) → ( ( 0g𝑀 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) = ( 0g𝑀 ) )
58 48 57 eqtrd ( ( ( 𝜑𝑢𝑉 ) ∧ ( 𝐴𝑢 ) = ( 0g𝑀 ) ) → ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) = ( 0g𝑀 ) )
59 58 ex ( ( 𝜑𝑢𝑉 ) → ( ( 𝐴𝑢 ) = ( 0g𝑀 ) → ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) = ( 0g𝑀 ) ) )
60 59 necon3d ( ( 𝜑𝑢𝑉 ) → ( ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) ≠ ( 0g𝑀 ) → ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) ) )
61 60 ss2rabdv ( 𝜑 → { 𝑢𝑉 ∣ ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) ≠ ( 0g𝑀 ) } ⊆ { 𝑢𝑉 ∣ ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) } )
62 ssfi ( ( { 𝑢𝑉 ∣ ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) } ∈ Fin ∧ { 𝑢𝑉 ∣ ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) ≠ ( 0g𝑀 ) } ⊆ { 𝑢𝑉 ∣ ( 𝐴𝑢 ) ≠ ( 0g𝑀 ) } ) → { 𝑢𝑉 ∣ ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) ≠ ( 0g𝑀 ) } ∈ Fin )
63 46 61 62 syl2anc ( 𝜑 → { 𝑢𝑉 ∣ ( ( 𝐴𝑢 ) ( .r𝑀 ) 𝑢 / 𝑣 𝐶 ) ≠ ( 0g𝑀 ) } ∈ Fin )
64 34 63 eqeltrd ( 𝜑 → { 𝑢 ∈ dom ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∣ ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g𝑀 ) } ∈ Fin )
65 15 64 eqeltrd ( 𝜑 → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) supp ( 0g𝑀 ) ) ∈ Fin )
66 isfsupp ( ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∈ V ∧ ( 0g𝑀 ) ∈ 𝑅 ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) finSupp ( 0g𝑀 ) ↔ ( Fun ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∧ ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) supp ( 0g𝑀 ) ) ∈ Fin ) ) )
67 9 13 66 syl2anc ( 𝜑 → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) finSupp ( 0g𝑀 ) ↔ ( Fun ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) ∧ ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) supp ( 0g𝑀 ) ) ∈ Fin ) ) )
68 8 65 67 mpbir2and ( 𝜑 → ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( .r𝑀 ) 𝐶 ) ) finSupp ( 0g𝑀 ) )