P. 214 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21301-21400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2idlval 21301	Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐽 = (LIdeal‘𝑂)    &   ⊢ 𝑇 = (2Ideal‘𝑅)    ⇒   ⊢ 𝑇 = (𝐼 ∩ 𝐽)
Theorem	isridl 21302*	A right ideal is a left ideal of the opposite ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑈 ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 (𝑦 · 𝑥) ∈ 𝐼)))
Theorem	2idlelb 21303	Membership in a two-sided ideal. Formerly part of proof for 2idlcpbl 21322. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐽 = (LIdeal‘𝑂)    &   ⊢ 𝑇 = (2Ideal‘𝑅)    ⇒   ⊢ (𝑈 ∈ 𝑇 ↔ (𝑈 ∈ 𝐼 ∧ 𝑈 ∈ 𝐽))
Theorem	2idllidld 21304	A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
Theorem	2idlridld 21305	A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑂))
Theorem	df2idl2rng 21306*	Alternate (the usual textbook) definition of a two-sided ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
⊢ 𝑈 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝐼 ∈ (SubGrp‘𝑅)) → (𝐼 ∈ 𝑈 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 ((𝑥 · 𝑦) ∈ 𝐼 ∧ (𝑦 · 𝑥) ∈ 𝐼)))
Theorem	df2idl2 21307*	Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
⊢ 𝑈 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑈 ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 ((𝑥 · 𝑦) ∈ 𝐼 ∧ (𝑦 · 𝑥) ∈ 𝐼))))
Theorem	ridl0 21308	Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	ridl1 21309	Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	2idl0 21310	Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝐼)
Theorem	2idl1 21311	Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝐼)
Theorem	2idlss 21312	A two-sided ideal is a subset of the base set. Formerly part of proof for 2idlcpbl 21322. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened by AV, 13-Mar-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (2Ideal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵)
Theorem	2idlbas 21313	The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 𝐵 = (Base‘𝐽)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐼)
Theorem	2idlelbas 21314	The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 𝐵 = (Base‘𝐽)    ⇒   ⊢ (𝜑 → (𝐵 ∈ (LIdeal‘𝑅) ∧ 𝐵 ∈ (LIdeal‘(oppr‘𝑅))))
Theorem	rng2idlsubrng 21315	A two-sided ideal of a non-unital ring which is a non-unital ring is a subring of the ring. (Contributed by AV, 20-Feb-2025.) (Revised by AV, 11-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (SubRng‘𝑅))
Theorem	rng2idlnsg 21316	A two-sided ideal of a non-unital ring which is a non-unital ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))
Theorem	rng2idl0 21317	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a non-unital ring. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng)    ⇒   ⊢ (𝜑 → (0g‘𝑅) ∈ 𝐼)
Theorem	rng2idlsubgsubrng 21318	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a subring of the ring. (Contributed by AV, 11-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅))    ⇒   ⊢ (𝜑 → 𝐼 ∈ (SubRng‘𝑅))
Theorem	rng2idlsubgnsg 21319	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅))    ⇒   ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))
Theorem	rng2idlsubg0 21320	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅))    ⇒   ⊢ (𝜑 → (0g‘𝑅) ∈ 𝐼)
Theorem	2idlcpblrng 21321	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝐸 = (𝑅 ~QG 𝑆)    &   ⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ (SubGrp‘𝑅)) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))
Theorem	2idlcpbl 21322	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝐸 = (𝑅 ~QG 𝑆)    &   ⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))
Theorem	qus2idrng 21323	The quotient of a non-unital ring modulo a two-sided ideal, which is a subgroup of the additive group of the non-unital ring, is a non-unital ring (qusring 21325 analog). (Contributed by AV, 23-Feb-2025.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (2Ideal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ (SubGrp‘𝑅)) → 𝑈 ∈ Rng)
Theorem	qus1 21324	The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → (𝑈 ∈ Ring ∧ [ 1 ](𝑅 ~QG 𝑆) = (1r‘𝑈)))
Theorem	qusring 21325	If 𝑆 is a two-sided ideal in 𝑅, then 𝑈 = 𝑅 / 𝑆 is a ring, called the quotient ring of 𝑅 by 𝑆. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (2Ideal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ Ring)
Theorem	qusrhm 21326*	If 𝑆 is a two-sided ideal in 𝑅, then the "natural map" from elements to their cosets is a ring homomorphism from 𝑅 to 𝑅 / 𝑆. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝑅 ~QG 𝑆))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑈))
Theorem	rhmpreimaidl 21327	The preimage of an ideal by a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.)
⊢ 𝐼 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (◡𝐹 “ 𝐽) ∈ 𝐼)
Theorem	kerlidl 21328	The kernel of a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (◡𝐹 “ { 0 }) ∈ 𝐼)
Theorem	qusmul2idl 21329	Value of the ring operation in a quotient ring by a two-sided ideal. (Contributed by Thierry Arnoux, 1-Sep-2024.)
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ([𝑋](𝑅 ~QG 𝐼) × [𝑌](𝑅 ~QG 𝐼)) = [(𝑋 · 𝑌)](𝑅 ~QG 𝐼))
Theorem	crngridl 21330	In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐼 = (LIdeal‘𝑂))
Theorem	crng2idl 21331	In a commutative ring, a two-sided ideal is the same as a left ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐼 = (2Ideal‘𝑅))
Theorem	qusmulrng 21332	Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 21333. Similar to qusmul2idl 21329. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.)
⊢ ∼ = (𝑅 ~QG 𝑆)    &   ⊢ 𝐻 = (𝑅 /s ∼ )    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝐻)    ⇒   ⊢ (((𝑅 ∈ Rng ∧ 𝑆 ∈ (2Ideal‘𝑅) ∧ 𝑆 ∈ (SubGrp‘𝑅)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	quscrng 21333	The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) (Proof shortened by AV, 3-Apr-2025.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ CRing)
Theorem	qusmulcrng 21334	Value of the ring operation in a quotient ring of a commutative ring. (Contributed by Thierry Arnoux, 1-Sep-2024.) (Proof shortened by metakunt, 3-Jun-2025.)
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ([𝑋](𝑅 ~QG 𝐼) × [𝑌](𝑅 ~QG 𝐼)) = [(𝑋 · 𝑌)](𝑅 ~QG 𝐼))
Theorem	rhmqusnsg 21335*	The mapping 𝐽 induced by a ring homomorphism 𝐹 from a subring 𝑁 of the quotient group 𝑄 over 𝐹's kernel 𝐾 is a ring homomorphism. (Contributed by Thierry Arnoux, 13-May-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝐺 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ⊆ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ (LIdeal‘𝐺))    ⇒   ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐻))
10.7.3.1  Condition for a non-unital ring to be unital In MathOverflow, the following theorem is claimed: "Theorem 1. Let A be a rng (= nonunital associative ring). Let J be a (two-sided) ideal of A. Assume that both rngs J and A/J are unital. Then, the rng A is also unital.", see https://mathoverflow.net/questions/487676 (/unitality-of-rngs-is-inherited-by-extensions). This thread also contains some hints to literature: Clifford and Preston's book "The Algebraic Theory of Semigroups"(Chapter 5 on representation theory), and Okninski's book Semigroup Algebras, Corollary 8 in Chapter 4. In the following, this theorem is proven formally, see rngringbdlem2 21357 (and variants rngringbd 21358 and ring2idlqusb 21360). This theorem is not trivial, since it is possible for a subset of a ring, especially a subring of a non-unital ring or (left/two-sided) ideal, to be a unital ring with a different ring unity. See also the comment for df-subrg 20599. In the given case, however, the ring unity of the larger ring can be determined by the ring unity of the two-sided ideal and a representative of the ring unity of the corresponding quotient, see ring2idlqus1 21369. An example for such a construction is given in pzriprng1ALT 21528, for the case mentioned in the comment for df-subrg 20599.
Theorem	rngqiprng1elbas 21336	The ring unity of a two-sided ideal of a non-unital ring belongs to the base set of the ring. (Contributed by AV, 15-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ (𝜑 → 1 ∈ 𝐵)
Theorem	rngqiprngghmlem1 21337	Lemma 1 for rngqiprngghm 21349. (Contributed by AV, 25-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ( 1 · 𝐴) ∈ (Base‘𝐽))
Theorem	rngqiprngghmlem2 21338	Lemma 2 for rngqiprngghm 21349. (Contributed by AV, 25-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → (( 1 · 𝐴)(+g‘𝐽)( 1 · 𝐶)) ∈ (Base‘𝐽))
Theorem	rngqiprngghmlem3 21339	Lemma 3 for rngqiprngghm 21349. (Contributed by AV, 25-Feb-2025.) (Proof shortened by AV, 24-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → ( 1 · (𝐴(+g‘𝑅)𝐶)) = (( 1 · 𝐴)(+g‘𝐽)( 1 · 𝐶)))
Theorem	rngqiprngimfolem 21340	Lemma for rngqiprngimfo 21351. (Contributed by AV, 5-Mar-2025.) (Proof shortened by AV, 24-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · ((𝐶(-g‘𝑅)( 1 · 𝐶))(+g‘𝑅)𝐴)) = 𝐴)
Theorem	rngqiprnglinlem1 21341	Lemma 1 for rngqiprnglin 21352. (Contributed by AV, 28-Feb-2025.) (Proof shortened by AV, 24-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → (( 1 · 𝐴) · ( 1 · 𝐶)) = ( 1 · (𝐴 · 𝐶)))
Theorem	rngqiprnglinlem2 21342	Lemma 2 for rngqiprnglin 21352. (Contributed by AV, 28-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → [(𝐴 · 𝐶)] ∼ = ([𝐴] ∼ (.r‘𝑄)[𝐶] ∼ ))
Theorem	rngqiprnglinlem3 21343	Lemma 3 for rngqiprnglin 21352. (Contributed by AV, 28-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → ([𝐴] ∼ (.r‘𝑄)[𝐶] ∼ ) ∈ (Base‘𝑄))
Theorem	rngqiprngimf1lem 21344	Lemma for rngqiprngimf1 21350. (Contributed by AV, 7-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → (([𝐴] ∼ = (0g‘𝑄) ∧ ( 1 · 𝐴) = (0g‘𝐽)) → 𝐴 = (0g‘𝑅)))
Theorem	rngqipbas 21345	The base set of the product of the quotient with a two-sided ideal and the two-sided ideal is the cartesian product of the base set of the quotient and the base set of the two-sided ideal. (Contributed by AV, 21-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    ⇒   ⊢ (𝜑 → (Base‘𝑃) = (𝐶 × 𝐼))
Theorem	rngqiprng 21346	The product of the quotient with a two-sided ideal and the two-sided ideal is a non-unital ring. (Contributed by AV, 23-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    ⇒   ⊢ (𝜑 → 𝑃 ∈ Rng)
Theorem	rngqiprngimf 21347*	𝐹 is a function from (the base set of) a non-unital ring to the product of the (base set 𝐶 of the) quotient with a two-sided ideal and the (base set 𝐼 of the) two-sided ideal (because of 2idlbas 21313, (Base‘𝐽) = 𝐼!) (Contributed by AV, 21-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐹:𝐵⟶(𝐶 × 𝐼))
Theorem	rngqiprngimfv 21348*	The value of the function 𝐹 at an element of (the base set of) a non-unital ring. (Contributed by AV, 24-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → (𝐹‘𝐴) = ⟨[𝐴] ∼ , ( 1 · 𝐴)⟩)
Theorem	rngqiprngghm 21349*	𝐹 is a homomorphism of the additive groups of non-unital rings. (Contributed by AV, 24-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑃))
Theorem	rngqiprngimf1 21350*	𝐹 is a one-to-one function from (the base set of) a non-unital ring to the product of the (base set of the) quotient with a two-sided ideal and the (base set of the) two-sided ideal. (Contributed by AV, 7-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐹:𝐵–1-1→(𝐶 × 𝐼))
Theorem	rngqiprngimfo 21351*	𝐹 is a function from (the base set of) a non-unital ring onto the product of the (base set of the) quotient with a two-sided ideal and the (base set of the) two-sided ideal. (Contributed by AV, 5-Mar-2025.) (Proof shortened by AV, 24-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐹:𝐵–onto→(𝐶 × 𝐼))
Theorem	rngqiprnglin 21352*	𝐹 is linear with respect to the multiplication. (Contributed by AV, 28-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ (𝜑 → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎 · 𝑏)) = ((𝐹‘𝑎)(.r‘𝑃)(𝐹‘𝑏)))
Theorem	rngqiprngho 21353*	𝐹 is a homomorphism of non-unital rings. (Contributed by AV, 21-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHom 𝑃))
Theorem	rngqiprngim 21354*	𝐹 is an isomorphism of non-unital rings. (Contributed by AV, 21-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngIso 𝑃))
Theorem	rng2idl1cntr 21355	The unity of a two-sided ideal of a non-unital ring is central, i.e., an element of the center of the multiplicative semigroup of the non-unital ring. This is part of the proof given in MathOverflow, which seems to be sufficient to show that 𝐹 given below (see rngqiprngimf 21347) is an isomorphism. In our proof, however we show that 𝐹 is linear regarding the multiplication (rngqiprnglin 21352) via rngqiprnglinlem1 21341 instead. (Contributed by AV, 13-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝜑 → 1 ∈ (Cntr‘𝑀))
Theorem	rngringbdlem1 21356	In a unital ring, the quotient of the ring and a two-sided ideal is unital. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ Ring) → 𝑄 ∈ Ring)
Theorem	rngringbdlem2 21357	A non-unital ring is unital if and only if there is a (two-sided) ideal of the ring which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 14-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    ⇒   ⊢ ((𝜑 ∧ 𝑄 ∈ Ring) → 𝑅 ∈ Ring)
Theorem	rngringbd 21358	A non-unital ring is unital if and only if there is a (two-sided) ideal of the ring which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    ⇒   ⊢ (𝜑 → (𝑅 ∈ Ring ↔ 𝑄 ∈ Ring))
Theorem	ring2idlqus 21359*	For every unital ring there is a (two-sided) ideal of the ring (in fact the base set of the ring itself) which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 13-Feb-2025.)
⊢ (𝑅 ∈ Ring → ∃𝑖 ∈ (2Ideal‘𝑅)((𝑅 ↾s 𝑖) ∈ Ring ∧ (𝑅 /s (𝑅 ~QG 𝑖)) ∈ Ring))
Theorem	ring2idlqusb 21360*	A non-unital ring is unital if and only if there is a (two-sided) ideal of the ring which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 20-Feb-2025.)
⊢ (𝑅 ∈ Rng → (𝑅 ∈ Ring ↔ ∃𝑖 ∈ (2Ideal‘𝑅)((𝑅 ↾s 𝑖) ∈ Ring ∧ (𝑅 /s (𝑅 ~QG 𝑖)) ∈ Ring)))
Theorem	rngqiprngfulem1 21361*	Lemma 1 for rngqiprngfu 21367 (and lemma for rngqiprngu 21368). (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 (1r‘𝑄) = [𝑥] ∼ )
Theorem	rngqiprngfulem2 21362	Lemma 2 for rngqiprngfu 21367 (and lemma for rngqiprngu 21368). (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝐵)
Theorem	rngqiprngfulem3 21363	Lemma 3 for rngqiprngfu 21367 (and lemma for rngqiprngu 21368). (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐵)
Theorem	rngqiprngfulem4 21364	Lemma 4 for rngqiprngfu 21367. (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    ⇒   ⊢ (𝜑 → [𝑈] ∼ = [𝐸] ∼ )
Theorem	rngqiprngfulem5 21365	Lemma 5 for rngqiprngfu 21367. (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    ⇒   ⊢ (𝜑 → ( 1 · 𝑈) = 1 )
Theorem	rngqipring1 21366	The ring unity of the product of the quotient with a two-sided ideal and the two-sided ideal, which both are rings. (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    ⇒   ⊢ (𝜑 → (1r‘𝑃) = ⟨[𝐸] ∼ , 1 ⟩)
Theorem	rngqiprngfu 21367*	The function value of 𝐹 at the constructed expected ring unity of 𝑅 is the ring unity of the product of the quotient with the two-sided ideal and the two-sided ideal. (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ (𝜑 → (𝐹‘𝑈) = ⟨[𝐸] ∼ , 1 ⟩)
Theorem	rngqiprngu 21368	If a non-unital ring has a (two-sided) ideal which is unital, and the quotient of the ring and the ideal is also unital, then the ring is also unital with a ring unity which can be constructed from the ring unity of the ideal and a representative of the ring unity of the quotient. (Contributed by AV, 17-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    ⇒   ⊢ (𝜑 → (1r‘𝑅) = 𝑈)
Theorem	ring2idlqus1 21369	If a non-unital ring has a (two-sided) ideal which is unital, and the quotient of the ring and the ideal is also unital, then the ring is also unital with a ring unity which can be constructed from the ring unity of the ideal and a representative of the ring unity of the quotient. (Contributed by AV, 17-Mar-2025.)
⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘(𝑅 ↾s 𝐼))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Rng ∧ 𝐼 ∈ (2Ideal‘𝑅)) ∧ ((𝑅 ↾s 𝐼) ∈ Ring ∧ (𝑅 /s (𝑅 ~QG 𝐼)) ∈ Ring) ∧ 𝑈 ∈ (1r‘(𝑅 /s (𝑅 ~QG 𝐼)))) → (𝑅 ∈ Ring ∧ (1r‘𝑅) = ((𝑈 − ( 1 · 𝑈)) + 1 )))
10.7.4  Principal ideal rings. Divisibility in the integers
Syntax	clpidl 21370	Ring left-principal-ideal function.
class LPIdeal
Syntax	clpir 21371	Class of left principal ideal rings.
class LPIR
Definition	df-lpidl 21372*	Define the class of left principal ideals of a ring, which are ideals with a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ LPIdeal = (𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})
Definition	df-lpir 21373	Define the class of left principal ideal rings, rings where every left ideal has a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ LPIR = {𝑤 ∈ Ring ∣ (LIdeal‘𝑤) = (LPIdeal‘𝑤)}
Theorem	lpival 21374*	Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})})
Theorem	islpidl 21375*	Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔})))
Theorem	lpi0 21376	The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃)
Theorem	lpi1 21377	The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃)
Theorem	islpir 21378	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃))
Theorem	lpiss 21379	Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈)
Theorem	islpir2 21380	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃))
Theorem	lpirring 21381	Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring)
Theorem	drnglpir 21382	Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR)
Theorem	rspsn 21383*	Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → (𝐾‘{𝐺}) = {𝑥 ∣ 𝐺 ∥ 𝑥})
Theorem	lidldvgen 21384*	An element generates an ideal iff it is contained in the ideal and all elements are right-divided by it. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵) → (𝐼 = (𝐾‘{𝐺}) ↔ (𝐺 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 𝐺 ∥ 𝑥)))
Theorem	lpigen 21385*	An ideal is principal iff it contains an element which right-divides all elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐼 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 𝑥 ∥ 𝑦))
10.7.5  Principal ideal domains
Syntax	cpid 21386	Class of principal ideal domains.
class PID
Definition	df-pid 21387	A principal ideal domain is an integral domain satisfying the left principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ PID = (IDomn ∩ LPIR)
10.8  The complex numbers as an algebraic extensible structure
10.8.1  Definition and basic properties
Syntax	cpsmet 21388	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 21389	Extend class notation with the class of all extended metric spaces.
class ∞Met
Syntax	cmet 21390	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 21391	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 21392	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 21393	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 21394	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 21395	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 21396*	Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
Definition	df-xmet 21397*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 21398, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
Definition	df-met 21398*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 24361. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. The 4 properties in Gleason's definition are shown by met0 24383, metgt0 24399, metsym 24390, and mettri 24392. (Contributed by NM, 25-Aug-2006.)
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
Definition	df-bl 21399*	Define the metric space ball function. See blval 24426 for its value. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))
Definition	df-mopn 21400	Define a function whose value is the family of open sets of a metric space. See elmopn 24482 for its main property. (Contributed by NM, 1-Sep-2006.)
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))