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	$$⊢S=I\mathrm{mPwSer}R$$
	psrmon.b	$$⊢B={\mathrm{Base}}_S$$
	psrmon.z	$$⊢\underset{\dot{}}{0}=0_R$$
	psrmon.o	$$⊢\underset{\dot{}}{1}=1_R$$
	psrmon.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	psrmon.i	$$⊢\phi \to I\in W$$
	psrmon.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	psrmon.x	$$⊢\phi \to X\in D$$
	psrmonmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	psrmonmul.y	$$⊢\phi \to Y\in D$$
	psrmonmul.g	$$⊢G=\left(y\in D⟼\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
Assertion	psrmonmul2	$$⊢\phi \to G\left(X\right)\underset{\dot{}}{·}G\left(Y\right)=G\left(X{+}_{f}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		psrmon.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrmon.b	$$⊢B={\mathrm{Base}}_S$$
3		psrmon.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		psrmon.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		psrmon.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
6		psrmon.i	$$⊢\phi \to I\in W$$
7		psrmon.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		psrmon.x	$$⊢\phi \to X\in D$$
9		psrmonmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
10		psrmonmul.y	$$⊢\phi \to Y\in D$$
11		psrmonmul.g	$$⊢G=\left(y\in D⟼\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
12	1 2 3 4 5 6 7 8 9 10	psrmonmul	$$⊢\phi \to \left(z\in D⟼if\left(z=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left(z\in D⟼if\left(z=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(z\in D⟼if\left(z=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
13		eqeq2	$$⊢y=X\to \left(z=y\leftrightarrow z=X\right)$$
14	13	ifbid	$$⊢y=X\to if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(z=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
15	14	mpteq2dv	$$⊢y=X\to \left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(z\in D⟼if\left(z=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
16		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
17	5 16	rabex2	$$⊢D\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to D\in \mathrm{V}$$
19	18	mptexd	$$⊢\phi \to \left(z\in D⟼if\left(z=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
20	11 15 8 19	fvmptd3	$$⊢\phi \to G\left(X\right)=\left(z\in D⟼if\left(z=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
21		eqeq2	$$⊢y=Y\to \left(z=y\leftrightarrow z=Y\right)$$
22	21	ifbid	$$⊢y=Y\to if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(z=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
23	22	mpteq2dv	$$⊢y=Y\to \left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(z\in D⟼if\left(z=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
24	18	mptexd	$$⊢\phi \to \left(z\in D⟼if\left(z=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
25	11 23 10 24	fvmptd3	$$⊢\phi \to G\left(Y\right)=\left(z\in D⟼if\left(z=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
26	20 25	oveq12d	$$⊢\phi \to G\left(X\right)\underset{\dot{}}{·}G\left(Y\right)=\left(z\in D⟼if\left(z=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left(z\in D⟼if\left(z=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
27		eqeq2	$$⊢y=X{+}_{f}Y\to \left(z=y\leftrightarrow z=X{+}_{f}Y\right)$$
28	27	ifbid	$$⊢y=X{+}_{f}Y\to if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(z=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
29	28	mpteq2dv	$$⊢y=X{+}_{f}Y\to \left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(z\in D⟼if\left(z=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
30	5	psrbasfsupp	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
31	30	psrbagaddcl	$$⊢\left(X\in D\wedge Y\in D\right)\to X{+}_{f}Y\in D$$
32	8 10 31	syl2anc	$$⊢\phi \to X{+}_{f}Y\in D$$
33	18	mptexd	$$⊢\phi \to \left(z\in D⟼if\left(z=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
34	11 29 32 33	fvmptd3	$$⊢\phi \to G\left(X{+}_{f}Y\right)=\left(z\in D⟼if\left(z=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
35	12 26 34	3eqtr4d	$$⊢\phi \to G\left(X\right)\underset{\dot{}}{·}G\left(Y\right)=G\left(X{+}_{f}Y\right)$$