P. 213 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21201-21300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	qusmulcrng 21201	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 21202*	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 21224 (and variants rngringbd 21225 and ring2idlqusb 21227). 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 20486. 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 21236. An example for such a construction is given in pzriprng1ALT 21413, for the case mentioned in the comment for df-subrg 20486.
Theorem	rngqiprng1elbas 21203	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 21204	Lemma 1 for rngqiprngghm 21216. (Contributed by AV, 25-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ( 1 · 𝐴) ∈ (Base‘𝐽))
Theorem	rngqiprngghmlem2 21205	Lemma 2 for rngqiprngghm 21216. (Contributed by AV, 25-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → (( 1 · 𝐴)(+g‘𝐽)( 1 · 𝐶)) ∈ (Base‘𝐽))
Theorem	rngqiprngghmlem3 21206	Lemma 3 for rngqiprngghm 21216. (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 21207	Lemma for rngqiprngimfo 21218. (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 21208	Lemma 1 for rngqiprnglin 21219. (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 21209	Lemma 2 for rngqiprnglin 21219. (Contributed by AV, 28-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → [(𝐴 · 𝐶)] ∼ = ([𝐴] ∼ (.r‘𝑄)[𝐶] ∼ ))
Theorem	rngqiprnglinlem3 21210	Lemma 3 for rngqiprnglin 21219. (Contributed by AV, 28-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → ([𝐴] ∼ (.r‘𝑄)[𝐶] ∼ ) ∈ (Base‘𝑄))
Theorem	rngqiprngimf1lem 21211	Lemma for rngqiprngimf1 21217. (Contributed by AV, 7-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → (([𝐴] ∼ = (0g‘𝑄) ∧ ( 1 · 𝐴) = (0g‘𝐽)) → 𝐴 = (0g‘𝑅)))
Theorem	rngqipbas 21212	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 21213	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 21214*	𝐹 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 21180, (Base‘𝐽) = 𝐼!) (Contributed by AV, 21-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ 𝑃 = (𝑄 ×s 𝐽)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨[𝑥] ∼ , ( 1 · 𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐹:𝐵⟶(𝐶 × 𝐼))
Theorem	rngqiprngimfv 21215*	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 21216*	𝐹 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 21217*	𝐹 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 21218*	𝐹 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 21219*	𝐹 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 21220*	𝐹 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 21221*	𝐹 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 21222	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 21214) is an isomorphism. In our proof, however we show that 𝐹 is linear regarding the multiplication (rngqiprnglin 21219) via rngqiprnglinlem1 21208 instead. (Contributed by AV, 13-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝜑 → 1 ∈ (Cntr‘𝑀))
Theorem	rngringbdlem1 21223	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 21224	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 21225	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 21226*	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 21227*	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 21228*	Lemma 1 for rngqiprngfu 21234 (and lemma for rngqiprngu 21235). (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 (1r‘𝑄) = [𝑥] ∼ )
Theorem	rngqiprngfulem2 21229	Lemma 2 for rngqiprngfu 21234 (and lemma for rngqiprngu 21235). (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝐵)
Theorem	rngqiprngfulem3 21230	Lemma 3 for rngqiprngfu 21234 (and lemma for rngqiprngu 21235). (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐵)
Theorem	rngqiprngfulem4 21231	Lemma 4 for rngqiprngfu 21234. (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    ⇒   ⊢ (𝜑 → [𝑈] ∼ = [𝐸] ∼ )
Theorem	rngqiprngfulem5 21232	Lemma 5 for rngqiprngfu 21234. (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 21233	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 21234*	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 21235	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 21236	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 21237	Ring left-principal-ideal function.
class LPIdeal
Syntax	clpir 21238	Class of left principal ideal rings.
class LPIR
Definition	df-lpidl 21239*	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 21240	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 21241*	Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})})
Theorem	islpidl 21242*	Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔})))
Theorem	lpi0 21243	The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃)
Theorem	lpi1 21244	The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃)
Theorem	islpir 21245	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃))
Theorem	lpiss 21246	Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈)
Theorem	islpir2 21247	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃))
Theorem	lpirring 21248	Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring)
Theorem	drnglpir 21249	Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR)
Theorem	rspsn 21250*	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 21251*	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 21252*	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 21253	Class of principal ideal domains.
class PID
Definition	df-pid 21254	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 21255	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 21256	Extend class notation with the class of all extended metric spaces.
class ∞Met
Syntax	cmet 21257	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 21258	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 21259	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 21260	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 21261	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 21262	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 21263*	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 21264*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 21265, 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 21265*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 24216. 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 24238, metgt0 24254, metsym 24245, and mettri 24247. (Contributed by NM, 25-Aug-2006.)
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
Definition	df-bl 21266*	Define the metric space ball function. See blval 24281 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 21267	Define a function whose value is the family of open sets of a metric space. See elmopn 24337 for its main property. (Contributed by NM, 1-Sep-2006.)
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
Definition	df-fbas 21268*	Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
⊢ fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)})
Definition	df-fg 21269*	Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
Definition	df-metu 21270*	Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ metUnif = (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))))
Syntax	ccnfld 21271	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 21272*	The field of complex numbers. Other number fields and rings can be constructed by applying the ↾s restriction operator, for instance (ℂfld ↾ 𝔸) is the field of algebraic numbers. The contract of this set is defined entirely by cnfldex 21274, cnfldadd 21277, cnfldmul 21279, cnfldcj 21280, cnfldtset 21281, cnfldle 21282, cnfldds 21283, and cnfldbas 21275. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025.) (New usage is discouraged.)
⊢ ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
Theorem	cnfldstr 21273	The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21272. (Revised by GG, 31-Mar-2025.)
⊢ ℂfld Struct ⟨1, ;13⟩
Theorem	cnfldex 21274	The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Avoid complex number axioms and ax-pow 5323. (Revised by GG, 16-Mar-2025.)
⊢ ℂfld ∈ V
Theorem	cnfldbas 21275	The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21272. (Revised by GG, 31-Mar-2025.)
⊢ ℂ = (Base‘ℂfld)
Theorem	mpocnfldadd 21276*	The addition operation of the field of complex numbers. Version of cnfldadd 21277 using maps-to notation, which does not require ax-addf 11154. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) = (+g‘ℂfld)
Theorem	cnfldadd 21277	The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21272. (Revised by GG, 27-Apr-2025.)
⊢ + = (+g‘ℂfld)
Theorem	mpocnfldmul 21278*	The multiplication operation of the field of complex numbers. Version of cnfldmul 21279 using maps-to notation, which does not require ax-mulf 11155. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (.r‘ℂfld)
Theorem	cnfldmul 21279	The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21272. (Revised by GG, 27-Apr-2025.)
⊢ · = (.r‘ℂfld)
Theorem	cnfldcj 21280	The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21272. (Revised by GG, 31-Mar-2025.)
⊢ ∗ = (*𝑟‘ℂfld)
Theorem	cnfldtset 21281	The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21272. (Revised by GG, 31-Mar-2025.)
⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld)
Theorem	cnfldle 21282	The ordering of the field of complex numbers. Note that this is not actually an ordering on ℂ, but we put it in the structure anyway because restricting to ℝ does not affect this component, so that (ℂfld ↾s ℝ) is an ordered field even though ℂfld itself is not. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21272. (Revised by GG, 31-Mar-2025.)
⊢ ≤ = (le‘ℂfld)
Theorem	cnfldds 21283	The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21272. (Revised by GG, 31-Mar-2025.)
⊢ (abs ∘ − ) = (dist‘ℂfld)
Theorem	cnfldunif 21284	The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21272. (Revised by GG, 31-Mar-2025.)
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld)
Theorem	cnfldfun 21285	The field of complex numbers is a function. The proof is much shorter than the proof of cnfldfunALT 21286 by using cnfldstr 21273 and structn0fun 17128: in addition, it must be shown that ∅ ∉ ℂfld. (Contributed by AV, 18-Nov-2021.) Revise df-cnfld 21272. (Revised by GG, 31-Mar-2025.)
⊢ Fun ℂfld
Theorem	cnfldfunALT 21286	The field of complex numbers is a function. Alternate proof of cnfldfun 21285 not requiring that the index set of the components is ordered, but using quadratically many inequalities for the indices. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 11-Nov-2024.) Revise df-cnfld 21272. (Revised by GG, 31-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	dfcnfldOLD 21287	Obsolete version of df-cnfld 21272 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
Theorem	cnfldstrOLD 21288	Obsolete version of cnfldstr 21273 as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂfld Struct ⟨1, ;13⟩
Theorem	cnfldexOLD 21289	Obsolete version of cnfldex 21274 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂfld ∈ V
Theorem	cnfldbasOLD 21290	Obsolete version of cnfldbas 21275 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂ = (Base‘ℂfld)
Theorem	cnfldaddOLD 21291	Obsolete version of cnfldadd 21277 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ + = (+g‘ℂfld)
Theorem	cnfldmulOLD 21292	Obsolete version of cnfldmul 21279 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ · = (.r‘ℂfld)
Theorem	cnfldcjOLD 21293	Obsolete version of cnfldcj 21280 as of 27-Apr-2025. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∗ = (*𝑟‘ℂfld)
Theorem	cnfldtsetOLD 21294	Obsolete version of cnfldtset 21281 as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld)
Theorem	cnfldleOLD 21295	Obsolete version of cnfldle 21282 as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ≤ = (le‘ℂfld)
Theorem	cnflddsOLD 21296	Obsolete version of cnfldds 21283 as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (abs ∘ − ) = (dist‘ℂfld)
Theorem	cnfldunifOLD 21297	Obsolete version of cnfldunif 21284 as of 27-Apr-2025. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld)
Theorem	cnfldfunOLD 21298	Obsolete version of cnfldfun 21285 as of 27-Apr-2025. (Contributed by AV, 18-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	cnfldfunALTOLD 21299	Obsolete version of cnfldfunALT 21286 as of 27-Apr-2025. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 11-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	xrsstr 21300	The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 Struct ⟨1, ;12⟩