P. 147 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zringabl 14601	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ Abel
Theorem	zringgrp 14602	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
⊢ ℤring ∈ Grp
Theorem	zringbas 14603	The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.)
⊢ ℤ = (Base‘ℤring)
Theorem	zringplusg 14604	The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ + = (+g‘ℤring)
Theorem	zringmulg 14605	The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴(.g‘ℤring)𝐵) = (𝐴 · 𝐵))
Theorem	zringmulr 14606	The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ · = (.r‘ℤring)
Theorem	zring0 14607	The zero element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ 0 = (0g‘ℤring)
Theorem	zring1 14608	The unity element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ 1 = (1r‘ℤring)
Theorem	zringnzr 14609	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ℤring ∈ NzRing
Theorem	dvdsrzring 14610	Ring divisibility in the ring of integers corresponds to ordinary divisibility in ℤ. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.)
⊢ ∥ = (∥r‘ℤring)
Theorem	zringinvg 14611	The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ (𝐴 ∈ ℤ → -𝐴 = ((invg‘ℤring)‘𝐴))
Theorem	zringsubgval 14612	Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.)
⊢ − = (-g‘ℤring)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	zringmpg 14613	The multiplicative group of the ring of integers is the restriction of the multiplicative group of the complex numbers to the integers. (Contributed by AV, 15-Jun-2019.)
⊢ ((mulGrp‘ℂfld) ↾s ℤ) = (mulGrp‘ℤring)
Theorem	expghmap 14614*	Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) (Revised by Jim Kingdon, 11-Sep-2025.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ 𝑈 = (𝑀 ↾s {𝑧 ∈ ℂ ∣ 𝑧 # 0})    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝑥 ∈ ℤ ↦ (𝐴↑𝑥)) ∈ (ℤring GrpHom 𝑈))
Theorem	mulgghm2 14615*	The powers of a group element give a homomorphism from ℤ to a group. The name 1 should not be taken as a constraint as it may be any group element. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅))
Theorem	mulgrhm 14616*	The powers of the element 1 give a ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐹 ∈ (ℤring RingHom 𝑅))
Theorem	mulgrhm2 14617*	The powers of the element 1 give the unique ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (ℤring RingHom 𝑅) = {𝐹})
7.7.3  Algebraic constructions based on the complex numbers
Syntax	czrh 14618	Map the rationals into a field, or the integers into a ring.
class ℤRHom
Syntax	czlm 14619	Augment an abelian group with vector space operations to turn it into a ℤ-module.
class ℤMod
Syntax	czn 14620	The ring of integers modulo 𝑛.
class ℤ/nℤ
Definition	df-zrh 14621	Define the unique homomorphism from the integers into a ring. This encodes the usual notation of 𝑛 = 1r + 1r + ... + 1r for integers (see also df-mulg 13700). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))
Definition	df-zlm 14622	Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝑔)⟩))
Definition	df-zn 14623*	Define the ring of integers mod 𝑛. This is literally the quotient ring of ℤ by the ideal 𝑛ℤ, but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤ/nℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))
Theorem	zrhval 14624	Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ 𝐿 = ∪ (ℤring RingHom 𝑅)
Theorem	zrhvalg 14625	Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐿 = ∪ (ℤring RingHom 𝑅))
Theorem	zrhval2 14626*	Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )))
Theorem	zrhmulg 14627	Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 ))
Theorem	zrhex 14628	Set existence for ℤRHom. (Contributed by Jim Kingdon, 19-May-2025.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐿 ∈ V)
Theorem	zrhrhmb 14629	The ℤRHom homomorphism is the unique ring homomorphism from ℤ. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐹 ∈ (ℤring RingHom 𝑅) ↔ 𝐹 = 𝐿))
Theorem	zrhrhm 14630	The ℤRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅))
Theorem	zrh1 14631	Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 )
Theorem	zrh0 14632	Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 )
Theorem	zrhpropd 14633*	The ℤ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (ℤRHom‘𝐾) = (ℤRHom‘𝐿))
Theorem	zlmval 14634	Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑊 = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))
Theorem	zlmlemg 14635	Lemma for zlmbasg 14636 and zlmplusgg 14637. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ∈ ℕ    &   ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx)    &   ⊢ (𝐸‘ndx) ≠ ( ·𝑠 ‘ndx)    ⇒   ⊢ (𝐺 ∈ 𝑉 → (𝐸‘𝐺) = (𝐸‘𝑊))
Theorem	zlmbasg 14636	Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐵 = (Base‘𝑊))
Theorem	zlmplusgg 14637	Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → + = (+g‘𝑊))
Theorem	zlmmulrg 14638	Ring operation of a ℤ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → · = (.r‘𝑊))
Theorem	zlmsca 14639	Scalar ring of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → ℤring = (Scalar‘𝑊))
Theorem	zlmvscag 14640	Scalar multiplication operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → · = ( ·𝑠 ‘𝑊))
Theorem	znlidl 14641	The set 𝑛ℤ is an ideal in ℤ. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    ⇒   ⊢ (𝑁 ∈ ℤ → (𝑆‘{𝑁}) ∈ (LIdeal‘ℤring))
Theorem	zncrng2 14642	Making a commutative ring as a quotient of ℤ and 𝑛ℤ. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    ⇒   ⊢ (𝑁 ∈ ℤ → 𝑈 ∈ CRing)
Theorem	znval 14643	The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑈) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 = (𝑈 sSet ⟨(le‘ndx), ≤ ⟩))
Theorem	znle 14644	The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑈) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹))
Theorem	znval2 14645	Self-referential expression for the ℤ/nℤ structure. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ ≤ = (le‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 = (𝑈 sSet ⟨(le‘ndx), ≤ ⟩))
Theorem	znbaslemnn 14646	Lemma for znbas 14651. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ∈ ℕ    &   ⊢ (𝐸‘ndx) ≠ (le‘ndx)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐸‘𝑈) = (𝐸‘𝑌))
Theorem	znbas2 14647	The base set of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (Base‘𝑈) = (Base‘𝑌))
Theorem	znadd 14648	The additive structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (+g‘𝑈) = (+g‘𝑌))
Theorem	znmul 14649	The multiplicative structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (.r‘𝑈) = (.r‘𝑌))
Theorem	znzrh 14650	The ℤ ring homomorphism of ℤ/nℤ is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (ℤRHom‘𝑈) = (ℤRHom‘𝑌))
Theorem	znbas 14651	The base set of ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑅 = (ℤring ~QG (𝑆‘{𝑁}))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (ℤ / 𝑅) = (Base‘𝑌))
Theorem	zncrng 14652	ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing)
Theorem	znzrh2 14653*	The ℤ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ ∼ = (ℤring ~QG (𝑆‘{𝑁}))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐿 = (𝑥 ∈ ℤ ↦ [𝑥] ∼ ))
Theorem	znzrhval 14654	The ℤ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ ∼ = (ℤring ~QG (𝑆‘{𝑁}))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (𝐿‘𝐴) = [𝐴] ∼ )
Theorem	znzrhfo 14655	The ℤ ring homomorphism is a surjection onto ℤ/nℤ. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐿:ℤ–onto→𝐵)
Theorem	zndvds 14656	Express equality of equivalence classes in ℤ / 𝑛ℤ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐿‘𝐴) = (𝐿‘𝐵) ↔ 𝑁 ∥ (𝐴 − 𝐵)))
Theorem	zndvds0 14657	Special case of zndvds 14656 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = 0 ↔ 𝑁 ∥ 𝐴))
Theorem	znf1o 14658	The function 𝐹 enumerates all equivalence classes in ℤ/nℤ for each 𝑛. When 𝑛 = 0, ℤ / 0ℤ = ℤ / {0} ≈ ℤ so we let 𝑊 = ℤ; otherwise 𝑊 = {0, ..., 𝑛 − 1} enumerates all the equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑊–1-1-onto→𝐵)
Theorem	znle2 14659	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹))
Theorem	znleval 14660	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ 𝑋 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴 ≤ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))))
Theorem	znleval2 14661	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ 𝑋 = (Base‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≤ 𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))
Theorem	znfi 14662	The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
Theorem	znhash 14663	The ℤ/nℤ structure has 𝑛 elements. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → (♯‘𝐵) = 𝑁)
Theorem	znidom 14664	The ℤ/nℤ structure is an integral domain when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Jim Kingdon, 13-Aug-2025.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℙ → 𝑌 ∈ IDomn)
Theorem	znidomb 14665	The ℤ/nℤ structure is a domain precisely when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑌 ∈ IDomn ↔ 𝑁 ∈ ℙ))
Theorem	znunit 14666	The units of ℤ/nℤ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑌)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐴 gcd 𝑁) = 1))
Theorem	znrrg 14667	The regular elements of ℤ/nℤ are exactly the units. (This theorem fails for 𝑁 = 0, where all nonzero integers are regular, but only ±1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑌)    &   ⊢ 𝐸 = (RLReg‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐸 = 𝑈)
PART 8  BASIC LINEAR ALGEBRA According to Wikipedia ("Linear algebra", 03-Mar-2019, https://en.wikipedia.org/wiki/Linear_algebra) "Linear algebra is the branch of mathematics concerning linear equations [...], linear functions [...] and their representations through matrices and vector spaces." Or according to the Merriam-Webster dictionary ("linear algebra", 12-Mar-2019, https://www.merriam-webster.com/dictionary/linear%20algebra) "Definition of linear algebra: a branch of mathematics that is concerned with mathematical structures closed under the operations of addition and scalar multiplication and that includes the theory of systems of linear equations, matrices, determinants, vector spaces, and linear transformations." Dealing with modules (over rings) instead of vector spaces (over fields) allows for a more unified approach. Therefore, linear equations, matrices, determinants, are usually regarded as "over a ring" in this part. Unless otherwise stated, the rings of scalars need not be commutative (see df-cring 14005), but the existence of a unity element is always assumed (our rings are unital, see df-ring 14004). For readers knowing vector spaces but unfamiliar with modules: the elements of a module are still called "vectors" and they still form a group under addition, with a zero vector as neutral element, like in a vector space. Like in a vector space, vectors can be multiplied by scalars, with the usual rules, the only difference being that the scalars are only required to form a ring, and not necessarily a field or a division ring. Note that any vector space is a (special kind of) module, so any theorem proved below for modules applies to any vector space.
8.1  Abstract multivariate polynomials
8.1.1  Definition and basic properties
Syntax	cmps 14668	Multivariate power series.
class mPwSer
Syntax	cmpl 14669	Multivariate polynomials.
class mPoly
Definition	df-psr 14670*	Define the algebra of power series over the index set 𝑖 and with coefficients from the ring 𝑟. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))
Definition	df-mplcoe 14671*	Define the subalgebra of the power series algebra generated by the variables; this is the polynomial algebra (the set of power series with finite degree). The index set (which has an element for each variable) is 𝑖, the coefficients are in ring 𝑟, and for each variable there is a "degree" such that the coefficient is zero for a term where the powers are all greater than those degrees. (Degree is in quotes because there is no guarantee that coefficients below that degree are nonzero, as we do not assume decidable equality for 𝑟). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 7-Oct-2025.)
⊢ mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}))
Theorem	reldmpsr 14672	The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ Rel dom mPwSer
Theorem	psrval 14673*	Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (TopOpen‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐵 = (𝐾 ↑𝑚 𝐷))    &   ⊢ ✚ = ( ∘𝑓 + ↾ (𝐵 × 𝐵))    &   ⊢ × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))    &   ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))    &   ⊢ (𝜑 → 𝐽 = (∏t‘(𝐷 × {𝑂})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑆 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
Theorem	fnpsr 14674	The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
⊢ mPwSer Fn (V × V)
Theorem	psrvalstrd 14675	The multivariate power series structure is a function. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → + ∈ 𝑌)    &   ⊢ (𝜑 → × ∈ 𝑍)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑃)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑄)    ⇒   ⊢ (𝜑 → ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(TopSet‘ndx), 𝐽⟩}) Struct ⟨1, 9⟩)
Theorem	psrbag 14676*	Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈ Fin)))
Theorem	psrbagf 14677*	A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ0)
Theorem	fczpsrbag 14678*	The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷)
Theorem	psrbaglesuppg 14679*	The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟 ≤ 𝐹)) → (◡𝐺 “ ℕ) ⊆ (◡𝐹 “ ℕ))
Theorem	psrbagfi 14680*	A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ Fin → 𝐷 = (ℕ0 ↑𝑚 𝐼))
Theorem	psrbasg 14681*	The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 8-Jul-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐾 ↑𝑚 𝐷))
Theorem	psrelbas 14682*	An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐷⟶𝐾)
Theorem	psrelbasfi 14683	Simpler form of psrelbas 14682 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:(ℕ0 ↑𝑚 𝐼)⟶𝐾)
Theorem	psrelbasfun 14684	An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑋 ∈ 𝐵 → Fun 𝑋)
Theorem	psrplusgg 14685	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑆)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ✚ = ( ∘𝑓 + ↾ (𝐵 × 𝐵)))
Theorem	psradd 14686	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ✚ 𝑌) = (𝑋 ∘𝑓 + 𝑌))
Theorem	psraddcl 14687	Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) Generalize to magmas. (Revised by SN, 12-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Mgm)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	psr0cl 14688*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐵)
Theorem	psr0lid 14689*	The zero element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐷 × { 0 }) + 𝑋) = 𝑋)
Theorem	psrnegcl 14690*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁 ∘ 𝑋) ∈ 𝐵)
Theorem	psrlinv 14691*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑁 ∘ 𝑋) + 𝑋) = (𝐷 × { 0 }))
Theorem	psrgrp 14692	The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by SN, 7-Feb-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑆 ∈ Grp)
Theorem	psr0 14693*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (𝜑 → 0 = (𝐷 × {𝑂}))
Theorem	psrneg 14694*	The negative function of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑀 = (invg‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) = (𝑁 ∘ 𝑋))
Theorem	psr1clfi 14695*	The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐵)
Theorem	reldmmpl 14696	The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ Rel dom mPoly
Theorem	mplvalcoe 14697*	Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = {𝑓 ∈ 𝐵 ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝐼)∀𝑏 ∈ (ℕ0 ↑𝑚 𝐼)(∀𝑘 ∈ 𝐼 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = 0 )}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑃 = (𝑆 ↾s 𝑈))
Theorem	mplbascoe 14698*	Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑈 = {𝑓 ∈ 𝐵 ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝐼)∀𝑏 ∈ (ℕ0 ↑𝑚 𝐼)(∀𝑘 ∈ 𝐼 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = 0 )})
Theorem	mplelbascoe 14699*	Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝐼)∀𝑏 ∈ (ℕ0 ↑𝑚 𝐼)(∀𝑘 ∈ 𝐼 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑋‘𝑏) = 0 ))))
Theorem	fnmpl 14700	mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.)
⊢ mPoly Fn (V × V)