This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )