Theorem mplnzr

Description: The multivariate polynomials over a nonzero ring form a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	mplnzr.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplnzr.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mplnzr.r	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
Assertion	mplnzr	⊢ ( 𝜑 → 𝑃 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		mplnzr.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplnzr.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		mplnzr.r	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
4		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
5	4 2 3	psrnzr	⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) ∈ NzRing )
6		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
7		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
9	1 4 6 7 8	mplbas	⊢ ( Base ‘ 𝑃 ) = { ℎ ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ ℎ finSupp ( 0g ‘ 𝑅 ) }
10	9	eqcomi	⊢ { ℎ ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ ℎ finSupp ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑃 )
11		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
12	3 11	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
13	4 1 10 2 12	mplsubrg	⊢ ( 𝜑 → { ℎ ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ ℎ finSupp ( 0g ‘ 𝑅 ) } ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
14		eqid	⊢ { ℎ ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ ℎ finSupp ( 0g ‘ 𝑅 ) } = { ℎ ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ ℎ finSupp ( 0g ‘ 𝑅 ) }
15	1 4 6 7 14	mplval	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s { ℎ ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ ℎ finSupp ( 0g ‘ 𝑅 ) } )
16	15	subrgnzr	⊢ ( ( ( 𝐼 mPwSer 𝑅 ) ∈ NzRing ∧ { ℎ ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ ℎ finSupp ( 0g ‘ 𝑅 ) } ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑃 ∈ NzRing )
17	5 13 16	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ NzRing )