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 ⊢ P = I mPoly R
mplnzr.i ⊢ φ → I ∈ V
mplnzr.r ⊢ φ → R ∈ NzRing
Assertion mplnzr ⊢ φ → P ∈ NzRing

Proof

Step Hyp Ref Expression
1 mplnzr.p ⊢ P = I mPoly R
2 mplnzr.i ⊢ φ → I ∈ V
3 mplnzr.r ⊢ φ → R ∈ NzRing
4 eqid ⊢ I mPwSer R = I mPwSer R
5 4 2 3 psrnzr ⊢ φ → I mPwSer R ∈ NzRing
6 eqid ⊢ Base I mPwSer R = Base I mPwSer R
7 eqid ⊢ 0 R = 0 R
8 eqid ⊢ Base P = Base P
9 1 4 6 7 8 mplbas ⊢ Base P = h ∈ Base I mPwSer R | finSupp 0 R⁡ h
10 9 eqcomi ⊢ h ∈ Base I mPwSer R | finSupp 0 R⁡ h = Base P
11 nzrring ⊢ R ∈ NzRing → R ∈ Ring
12 3 11 syl ⊢ φ → R ∈ Ring
13 4 1 10 2 12 mplsubrg ⊢ φ → h ∈ Base I mPwSer R | finSupp 0 R⁡ h ∈ SubRing ⁡ I mPwSer R
14 eqid ⊢ h ∈ Base I mPwSer R | finSupp 0 R⁡ h = h ∈ Base I mPwSer R | finSupp 0 R⁡ h
15 1 4 6 7 14 mplval ⊢ P = I mPwSer R ↾ 𝑠 h ∈ Base I mPwSer R | finSupp 0 R⁡ h
16 15 subrgnzr ⊢ I mPwSer R ∈ NzRing ∧ h ∈ Base I mPwSer R | finSupp 0 R⁡ h ∈ SubRing ⁡ I mPwSer R → P ∈ NzRing
17 5 13 16 syl2anc ⊢ φ → P ∈ NzRing