Theorem psrmonmul2

Description: The product of two power series monomials adds the exponent vectors together. Here, the function G is a monomial builder, which maps a bag of variables with the monic monomial with only those variables. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	psrmon.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrmon.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psrmon.z	⊢ 0 = ( 0g ‘ 𝑅 )
	psrmon.o	⊢ 1 = ( 1r ‘ 𝑅 )
	psrmon.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
	psrmon.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	psrmon.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	psrmon.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	psrmonmul.t	⊢ · = ( .r ‘ 𝑆 )
	psrmonmul.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
	psrmonmul.g	⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) )
Assertion	psrmonmul2	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) · ( 𝐺 ‘ 𝑌 ) ) = ( 𝐺 ‘ ( 𝑋 ∘f + 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psrmon.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrmon.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		psrmon.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		psrmon.o	⊢ 1 = ( 1r ‘ 𝑅 )
5		psrmon.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
6		psrmon.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7		psrmon.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		psrmon.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9		psrmonmul.t	⊢ · = ( .r ‘ 𝑆 )
10		psrmonmul.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
11		psrmonmul.g	⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) )
12	1 2 3 4 5 6 7 8 9 10	psrmonmul	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) · ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )
13		eqeq2	⊢ ( 𝑦 = 𝑋 → ( 𝑧 = 𝑦 ↔ 𝑧 = 𝑋 ) )
14	13	ifbid	⊢ ( 𝑦 = 𝑋 → if ( 𝑧 = 𝑦 , 1 , 0 ) = if ( 𝑧 = 𝑋 , 1 , 0 ) )
15	14	mpteq2dv	⊢ ( 𝑦 = 𝑋 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) )
16		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
17	5 16	rabex2	⊢ 𝐷 ∈ V
18	17	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
19	18	mptexd	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) ∈ V )
20	11 15 8 19	fvmptd3	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) )
21		eqeq2	⊢ ( 𝑦 = 𝑌 → ( 𝑧 = 𝑦 ↔ 𝑧 = 𝑌 ) )
22	21	ifbid	⊢ ( 𝑦 = 𝑌 → if ( 𝑧 = 𝑦 , 1 , 0 ) = if ( 𝑧 = 𝑌 , 1 , 0 ) )
23	22	mpteq2dv	⊢ ( 𝑦 = 𝑌 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) )
24	18	mptexd	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) ∈ V )
25	11 23 10 24	fvmptd3	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) )
26	20 25	oveq12d	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) · ( 𝐺 ‘ 𝑌 ) ) = ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑋 , 1 , 0 ) ) · ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑌 , 1 , 0 ) ) ) )
27		eqeq2	⊢ ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) → ( 𝑧 = 𝑦 ↔ 𝑧 = ( 𝑋 ∘f + 𝑌 ) ) )
28	27	ifbid	⊢ ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) → if ( 𝑧 = 𝑦 , 1 , 0 ) = if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
29	28	mpteq2dv	⊢ ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )
30	5	psrbasfsupp	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
31	30	psrbagaddcl	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( 𝑋 ∘f + 𝑌 ) ∈ 𝐷 )
32	8 10 31	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∘f + 𝑌 ) ∈ 𝐷 )
33	18	mptexd	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) ∈ V )
34	11 29 32 33	fvmptd3	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑋 ∘f + 𝑌 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )
35	12 26 34	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) · ( 𝐺 ‘ 𝑌 ) ) = ( 𝐺 ‘ ( 𝑋 ∘f + 𝑌 ) ) )