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	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplidom.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	mplidom.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
Assertion	mplidom	⊢ ( 𝜑 → 𝑃 ∈ IDomn )

Proof

Step	Hyp	Ref	Expression
1		mplidom.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplidom.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
3		mplidom.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
4		fveq2	⊢ ( 𝑒 = 𝑓 → ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑒 ) = ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) )
5	4	fveq1d	⊢ ( 𝑒 = 𝑓 → ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑒 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) = ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) )
6	5	mpteq2dv	⊢ ( 𝑒 = 𝑓 → ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑒 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) = ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) )
7	6	cbvmptv	⊢ ( 𝑒 ∈ ( Base ‘ ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) ) ↦ ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑒 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) ) ↦ ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) )
8		fveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 ‘ ∅ ) = ( 𝑛 ‘ ∅ ) )
9	8	opeq2d	⊢ ( 𝑚 = 𝑛 → ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ = ⟨ 𝑥 , ( 𝑛 ‘ ∅ ) ⟩ )
10	9	sneqd	⊢ ( 𝑚 = 𝑛 → { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } = { ⟨ 𝑥 , ( 𝑛 ‘ ∅ ) ⟩ } )
11	10	fveq2d	⊢ ( 𝑚 = 𝑛 → ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) = ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
12	11	cbvmptv	⊢ ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
13	12	mpteq2i	⊢ ( 𝑓 ∈ ( Base ‘ ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) ) ↦ ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) ) ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
14	7 13	eqtri	⊢ ( 𝑒 ∈ ( Base ‘ ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) ) ↦ ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑒 ) ‘ { ⟨ 𝑥 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) ) ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
15		eqid	⊢ ( Base ‘ ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) ) = ( Base ‘ ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) )
16		eqid	⊢ ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) = ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 )
17		eqid	⊢ ( ( ( 𝑗 ∪ { 𝑥 } ) ∖ { 𝑥 } ) mPoly 𝑅 ) = ( ( ( 𝑗 ∪ { 𝑥 } ) ∖ { 𝑥 } ) mPoly 𝑅 )
18		eqid	⊢ ( Poly1 ‘ ( ( ( 𝑗 ∪ { 𝑥 } ) ∖ { 𝑥 } ) mPoly 𝑅 ) ) = ( Poly1 ‘ ( ( ( 𝑗 ∪ { 𝑥 } ) ∖ { 𝑥 } ) mPoly 𝑅 ) )
19	1 2 3 14 15 16 17 18	mplidomlem	⊢ ( 𝜑 → 𝑃 ∈ IDomn )