Theorem psrmon

Description: A monomial is a power series. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	psrmon.s	|- S = ( I mPwSer R )
	psrmon.b	|- B = ( Base ` S )
	psrmon.z	|- .0. = ( 0g ` R )
	psrmon.o	|- .1. = ( 1r ` R )
	psrmon.d	|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
	psrmon.i	|- ( ph -> I e. W )
	psrmon.r	|- ( ph -> R e. Ring )
	psrmon.x	|- ( ph -> X e. D )
Assertion	psrmon	|- ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. B )

Proof

Step	Hyp	Ref	Expression
1		psrmon.s	|- S = ( I mPwSer R )
2		psrmon.b	|- B = ( Base ` S )
3		psrmon.z	|- .0. = ( 0g ` R )
4		psrmon.o	|- .1. = ( 1r ` R )
5		psrmon.d	|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
6		psrmon.i	|- ( ph -> I e. W )
7		psrmon.r	|- ( ph -> R e. Ring )
8		psrmon.x	|- ( ph -> X e. D )
9		eqid	|- ( Base ` R ) = ( Base ` R )
10	9 4	ringidcl	|- ( R e. Ring -> .1. e. ( Base ` R ) )
11	9 3	ring0cl	|- ( R e. Ring -> .0. e. ( Base ` R ) )
12	10 11	ifcld	|- ( R e. Ring -> if ( y = X , .1. , .0. ) e. ( Base ` R ) )
13	7 12	syl	|- ( ph -> if ( y = X , .1. , .0. ) e. ( Base ` R ) )
14	13	adantr	|- ( ( ph /\ y e. D ) -> if ( y = X , .1. , .0. ) e. ( Base ` R ) )
15	14	fmpttd	|- ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
16		fvex	|- ( Base ` R ) e. _V
17		ovex	|- ( NN0 ^m I ) e. _V
18	5 17	rabex2	|- D e. _V
19	16 18	elmap	|- ( ( y e. D |-> if ( y = X , .1. , .0. ) ) e. ( ( Base ` R ) ^m D ) <-> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
20	15 19	sylibr	|- ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. ( ( Base ` R ) ^m D ) )
21	5	psrbasfsupp	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
22		eqid	|- ( Base ` S ) = ( Base ` S )
23	1 9 21 22 6	psrbas	|- ( ph -> ( Base ` S ) = ( ( Base ` R ) ^m D ) )
24	20 23	eleqtrrd	|- ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. ( Base ` S ) )
25	24 2	eleqtrrdi	|- ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. B )