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 ⊢ 𝑃 = ( 𝐼 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 )