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

Metamath Proof Explorer

Theorem mplidom

Description: The multivariate polynomials over an integral domain form an integral domain. See ply1idom . (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses mplidom.p 
|- P = ( I mPoly R )
mplidom.i 
|- ( ph -> I e. Fin )
mplidom.r 
|- ( ph -> R e. IDomn )
Assertion mplidom 
|- ( ph -> P e. IDomn )

Proof

Step Hyp Ref Expression
1 mplidom.p 
 |-  P = ( I mPoly R )
2 mplidom.i 
 |-  ( ph -> I e. Fin )
3 mplidom.r 
 |-  ( ph -> R e. IDomn )
4 fveq2 
 |-  ( e = f -> ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` e ) = ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) )
5 4 fveq1d 
 |-  ( e = f -> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` e ) ` { <. x , ( m ` (/) ) >. } ) = ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( m ` (/) ) >. } ) )
6 5 mpteq2dv 
 |-  ( e = f -> ( m e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` e ) ` { <. x , ( m ` (/) ) >. } ) ) = ( m e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( m ` (/) ) >. } ) ) )
7 6 cbvmptv 
 |-  ( e e. ( Base ` ( ( j u. { x } ) mPoly R ) ) |-> ( m e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` e ) ` { <. x , ( m ` (/) ) >. } ) ) ) = ( f e. ( Base ` ( ( j u. { x } ) mPoly R ) ) |-> ( m e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( m ` (/) ) >. } ) ) )
8 fveq1 
 |-  ( m = n -> ( m ` (/) ) = ( n ` (/) ) )
9 8 opeq2d 
 |-  ( m = n -> <. x , ( m ` (/) ) >. = <. x , ( n ` (/) ) >. )
10 9 sneqd 
 |-  ( m = n -> { <. x , ( m ` (/) ) >. } = { <. x , ( n ` (/) ) >. } )
11 10 fveq2d 
 |-  ( m = n -> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( m ` (/) ) >. } ) = ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( n ` (/) ) >. } ) )
12 11 cbvmptv 
 |-  ( m e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( m ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( n ` (/) ) >. } ) )
13 12 mpteq2i 
 |-  ( f e. ( Base ` ( ( j u. { x } ) mPoly R ) ) |-> ( m e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( m ` (/) ) >. } ) ) ) = ( f e. ( Base ` ( ( j u. { x } ) mPoly R ) ) |-> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( n ` (/) ) >. } ) ) )
14 7 13 eqtri 
 |-  ( e e. ( Base ` ( ( j u. { x } ) mPoly R ) ) |-> ( m e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` e ) ` { <. x , ( m ` (/) ) >. } ) ) ) = ( f e. ( Base ` ( ( j u. { x } ) mPoly R ) ) |-> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( n ` (/) ) >. } ) ) )
15 eqid 
 |-  ( Base ` ( ( j u. { x } ) mPoly R ) ) = ( Base ` ( ( j u. { x } ) mPoly R ) )
16 eqid 
 |-  ( ( j u. { x } ) mPoly R ) = ( ( j u. { x } ) mPoly R )
17 eqid 
 |-  ( ( ( j u. { x } ) \ { x } ) mPoly R ) = ( ( ( j u. { x } ) \ { x } ) mPoly R )
18 eqid 
 |-  ( Poly1 ` ( ( ( j u. { x } ) \ { x } ) mPoly R ) ) = ( Poly1 ` ( ( ( j u. { x } ) \ { x } ) mPoly R ) )
19 1 2 3 14 15 16 17 18 mplidomlem 
 |-  ( ph -> P e. IDomn )