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 
|- P = ( I mPoly R )
mplnzr.i 
|- ( ph -> I e. V )
mplnzr.r 
|- ( ph -> R e. NzRing )
Assertion mplnzr 
|- ( ph -> P e. NzRing )

Proof

Step Hyp Ref Expression
1 mplnzr.p 
 |-  P = ( I mPoly R )
2 mplnzr.i 
 |-  ( ph -> I e. V )
3 mplnzr.r 
 |-  ( ph -> R e. NzRing )
4 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
5 4 2 3 psrnzr 
 |-  ( ph -> ( I mPwSer R ) e. NzRing )
6 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 eqid 
 |-  ( Base ` P ) = ( Base ` P )
9 1 4 6 7 8 mplbas 
 |-  ( Base ` P ) = { h e. ( Base ` ( I mPwSer R ) ) | h finSupp ( 0g ` R ) }
10 9 eqcomi 
 |-  { h e. ( Base ` ( I mPwSer R ) ) | h finSupp ( 0g ` R ) } = ( Base ` P )
11 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
12 3 11 syl 
 |-  ( ph -> R e. Ring )
13 4 1 10 2 12 mplsubrg 
 |-  ( ph -> { h e. ( Base ` ( I mPwSer R ) ) | h finSupp ( 0g ` R ) } e. ( SubRing ` ( I mPwSer R ) ) )
14 eqid 
 |-  { h e. ( Base ` ( I mPwSer R ) ) | h finSupp ( 0g ` R ) } = { h e. ( Base ` ( I mPwSer R ) ) | h finSupp ( 0g ` R ) }
15 1 4 6 7 14 mplval 
 |-  P = ( ( I mPwSer R ) |`s { h e. ( Base ` ( I mPwSer R ) ) | h finSupp ( 0g ` R ) } )
16 15 subrgnzr 
 |-  ( ( ( I mPwSer R ) e. NzRing /\ { h e. ( Base ` ( I mPwSer R ) ) | h finSupp ( 0g ` R ) } e. ( SubRing ` ( I mPwSer R ) ) ) -> P e. NzRing )
17 5 13 16 syl2anc 
 |-  ( ph -> P e. NzRing )