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 ⊢ φ → I ∈ Fin
mplidom.r ⊢ φ → R ∈ IDomn
Assertion mplidom ⊢ φ → P ∈ IDomn

Proof

Step Hyp Ref Expression
1 mplidom.p ⊢ P = I mPoly R
2 mplidom.i ⊢ φ → I ∈ Fin
3 mplidom.r ⊢ φ → R ∈ IDomn
4 fveq2 ⊢ e = f → j ∪ x selectVars R ⁡ x ⁡ e = j ∪ x selectVars R ⁡ x ⁡ f
5 4 fveq1d ⊢ e = f → j ∪ x selectVars R ⁡ x ⁡ e ⁡ x m ⁡ ∅ = j ∪ x selectVars R ⁡ x ⁡ f ⁡ x m ⁡ ∅
6 5 mpteq2dv ⊢ e = f → m ∈ ℕ 0 1 𝑜 ⟼ j ∪ x selectVars R ⁡ x ⁡ e ⁡ x m ⁡ ∅ = m ∈ ℕ 0 1 𝑜 ⟼ j ∪ x selectVars R ⁡ x ⁡ f ⁡ x m ⁡ ∅
7 6 cbvmptv ⊢ e ∈ Base j ∪ x mPoly R ⟼ m ∈ ℕ 0 1 𝑜 ⟼ j ∪ x selectVars R ⁡ x ⁡ e ⁡ x m ⁡ ∅ = f ∈ Base j ∪ x mPoly R ⟼ m ∈ ℕ 0 1 𝑜 ⟼ j ∪ 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 ∪ x selectVars R ⁡ x ⁡ f ⁡ x m ⁡ ∅ = j ∪ x selectVars R ⁡ x ⁡ f ⁡ x n ⁡ ∅
12 11 cbvmptv ⊢ m ∈ ℕ 0 1 𝑜 ⟼ j ∪ x selectVars R ⁡ x ⁡ f ⁡ x m ⁡ ∅ = n ∈ ℕ 0 1 𝑜 ⟼ j ∪ x selectVars R ⁡ x ⁡ f ⁡ x n ⁡ ∅
13 12 mpteq2i ⊢ f ∈ Base j ∪ x mPoly R ⟼ m ∈ ℕ 0 1 𝑜 ⟼ j ∪ x selectVars R ⁡ x ⁡ f ⁡ x m ⁡ ∅ = f ∈ Base j ∪ x mPoly R ⟼ n ∈ ℕ 0 1 𝑜 ⟼ j ∪ x selectVars R ⁡ x ⁡ f ⁡ x n ⁡ ∅
14 7 13 eqtri ⊢ e ∈ Base j ∪ x mPoly R ⟼ m ∈ ℕ 0 1 𝑜 ⟼ j ∪ x selectVars R ⁡ x ⁡ e ⁡ x m ⁡ ∅ = f ∈ Base j ∪ x mPoly R ⟼ n ∈ ℕ 0 1 𝑜 ⟼ j ∪ x selectVars R ⁡ x ⁡ f ⁡ x n ⁡ ∅
15 eqid ⊢ Base j ∪ x mPoly R = Base j ∪ x mPoly R
16 eqid ⊢ j ∪ x mPoly R = j ∪ x mPoly R
17 eqid ⊢ j ∪ x ∖ x mPoly R = j ∪ x ∖ x mPoly R
18 eqid ⊢ Poly 1 ⁡ j ∪ x ∖ x mPoly R = Poly 1 ⁡ j ∪ x ∖ x mPoly R
19 1 2 3 14 15 16 17 18 mplidomlem ⊢ φ → P ∈ IDomn