mplidom - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mplidom		Structured version Visualization version GIF version

Theorem mplidom 33715

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

**Hypotheses**
Ref	Expression
mplidom.p	⊢ 𝑃 = (𝐼 mPoly 𝑅)
mplidom.i	⊢ (𝜑 → 𝐼 ∈ Fin)
mplidom.r	⊢ (𝜑 → 𝑅 ∈ IDomn)

**Assertion**
Ref	Expression
mplidom	⊢ (𝜑 → 𝑃 ∈ IDomn)

Proof of Theorem mplidom Dummy variables 𝑓 𝑗 𝑛 𝑥 𝑒 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplidom.p	. 2 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
2		mplidom.i	. 2 ⊢ (𝜑 → 𝐼 ∈ Fin)
3		mplidom.r	. 2 ⊢ (𝜑 → 𝑅 ∈ IDomn)
4		fveq2 6830	. . . . . 6 ⊢ (𝑒 = 𝑓 → ((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑒) = ((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓))
5	4	fveq1d 6832	. . . . 5 ⊢ (𝑒 = 𝑓 → (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑒)‘{⟨𝑥, (𝑚‘∅)⟩}) = (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑚‘∅)⟩}))
6	5	mpteq2dv 5169	. . . 4 ⊢ (𝑒 = 𝑓 → (𝑚 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑒)‘{⟨𝑥, (𝑚‘∅)⟩})) = (𝑚 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑚‘∅)⟩})))
7	6	cbvmptv 5179	. . 3 ⊢ (𝑒 ∈ (Base‘((𝑗 ∪ {𝑥}) mPoly 𝑅)) ↦ (𝑚 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑒)‘{⟨𝑥, (𝑚‘∅)⟩}))) = (𝑓 ∈ (Base‘((𝑗 ∪ {𝑥}) mPoly 𝑅)) ↦ (𝑚 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑚‘∅)⟩})))
8		fveq1 6829	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝑚‘∅) = (𝑛‘∅))
9	8	opeq2d 4814	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ⟨𝑥, (𝑚‘∅)⟩ = ⟨𝑥, (𝑛‘∅)⟩)
10	9	sneqd 4570	. . . . . 6 ⊢ (𝑚 = 𝑛 → {⟨𝑥, (𝑚‘∅)⟩} = {⟨𝑥, (𝑛‘∅)⟩})
11	10	fveq2d 6834	. . . . 5 ⊢ (𝑚 = 𝑛 → (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑚‘∅)⟩}) = (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑛‘∅)⟩}))
12	11	cbvmptv 5179	. . . 4 ⊢ (𝑚 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑚‘∅)⟩})) = (𝑛 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑛‘∅)⟩}))
13	12	mpteq2i 5171	. . 3 ⊢ (𝑓 ∈ (Base‘((𝑗 ∪ {𝑥}) mPoly 𝑅)) ↦ (𝑚 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑚‘∅)⟩}))) = (𝑓 ∈ (Base‘((𝑗 ∪ {𝑥}) mPoly 𝑅)) ↦ (𝑛 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑛‘∅)⟩})))
14	7, 13	eqtri 2759	. 2 ⊢ (𝑒 ∈ (Base‘((𝑗 ∪ {𝑥}) mPoly 𝑅)) ↦ (𝑚 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑒)‘{⟨𝑥, (𝑚‘∅)⟩}))) = (𝑓 ∈ (Base‘((𝑗 ∪ {𝑥}) mPoly 𝑅)) ↦ (𝑛 ∈ (ℕ₀ ↑_m 1_o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑛‘∅)⟩})))
15		eqid 2736	. 2 ⊢ (Base‘((𝑗 ∪ {𝑥}) mPoly 𝑅)) = (Base‘((𝑗 ∪ {𝑥}) mPoly 𝑅))
16		eqid 2736	. 2 ⊢ ((𝑗 ∪ {𝑥}) mPoly 𝑅) = ((𝑗 ∪ {𝑥}) mPoly 𝑅)
17		eqid 2736	. 2 ⊢ (((𝑗 ∪ {𝑥}) ∖ {𝑥}) mPoly 𝑅) = (((𝑗 ∪ {𝑥}) ∖ {𝑥}) mPoly 𝑅)
18		eqid 2736	. 2 ⊢ (Poly₁‘(((𝑗 ∪ {𝑥}) ∖ {𝑥}) mPoly 𝑅)) = (Poly₁‘(((𝑗 ∪ {𝑥}) ∖ {𝑥}) mPoly 𝑅))
19	1, 2, 3, 14, 15, 16, 17, 18	mplidomlem 33714	1 ⊢ (𝜑 → 𝑃 ∈ IDomn)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2115 ∖ cdif 3883 ∪ cun 3884 ∅c0 4264 {csn 4558 ⟨cop 4564 ↦ cmpt 5156 ‘cfv 6488 (class class class)co 7359 1_oc1o 8391 ↑_m cmap 8766 Fincfn 8886 ℕ₀cn0 12431 Basecbs 17173 IDomncidom 20668 mPoly cmpl 21884 selectVars cslv 22095 Poly₁cpl1 22165

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1970 ax-7 2011 ax-8 2117 ax-9 2125 ax-10 2148 ax-11 2164 ax-12 2185 ax-ext 2708 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7681 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110 ax-addf 11111

This theorem depends on definitions: df-bi 208 df-an 397 df-or 850 df-3or 1089 df-3an 1090 df-tru 1546 df-fal 1556 df-ex 1783 df-nf 1787 df-sb 2070 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3061 df-rmo 3341 df-reu 3342 df-rab 3389 df-v 3430 df-sbc 3727 df-csb 3835 df-dif 3889 df-un 3891 df-in 3893 df-ss 3903 df-pss 3906 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4842 df-int 4881 df-iun 4926 df-iin 4927 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7316 df-ov 7362 df-oprab 7363 df-mpo 7364 df-of 7623 df-ofr 7624 df-om 7810 df-1st 7934 df-2nd 7935 df-supp 8104 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-2o 8399 df-er 8636 df-map 8768 df-pm 8769 df-ixp 8839 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-fsupp 9268 df-sup 9348 df-oi 9418 df-card 9857 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-z 12519 df-dec 12639 df-uz 12783 df-fz 13456 df-fzo 13603 df-seq 13958 df-hash 14287 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-starv 17229 df-sca 17230 df-vsca 17231 df-ip 17232 df-tset 17233 df-ple 17234 df-ds 17236 df-unif 17237 df-hom 17238 df-cco 17239 df-0g 17398 df-gsum 17399 df-prds 17404 df-pws 17406 df-mre 17542 df-mrc 17543 df-acs 17545 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-mhm 18745 df-submnd 18746 df-grp 18906 df-minusg 18907 df-sbg 18908 df-mulg 19038 df-subg 19093 df-ghm 19182 df-cntz 19286 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-srg 20162 df-ring 20210 df-cring 20211 df-rhm 20446 df-rim 20447 df-ric 20449 df-nzr 20488 df-subrng 20521 df-subrg 20545 df-rlreg 20669 df-domn 20670 df-idom 20671 df-lmod 20855 df-lss 20925 df-lsp 20965 df-cnfld 21351 df-assa 21831 df-asp 21832 df-ascl 21833 df-psr 21887 df-mvr 21888 df-mpl 21889 df-opsr 21891 df-evls 22053 df-evl 22054 df-selv 22096 df-psr1 22168 df-vr1 22169 df-ply1 22170 df-coe1 22171 df-mdeg 26041 df-deg1 26042

This theorem is referenced by: (None)

W3C validator