This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑀 ) )