Theorem rmsuppss

Description: The support of a mapping of a multiplication of a constant with a function into a ring is a subset of the support of the function. (Contributed by AV, 11-Apr-2019)

	Ref	Expression
Hypothesis	rmsuppss.r	⊢ 𝑅 = ( Base ‘ 𝑀 )
Assertion	rmsuppss	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( 𝐴 supp ( 0g ‘ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rmsuppss.r	⊢ 𝑅 = ( Base ‘ 𝑀 )
2		oveq2	⊢ ( ( 𝐴 ‘ 𝑤 ) = ( 0g ‘ 𝑀 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( 𝐶 ( .r ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) )
3		simpll1	⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → 𝑀 ∈ Ring )
4		simpll3	⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → 𝐶 ∈ 𝑅 )
5		eqid	⊢ ( .r ‘ 𝑀 ) = ( .r ‘ 𝑀 )
6		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
7	1 5 6	ringrz	⊢ ( ( 𝑀 ∈ Ring ∧ 𝐶 ∈ 𝑅 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
8	3 4 7	syl2anc	⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
9	2 8	sylan9eqr	⊢ ( ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑤 ) = ( 0g ‘ 𝑀 ) ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( 0g ‘ 𝑀 ) )
10	9	ex	⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑤 ) = ( 0g ‘ 𝑀 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( 0g ‘ 𝑀 ) ) )
11	10	necon3d	⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) → ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) ) )
12	11	ss2rabdv	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → { 𝑤 ∈ 𝑉 ∣ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑤 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } )
13		elmapi	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 : 𝑉 ⟶ 𝑅 )
14	13	fdmd	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → dom 𝐴 = 𝑉 )
15	14	adantl	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → dom 𝐴 = 𝑉 )
16		rabeq	⊢ ( dom 𝐴 = 𝑉 → { 𝑤 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑤 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } )
17	15 16	syl	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → { 𝑤 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑤 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } )
18	12 17	sseqtrrd	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → { 𝑤 ∈ 𝑉 ∣ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑤 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } )
19		fveq2	⊢ ( 𝑣 = 𝑤 → ( 𝐴 ‘ 𝑣 ) = ( 𝐴 ‘ 𝑤 ) )
20	19	oveq2d	⊢ ( 𝑣 = 𝑤 → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) = ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) )
21	20	cbvmptv	⊢ ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) = ( 𝑤 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) )
22		simpl2	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑉 ∈ 𝑋 )
23		fvexd	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 0g ‘ 𝑀 ) ∈ V )
24		ovexd	⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ∈ V )
25	21 22 23 24	mptsuppd	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) = { 𝑤 ∈ 𝑉 ∣ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) } )
26		elmapfun	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → Fun 𝐴 )
27	26	adantl	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → Fun 𝐴 )
28		simpr	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) )
29		suppval1	⊢ ( ( Fun 𝐴 ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 0g ‘ 𝑀 ) ∈ V ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑤 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } )
30	27 28 23 29	syl3anc	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑤 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } )
31	18 25 30	3sstr4d	⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( 𝐴 supp ( 0g ‘ 𝑀 ) ) )