P. 337 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)

Type	Label	Description
Statement
21.3.10.43  Prime Elements
Theorem	rprmval 33601*	The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))})
Theorem	isrprm 33602*	Property for 𝑃 to be a prime element in the ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑃 ∈ (RPrime‘𝑅) ↔ (𝑃 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦)))))
Theorem	rprmcl 33603	A ring prime is an element of the base set. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	rprmdvds 33604	If a ring prime 𝑄 divides a product 𝑋 · 𝑌, then it divides either 𝑋 or 𝑌. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∥ (𝑋 · 𝑌))    ⇒   ⊢ (𝜑 → (𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑌))
Theorem	rprmnz 33605	A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑄 ≠ 0 )
Theorem	rprmnunit 33606	A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ¬ 𝑄 ∈ 𝑈)
Theorem	rsprprmprmidl 33607	In a commutative ring, ideals generated by prime elements are prime ideals. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑃 ∈ (RPrime‘𝑅))    ⇒   ⊢ (𝜑 → (𝐾‘{𝑃}) ∈ (PrmIdeal‘𝑅))
Theorem	rsprprmprmidlb 33608	In an integral domain, an ideal generated by a single element is a prime iff that element is prime. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑃 ↔ (𝐾‘{𝑋}) ∈ (PrmIdeal‘𝑅)))
Theorem	rprmndvdsr1 33609	A ring prime element does not divide the ring multiplicative identity. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 1 = (1r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ¬ 𝑄 ∥ 1 )
Theorem	rprmasso 33610	In an integral domain, the associate of a prime is a prime. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∥ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∥ 𝑋)    ⇒   ⊢ (𝜑 → 𝑌 ∈ 𝑃)
Theorem	rprmasso2 33611	In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∥ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑌 ∥ 𝑋)
Theorem	rprmasso3 33612*	In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∥ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ 𝑈 (𝑡 · 𝑋) = 𝑌)
Theorem	unitmulrprm 33613	A ring unit multiplied by a ring prime is a ring prime. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝐼 · 𝑄) ∈ 𝑃)
Theorem	rprmndvdsru 33614	A ring prime element does not divide any ring unit. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ¬ 𝑄 ∥ 𝑇)
Theorem	rprmirredlem 33615	Lemma for rprmirred 33616. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑄 ≠ 0 )    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 = (𝑋 · 𝑌))    &   ⊢ (𝜑 → 𝑄 ∥ 𝑋)    ⇒   ⊢ (𝜑 → 𝑌 ∈ 𝑈)
Theorem	rprmirred 33616	In an integral domain, ring primes are irreducible. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑄 ∈ 𝐼)
Theorem	rprmirredb 33617	In a principal ideal domain, the converse of rprmirred 33616 holds, i.e. irreducible elements are prime. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ PID)    ⇒   ⊢ (𝜑 → 𝐼 = 𝑃)
Theorem	rprmdvdspow 33618	If a prime element divides a ring "power", it divides the term. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑄 ∥ (𝑁 ↑ 𝑋))    ⇒   ⊢ (𝜑 → 𝑄 ∥ 𝑋)
Theorem	rprmdvdsprod 33619*	If a prime element 𝑄 divides a product, then it divides one term. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 finSupp 1 )    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ (𝜑 → 𝑄 ∥ (𝑀 Σg 𝐹))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐹 supp 1 )𝑄 ∥ (𝐹‘𝑥))
Theorem	1arithidomlem1 33620*	Lemma for 1arithidom 33622. (Contributed by Thierry Arnoux, 30-May-2025.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐽 = (0..^(♯‘𝐹))    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ Word 𝑃)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → ∀𝑔 ∈ Word 𝑃(∃𝑘 ∈ 𝑈 (𝑀 Σg 𝐹) = (𝑘 · (𝑀 Σg 𝑔)) → ∃𝑤∃𝑢 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))(𝑤:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ 𝑔 = (𝑢 ∘f · (𝐹 ∘ 𝑤)))))    &   ⊢ (𝜑 → 𝐻 ∈ Word 𝑃)    &   ⊢ (𝜑 → ∃𝑘 ∈ 𝑈 (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑘 · (𝑀 Σg 𝐻)))    &   ⊢ (𝜑 → 𝐾 ∈ (0..^(♯‘𝐻)))    &   ⊢ (𝜑 → 𝑄(∥r‘𝑅)(𝐻‘𝐾))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑈)    &   ⊢ (𝜑 → (𝑇 · 𝑄) = (𝐻‘𝐾))    &   ⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))    &   ⊢ (𝜑 → (𝐻 ∘ 𝑆) = (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻‘𝐾)”⟩))    &   ⊢ (𝜑 → 𝑁 ∈ 𝑈)    &   ⊢ (𝜑 → (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑁 · (𝑀 Σg 𝐻)))    ⇒   ⊢ (𝜑 → ∃𝑐∃𝑑 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))(𝑐:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) = (𝑑 ∘f · (𝐹 ∘ 𝑐))))
Theorem	1arithidomlem2 33621*	Lemma for 1arithidom 33622: induction step. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐽 = (0..^(♯‘𝐹))    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ Word 𝑃)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → ∀𝑔 ∈ Word 𝑃(∃𝑘 ∈ 𝑈 (𝑀 Σg 𝐹) = (𝑘 · (𝑀 Σg 𝑔)) → ∃𝑤∃𝑢 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))(𝑤:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ 𝑔 = (𝑢 ∘f · (𝐹 ∘ 𝑤)))))    &   ⊢ (𝜑 → 𝐻 ∈ Word 𝑃)    &   ⊢ (𝜑 → ∃𝑘 ∈ 𝑈 (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑘 · (𝑀 Σg 𝐻)))    &   ⊢ (𝜑 → 𝐾 ∈ (0..^(♯‘𝐻)))    &   ⊢ (𝜑 → 𝑄(∥r‘𝑅)(𝐻‘𝐾))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑈)    &   ⊢ (𝜑 → (𝑇 · 𝑄) = (𝐻‘𝐾))    &   ⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))    &   ⊢ (𝜑 → (𝐻 ∘ 𝑆) = (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻‘𝐾)”⟩))    &   ⊢ (𝜑 → 𝑁 ∈ 𝑈)    &   ⊢ (𝜑 → (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑁 · (𝑀 Σg 𝐻)))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑈 ↑m (0..^(♯‘𝐹))))    &   ⊢ (𝜑 → 𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)))    &   ⊢ (𝜑 → ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) = (𝐷 ∘f · (𝐹 ∘ 𝐶)))    ⇒   ⊢ (𝜑 → (((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ ◡𝑆):(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩)))–1-1-onto→(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) ∧ 𝐻 = (((𝐷 ++ ⟨“𝑇”⟩) ∘ ◡𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ ◡𝑆)))))
Theorem	1arithidom 33622*	Uniqueness of prime factorizations in an integral domain 𝑅. Given two equal products 𝐹 and 𝐺 of prime elements, 𝐹 and 𝐺 are equal up to a renumbering 𝑤 and a multiplication by units 𝑢. See also 1arith 16860. Chapter VII, Paragraph 3, Section 3, Proposition 2 of [BourbakiCAlg2], p. 228. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐽 = (0..^(♯‘𝐹))    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ Word 𝑃)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺))    ⇒   ⊢ (𝜑 → ∃𝑤∃𝑢 ∈ (𝑈 ↑m 𝐽)(𝑤:𝐽–1-1-onto→𝐽 ∧ 𝐺 = (𝑢 ∘f · (𝐹 ∘ 𝑤))))
21.3.10.44  Unique factorization domains
Syntax	cufd 33623	Class of unique factorization domains.
class UFD
Definition	df-ufd 33624*	Define the class of unique factorization domains. A unique factorization domain (UFD for short), is an integral domain such that every nonzero prime ideal contains a prime element (this is a characterization due to Irving Kaplansky). A UFD is sometimes also called a "factorial ring" following the terminology of Bourbaki. (Contributed by Mario Carneiro, 17-Feb-2015.) Exclude the 0 prime ideal. (Revised by Thierry Arnoux, 9-May-2025.) Exclude the 0 ring. (Revised by Thierry Arnoux, 14-Jun-2025.)
⊢ UFD = {𝑟 ∈ IDomn ∣ ∀𝑖 ∈ ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅}
Theorem	isufd 33625*	The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝐼 = (PrmIdeal‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅))
Theorem	ufdprmidl 33626*	In a unique factorization domain 𝑅, a nonzero prime ideal 𝐽 contains a prime element 𝑝. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐼 = (PrmIdeal‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐽 ≠ { 0 })    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝑃 𝑝 ∈ 𝐽)
Theorem	ufdidom 33627	A nonzero unique factorization domain is an integral domain. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ UFD)    ⇒   ⊢ (𝜑 → 𝑅 ∈ IDomn)
Theorem	pidufd 33628	Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ PID)    ⇒   ⊢ (𝜑 → 𝑅 ∈ UFD)
Theorem	1arithufdlem1 33629*	Lemma for 1arithufd 33633. The set 𝑆 of elements which can be written as a product of primes is not empty. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    ⇒   ⊢ (𝜑 → 𝑆 ≠ ∅)
Theorem	1arithufdlem2 33630*	Lemma for 1arithufd 33633. The set 𝑆 of elements which can be written as a product of primes is multiplicatively closed. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑆)
Theorem	1arithufdlem3 33631*	Lemma for 1arithufd 33633. If a product (𝑌 · 𝑋) can be written as a product of primes, with 𝑋 non-unit, nonzero, so can 𝑋. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑆)
Theorem	1arithufdlem4 33632*	Lemma for 1arithufd 33633. Nonzero ring, non-field case. Those trivial cases are handled in the final proof. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑆)
Theorem	1arithufd 33633*	Existence of a factorization into irreducible elements in a unique factorization domain. Any non-zero, non-unit element 𝑋 of a UFD 𝑅 can be written as a product of primes 𝑓. As shown in 1arithidom 33622, that factorization is unique, up to the order of the factors and multiplication by units. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ Word 𝑃𝑋 = (𝑀 Σg 𝑓))
Theorem	dfufd2lem 33634	Lemma for dfufd2 33635. (Contributed by Thierry Arnoux, 6-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐼 ∈ (PrmIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑃)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ 𝐼)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼 ∩ 𝑃) ≠ ∅)
Theorem	dfufd2 33635*	Alternative definition of unique factorization domain (UFD). This is often the textbook definition. Chapter VII, Paragraph 3, Section 3, Proposition 2 of [BourbakiCAlg2], p. 228. (Contributed by Thierry Arnoux, 6-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)))
21.3.10.45  The ring of integers
Theorem	zringidom 33636	The ring of integers is an integral domain. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ ℤring ∈ IDomn
Theorem	zringpid 33637	The ring of integers is a principal ideal domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ℤring ∈ PID
Theorem	dfprm3 33638	The (positive) prime elements of the integer ring are the prime numbers. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ℙ = (ℕ ∩ (RPrime‘ℤring))
Theorem	zringfrac 33639*	The field of fractions of the ring of integers is isomorphic to the field of the rational numbers. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ ∼ = (ℤring ~RL (ℤ ∖ {0}))    &   ⊢ 𝐹 = (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )    ⇒   ⊢ 𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤring))
21.3.10.46  Associative Algebra
Theorem	assaassd 33640	Left-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))
Theorem	assaassrd 33641	Right-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))
21.3.10.47  Univariate Polynomials
Theorem	0ringmon1p 33642	There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → (♯‘𝐵) = 1)    ⇒   ⊢ (𝜑 → 𝑀 = ∅)
Theorem	fply1 33643	Conditions for a function to be a univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (Base‘(Poly1‘𝑅))    &   ⊢ (𝜑 → 𝐹:(ℕ0 ↑m 1o)⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑃)
Theorem	ply1lvec 33644	In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑃 ∈ LVec)
Theorem	evls1fn 33645	Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → 𝑂 Fn 𝑈)
Theorem	evls1dm 33646	The domain of the subring polynomial evaluation function. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → dom 𝑂 = 𝑈)
Theorem	evls1fvf 33647	The subring evaluation function for a univariate polynomial as a function, with domain and codomain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑂‘𝑄):𝐵⟶𝐵)
Theorem	evl1fvf 33648	The univariate polynomial evaluation function as a function, with domain and codomain. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑂‘𝑄):𝐵⟶𝐵)
Theorem	evl1fpws 33649*	Evaluation of a univariate polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐴 = (coe1‘𝑀)    ⇒   ⊢ (𝜑 → (𝑂‘𝑀) = (𝑥 ∈ 𝐵 ↦ (𝑅 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))))
Theorem	ressply1evls1 33650	Subring evaluation of a univariate polynomial is the same as the subring evaluation in the bigger ring. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝐺 = (𝐸 ↾s 𝑅)    &   ⊢ 𝑂 = (𝐸 evalSub1 𝑆)    &   ⊢ 𝑄 = (𝐺 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝐾 = (𝐸 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝐸))    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝐺))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘𝐹) = ((𝑂‘𝐹) ↾ 𝑅))
Theorem	ressdeg1 33651	The degree of a univariate polynomial in a structure restriction. (Contributed by Thierry Arnoux, 20-Jan-2025.)
⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝐷‘𝑃) = ((deg1‘𝐻)‘𝑃))
Theorem	ressply10g 33652	A restricted polynomial algebra has the same group identity (zero polynomial). (Contributed by Thierry Arnoux, 20-Jan-2025.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑍 = (0g‘𝑆)    ⇒   ⊢ (𝜑 → 𝑍 = (0g‘𝑈))
Theorem	ressply1mon1p 33653	The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝑁 = (Monic1p‘𝐻)    ⇒   ⊢ (𝜑 → 𝑁 = (𝐵 ∩ 𝑀))
Theorem	ressply1invg 33654	An element of a restricted polynomial algebra has the same group inverse. (Contributed by Thierry Arnoux, 30-Jan-2025.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((invg‘𝑈)‘𝑋) = ((invg‘𝑃)‘𝑋))
Theorem	ressply1sub 33655	A restricted polynomial algebra has the same subtraction operation. (Contributed by Thierry Arnoux, 30-Jan-2025.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(-g‘𝑈)𝑌) = (𝑋(-g‘𝑃)𝑌))
Theorem	ressasclcl 33656	Closure of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) ∈ 𝐵)
Theorem	evls1subd 33657	Univariate polynomial evaluation of a difference of polynomials. (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐷 = (-g‘𝑊)    &   ⊢ − = (-g‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑀𝐷𝑁))‘𝐶) = (((𝑄‘𝑀)‘𝐶) − ((𝑄‘𝑁)‘𝐶)))
Theorem	deg1le0eq0 33658	A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl 26079. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑂 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐷‘𝐹) ≤ 0)    ⇒   ⊢ (𝜑 → (𝐹 = 𝑂 ↔ ((coe1‘𝐹)‘0) = 0 ))
Theorem	ply1asclunit 33659	A non-zero scalar polynomial over a field 𝐹 is a unit. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐴‘𝑌) ∈ (Unit‘𝑃))
Theorem	ply1unit 33660	In a field 𝐹, a polynomial 𝐶 is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit 33659. (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ 𝐷 = (deg1‘𝐹)    &   ⊢ (𝜑 → 𝐶 ∈ (Base‘𝑃))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (Unit‘𝑃) ↔ (𝐷‘𝐶) = 0))
Theorem	evl1deg1 33661	Evaluation of a univariate polynomial of degree 1. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐶 = (coe1‘𝑀)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐶‘1)    &   ⊢ 𝐵 = (𝐶‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝑀) = 1)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = ((𝐴 · 𝑋) + 𝐵))
Theorem	evl1deg2 33662	Evaluation of a univariate polynomial of degree 2. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐹 = (coe1‘𝑀)    &   ⊢ 𝐸 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐹‘2)    &   ⊢ 𝐵 = (𝐹‘1)    &   ⊢ 𝐶 = (𝐹‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐸‘𝑀) = 2)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐵 · 𝑋) + 𝐶)))
Theorem	evl1deg3 33663	Evaluation of a univariate polynomial of degree 3. (Contributed by Thierry Arnoux, 14-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐹 = (coe1‘𝑀)    &   ⊢ 𝐸 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐹‘3)    &   ⊢ 𝐵 = (𝐹‘2)    &   ⊢ 𝐶 = (𝐹‘1)    &   ⊢ 𝐷 = (𝐹‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐸‘𝑀) = 3)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = (((𝐴 · (3 ↑ 𝑋)) + (𝐵 · (2 ↑ 𝑋))) + ((𝐶 · 𝑋) + 𝐷)))
Theorem	evls1monply1 33664	Subring evaluation of a scaled monomial. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑋 = (var1‘𝑈)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑊))    &   ⊢ ∧ = (.g‘(mulGrp‘𝑆))    &   ⊢ ∗ = ( ·𝑠 ‘𝑊)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴 ∗ (𝑁 ↑ 𝑋)))‘𝑌) = (𝐴 · (𝑁 ∧ 𝑌)))
Theorem	ply1dg1rt 33665	Express the root − 𝐵 / 𝐴 of a polynomial 𝐴 · 𝑋 + 𝐵 of degree 1 over a field. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝐺) = 1)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐶 = (coe1‘𝐺)    &   ⊢ 𝐴 = (𝐶‘1)    &   ⊢ 𝐵 = (𝐶‘0)    &   ⊢ 𝑍 = ((𝑁‘𝐵) / 𝐴)    ⇒   ⊢ (𝜑 → (◡(𝑂‘𝐺) “ { 0 }) = {𝑍})
Theorem	ply1dg1rtn0 33666	Polynomials of degree 1 over a field always have some roots. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝐺) = 1)    ⇒   ⊢ (𝜑 → (◡(𝑂‘𝐺) “ { 0 }) ≠ ∅)
Theorem	ply1mulrtss 33667	The roots of a factor 𝐹 are also roots of the product of polynomials (𝐹 · 𝐺). (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    &   ⊢ · = (.r‘𝑃)    ⇒   ⊢ (𝜑 → (◡(𝑂‘𝐹) “ { 0 }) ⊆ (◡(𝑂‘(𝐹 · 𝐺)) “ { 0 }))
Theorem	deg1prod 33668*	Degree of a product of polynomials. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶(𝐵 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐷‘(𝑀 Σg 𝐹)) = Σ𝑘 ∈ 𝐴 (𝐷‘(𝐹‘𝑘)))
Theorem	ply1dg3rt0irred 33669	If a cubic polynomial over a field has no roots, it is irreducible. (Proposed by Saveliy Skresanov, 5-Jun-2025.) (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 0 = (0g‘𝐹)    &   ⊢ 𝑂 = (eval1‘𝐹)    &   ⊢ 𝐷 = (deg1‘𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → (◡(𝑂‘𝑄) “ { 0 }) = ∅)    &   ⊢ (𝜑 → (𝐷‘𝑄) = 3)    ⇒   ⊢ (𝜑 → 𝑄 ∈ (Irred‘𝑃))
Theorem	m1pmeq 33670	If two monic polynomials 𝐼 and 𝐽 differ by a unit factor 𝐾, then they are equal. (Contributed by Thierry Arnoux, 27-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝑀 = (Monic1p‘𝐹)    &   ⊢ 𝑈 = (Unit‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 = (𝐾 · 𝐽))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐽)
Theorem	ply1fermltl 33671	Fermat's little theorem for polynomials. If 𝑃 is prime, Then (𝑋 + 𝐴)↑𝑃 = ((𝑋↑𝑃) + 𝐴) modulo 𝑃. (Contributed by Thierry Arnoux, 24-Jul-2024.)
⊢ 𝑍 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝑊 = (Poly1‘𝑍)    &   ⊢ 𝑋 = (var1‘𝑍)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (mulGrp‘𝑊)    &   ⊢ ↑ = (.g‘𝑁)    &   ⊢ 𝐶 = (algSc‘𝑊)    &   ⊢ 𝐴 = (𝐶‘((ℤRHom‘𝑍)‘𝐸))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐸 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝐴)) = ((𝑃 ↑ 𝑋) + 𝐴))
Theorem	coe1mon 33672*	Coefficient vector of a monomial. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → (coe1‘(𝑁 ↑ 𝑋)) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 𝑁, 1 , 0 )))
Theorem	ply1moneq 33673	Two monomials are equal iff their powers are equal. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑀 ↑ 𝑋) = (𝑁 ↑ 𝑋) ↔ 𝑀 = 𝑁))
Theorem	ply1coedeg 33674*	Decompose a univariate polynomial 𝐾 as a sum of powers, up to its degree 𝐷. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐷 = ((deg1‘𝑅)‘𝐾)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐾 = (𝑃 Σg (𝑘 ∈ (0...𝐷) ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
Theorem	coe1zfv 33675	The coefficients of the zero univariate polynomial. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((coe1‘𝑍)‘𝑁) = 0 )
Theorem	coe1vr1 33676*	Polynomial coefficient of the variable. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → (coe1‘𝑋) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 1, 1 , 0 )))
Theorem	deg1vr 33677	The degree of the variable polynomial is 1. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → (𝐷‘𝑋) = 1)
Theorem	vr1nz 33678	A univariate polynomial variable cannot be the zero polynomial. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑋 = (var1‘𝑈)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ NzRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑍)
Theorem	ply1degltel 33679	Characterize elementhood in the set 𝑆 of polynomials of degree less than 𝑁. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ≤ (𝑁 − 1))))
Theorem	ply1degleel 33680	Characterize elementhood in the set 𝑆 of polynomials of degree less than 𝑁. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) < 𝑁)))
Theorem	ply1degltlss 33681	The space 𝑆 of the univariate polynomials of degree less than 𝑁 forms a vector subspace. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃))
Theorem	gsummoncoe1fzo 33682*	A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐿 ∈ (0..^𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝑘 = 𝐿 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = 𝐶)
Theorem	gsummoncoe1fz 33683*	A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. See gsummoncoe1fzo 33682. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...𝐷)𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐿 ∈ (0...𝐷))    &   ⊢ (𝑘 = 𝐿 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ (0...𝐷) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = 𝐶)
Theorem	ply1gsumz 33684*	If a polynomial given as a sum of scaled monomials by factors 𝐴 is the zero polynomial, then all factors 𝐴 are zero. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐴:(0..^𝑁)⟶𝐵)    &   ⊢ (𝜑 → (𝑃 Σg (𝐴 ∘f ( ·𝑠 ‘𝑃)𝐹)) = 𝑍)    ⇒   ⊢ (𝜑 → 𝐴 = ((0..^𝑁) × { 0 }))
Theorem	deg1addlt 33685	If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. See also deg1addle 26067. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑌 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ*)    &   ⊢ (𝜑 → (𝐷‘𝐹) < 𝐿)    &   ⊢ (𝜑 → (𝐷‘𝐺) < 𝐿)    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) < 𝐿)
Theorem	ig1pnunit 33686	The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃))    &   ⊢ (𝜑 → 𝐼 ≠ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝐺‘𝐼) ∈ (Unit‘𝑃))
Theorem	ig1pmindeg 33687	The polynomial ideal generator is of minimum degree. (Contributed by Thierry Arnoux, 19-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃))    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐷‘(𝐺‘𝐼)) ≤ (𝐷‘𝐹))
21.3.10.48  Polynomial quotient and polynomial remainder
Theorem	q1pdir 33688	Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ + = (+g‘𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	q1pvsca 33689	Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴) / 𝐶) = (𝐵 × (𝐴 / 𝐶)))
Theorem	r1pvsca 33690	Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴)𝐸𝐷) = (𝐵 × (𝐴𝐸𝐷)))
Theorem	r1p0 33691	Polynomial remainder operation of a division of the zero polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ (𝜑 → ( 0 𝐸𝐷) = 0 )
Theorem	r1pcyc 33692	The polynomial remainder operation is periodic. See modcyc 13831. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + (𝐶 · 𝐵))𝐸𝐵) = (𝐴𝐸𝐵))
Theorem	r1padd1 33693	Addition property of the polynomial remainder operation, similar to modadd1 13833. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷))    &   ⊢ + = (+g‘𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷))
Theorem	r1pid2OLD 33694	Obsolete version of r1pid2 26128 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 2-Apr-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (𝐷‘𝐴) < (𝐷‘𝐵)))
Theorem	r1plmhm 33695*	The univariate polynomial remainder function 𝐹 is a module homomorphism. Its image (𝐹 “s 𝑃) is sometimes called the "ring of remainders" (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑈 ↦ (𝑓𝐸𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑁)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 LMHom (𝐹 “s 𝑃)))
Theorem	r1pquslmic 33696*	The univariate polynomial remainder ring (𝐹 “s 𝑃) is module isomorphic with the quotient ring. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑈 ↦ (𝑓𝐸𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑁)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝐾))    ⇒   ⊢ (𝜑 → 𝑄 ≃𝑚 (𝐹 “s 𝑃))
21.3.10.49  Multivariate Polynomials
Theorem	psrbasfsupp 33697	Rewrite a finite support for nonnegative integers : For functions mapping a set 𝐼 to the nonnegative integers, having finite support can also be written as having a finite preimage of the positive integers. The latter expression is used for example in psrbas 21894, but with the former expression, theorems about finite support can be used more directly. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ 𝑓 finSupp 0}    ⇒   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
Syntax	cextv 33698	Extend class notation with the "variable extension" function.
class extendVars
Definition	df-extv 33699*	Define the "variable extension" function. The function ((𝐼extendVars𝑅)‘𝐴) converts polynomials with variables indexed by (𝐼 ∖ {𝐴}) into polynomials indexed by 𝐼, and therefore maps elements of ((𝐼 ∖ {𝐴}) mPoly 𝑅) onto (𝐼 mPoly 𝑅). (Contributed by Thierry Arnoux, 20-Jan-2026.)
⊢ extendVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑎 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘((𝑖 ∖ {𝑎}) mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟))))))
Theorem	extvval 33700*	Value of the "variable extension" function. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐽 = (𝐼 ∖ {𝑎})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    ⇒   ⊢ (𝜑 → (𝐼extendVars𝑅) = (𝑎 ∈ 𝐼 ↦ (𝑓 ∈ 𝑀 ↦ (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝐼 ∖ {𝑎}))), 0 )))))