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 )