P. 336 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33501-33600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	idlsrgtset 33501*	Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐽 = (TopSet‘𝑆))
Theorem	idlsrgmulrval 33502	Value of the ring multiplication for the ideals of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ ⊗ = (.r‘𝑆)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ · = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ⊗ 𝐽) = ((RSpan‘𝑅)‘(𝐼 · 𝐽)))
Theorem	idlsrgmulrcl 33503	Ideals of a ring 𝑅 are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ ⊗ = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ∈ 𝐵)
Theorem	idlsrgmulrss1 33504	In a commutative ring, the product of two ideals is a subset of the first one. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ ⊗ = (.r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ⊆ 𝐼)
Theorem	idlsrgmulrss2 33505	The product of two ideals is a subset of the second one. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ ⊗ = (.r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ⊆ 𝐽)
Theorem	idlsrgmulrssin 33506	In a commutative ring, the product of two ideals is a subset of their intersection. (Contributed by Thierry Arnoux, 17-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ ⊗ = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ⊆ (𝐼 ∩ 𝐽))
Theorem	idlsrgmnd 33507	The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Mnd)
Theorem	idlsrgcmnd 33508	The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑆 ∈ CMnd)
21.3.9.40  Prime Elements
Theorem	rprmval 33509*	The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))})
Theorem	isrprm 33510*	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 33511	A ring prime is an element of the base set. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	rprmdvds 33512	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 33513	A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑄 ≠ 0 )
Theorem	rprmnunit 33514	A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ¬ 𝑄 ∈ 𝑈)
Theorem	rsprprmprmidl 33515	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 33516	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 33517	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 33518	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 33519	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 33520*	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 33521	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 33522	A ring prime element does not divide any ring unit. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ¬ 𝑄 ∥ 𝑇)
Theorem	rprmirredlem 33523	Lemma for rprmirred 33524. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑄 ≠ 0 )    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 = (𝑋 · 𝑌))    &   ⊢ (𝜑 → 𝑄 ∥ 𝑋)    ⇒   ⊢ (𝜑 → 𝑌 ∈ 𝑈)
Theorem	rprmirred 33524	In an integral domain, ring primes are irreducible. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑄 ∈ 𝐼)
Theorem	rprmirredb 33525	In a principal ideal domain, the converse of rprmirred 33524 holds, i.e. irreducible elements are prime. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ PID)    ⇒   ⊢ (𝜑 → 𝐼 = 𝑃)
Theorem	rprmdvdspow 33526	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 33527*	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 33528*	Lemma for 1arithidom 33530. (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 33529*	Lemma for 1arithidom 33530: 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 33530*	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 16974. 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.9.41  Unique factorization domains
Syntax	cufd 33531	Class of unique factorization domains.
class UFD
Definition	df-ufd 33532*	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 33533*	The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝐼 = (PrmIdeal‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅))
Theorem	ufdprmidl 33534*	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 33535	A nonzero unique factorization domain is an integral domain. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ UFD)    ⇒   ⊢ (𝜑 → 𝑅 ∈ IDomn)
Theorem	pidufd 33536	Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ PID)    ⇒   ⊢ (𝜑 → 𝑅 ∈ UFD)
Theorem	1arithufdlem1 33537*	Lemma for 1arithufd 33541. 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 33538*	Lemma for 1arithufd 33541. 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 33539*	Lemma for 1arithufd 33541. 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 33540*	Lemma for 1arithufd 33541. 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 33541*	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 33530, 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 33542	Lemma for dfufd2 33543. (Contributed by Thierry Arnoux, 6-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐼 ∈ (PrmIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑃)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ 𝐼)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼 ∩ 𝑃) ≠ ∅)
Theorem	dfufd2 33543*	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.9.42  The ring of integers
Theorem	zringidom 33544	The ring of integers is an integral domain. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ ℤring ∈ IDomn
Theorem	zringpid 33545	The ring of integers is a principal ideal domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ℤring ∈ PID
Theorem	dfprm3 33546	The (positive) prime elements of the integer ring are the prime numbers. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ℙ = (ℕ ∩ (RPrime‘ℤring))
Theorem	zringfrac 33547*	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.9.43  Univariate Polynomials
Theorem	0ringmon1p 33548	There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → (♯‘𝐵) = 1)    ⇒   ⊢ (𝜑 → 𝑀 = ∅)
Theorem	fply1 33549	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 33550	In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑃 ∈ LVec)
Theorem	evls1fn 33551	Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → 𝑂 Fn 𝑈)
Theorem	evls1dm 33552	The domain of the subring polynomial evaluation function. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → dom 𝑂 = 𝑈)
Theorem	evls1fvf 33553	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 33554	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 33555*	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	ressdeg1 33556	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 33557	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 33558	The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.)
⊢ 𝑆 = (Poly1‘𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (Poly1‘𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝑁 = (Monic1p‘𝐻)    ⇒   ⊢ (𝜑 → 𝑁 = (𝐵 ∩ 𝑀))
Theorem	ressply1invg 33559	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 33560	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 33561	Closure of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) ∈ 𝐵)
Theorem	evls1subd 33562	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 33563	A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl 26172. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑂 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐷‘𝐹) ≤ 0)    ⇒   ⊢ (𝜑 → (𝐹 = 𝑂 ↔ ((coe1‘𝐹)‘0) = 0 ))
Theorem	ply1asclunit 33564	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 33565	In a field 𝐹, a polynomial 𝐶 is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit 33564. (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ 𝐷 = (deg1‘𝐹)    &   ⊢ (𝜑 → 𝐶 ∈ (Base‘𝑃))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (Unit‘𝑃) ↔ (𝐷‘𝐶) = 0))
Theorem	evl1deg1 33566	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 33567	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 33568	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	ply1dg1rt 33569	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 33570	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 33571	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	ply1dg3rt0irred 33572	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 33573	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 33574	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 33575*	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 33576	Two monomials are equal iff their powers are equal. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑀 ↑ 𝑋) = (𝑁 ↑ 𝑋) ↔ 𝑀 = 𝑁))
Theorem	coe1zfv 33577	The coefficients of the zero univariate polynomial. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((coe1‘𝑍)‘𝑁) = 0 )
Theorem	coe1vr1 33578*	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 33579	The degree of the variable polynomial is 1. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → (𝐷‘𝑋) = 1)
Theorem	ply1degltel 33580	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 33581	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 33582	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 33583*	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	ply1gsumz 33584*	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 33585	If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. See also deg1addle 26160. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑌 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ*)    &   ⊢ (𝜑 → (𝐷‘𝐹) < 𝐿)    &   ⊢ (𝜑 → (𝐷‘𝐺) < 𝐿)    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) < 𝐿)
Theorem	ig1pnunit 33586	The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃))    &   ⊢ (𝜑 → 𝐼 ≠ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝐺‘𝐼) ∈ (Unit‘𝑃))
Theorem	ig1pmindeg 33587	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.9.44  Polynomial quotient and polynomial remainder
Theorem	q1pdir 33588	Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ + = (+g‘𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	q1pvsca 33589	Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴) / 𝐶) = (𝐵 × (𝐴 / 𝐶)))
Theorem	r1pvsca 33590	Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴)𝐸𝐷) = (𝐵 × (𝐴𝐸𝐷)))
Theorem	r1p0 33591	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 33592	The polynomial remainder operation is periodic. See modcyc 13957. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + (𝐶 · 𝐵))𝐸𝐵) = (𝐴𝐸𝐵))
Theorem	r1padd1 33593	Addition property of the polynomial remainder operation, similar to modadd1 13959. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷))    &   ⊢ + = (+g‘𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷))
Theorem	r1pid2OLD 33594	Obsolete version of r1pid2 26221 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 33595*	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 33596*	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.9.45  The subring algebra
Theorem	sra1r 33597	The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 1 = (1r‘𝑊))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → 1 = (1r‘𝐴))
Theorem	sradrng 33598	Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing)
Theorem	srasubrg 33599	A subring of the original structure is also a subring of the constructed subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑊))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴))
Theorem	sralvec 33600	Given a sub division ring 𝐹 of a division ring 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.)
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    ⇒   ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)