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