Theorem psrmon

Description: A monomial is a power series. (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	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion	psrmon	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐵 )

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		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10	9 4	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
11	9 3	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
12	10 11	ifcld	⊢ ( 𝑅 ∈ Ring → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
13	7 12	syl	⊢ ( 𝜑 → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
15	14	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
16		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
17		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
18	5 17	rabex2	⊢ 𝐷 ∈ V
19	16 18	elmap	⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
20	15 19	sylibr	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
21	5	psrbasfsupp	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
22		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
23	1 9 21 22 6	psrbas	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
24	20 23	eleqtrrd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( Base ‘ 𝑆 ) )
25	24 2	eleqtrrdi	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐵 )