Theorem psrmon

Description: A monomial is a power series. (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$$
Assertion	psrmon	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$

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		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10	9 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
11	9 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
12	10 11	ifcld	$$⊢R\in \mathrm{Ring}\to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
13	7 12	syl	$$⊢\phi \to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
14	13	adantr	$$⊢\left(\phi \wedge y\in D\right)\to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
15	14	fmpttd	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
16		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
17		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
18	5 17	rabex2	$$⊢D\in \mathrm{V}$$
19	16 18	elmap	$$⊢\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \left({{\mathrm{Base}}_R}^D\right)\leftrightarrow \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
20	15 19	sylibr	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \left({{\mathrm{Base}}_R}^D\right)$$
21	5	psrbasfsupp	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
22		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
23	1 9 21 22 6	psrbas	$$⊢\phi \to {\mathrm{Base}}_S={{\mathrm{Base}}_R}^D$$
24	20 23	eleqtrrd	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_S$$
25	24 2	eleqtrrdi	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$