P. 217 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21601-21700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngqiprngimf1 21601*	𝐹 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 21602*	𝐹 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 21603*	𝐹 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 21604*	𝐹 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 21605*	𝐹 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 21606	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 21598) is an isomorphism. In our proof, however we show that 𝐹 is linear regarding the multiplication (rngqiprnglin 21603) via rngqiprnglinlem1 21592 instead. (Contributed by AV, 13-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝜑 → 1 ∈ (Cntr‘𝑀))
Theorem	rngringbdlem1 21607	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 21608	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 21609	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 21610*	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 21611*	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 21612*	Lemma 1 for rngqiprngfu 21618 (and lemma for rngqiprngu 21619). (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 (1r‘𝑄) = [𝑥] ∼ )
Theorem	rngqiprngfulem2 21613	Lemma 2 for rngqiprngfu 21618 (and lemma for rngqiprngu 21619). (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝐵)
Theorem	rngqiprngfulem3 21614	Lemma 3 for rngqiprngfu 21618 (and lemma for rngqiprngu 21619). (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐵)
Theorem	rngqiprngfulem4 21615	Lemma 4 for rngqiprngfu 21618. (Contributed by AV, 16-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ (𝜑 → 𝐽 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    &   ⊢ (𝜑 → 𝑄 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄))    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 )    ⇒   ⊢ (𝜑 → [𝑈] ∼ = [𝐸] ∼ )
Theorem	rngqiprngfulem5 21616	Lemma 5 for rngqiprngfu 21618. (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 21617	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 21618*	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 21619	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 21620	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.3.2  Prime Ideals
Syntax	cprmidl 21621	Extend class notation with the class of prime ideals.
class PrmIdeal
Definition	df-prmidl 21622*	Define the class of prime ideals of a ring 𝑅. A proper ideal 𝐼 of 𝑅 is prime if whenever 𝐴𝐵 ⊆ 𝐼 for ideals 𝐴 and 𝐵, either 𝐴 ⊆ 𝐼 or 𝐵 ⊆ 𝐼. The more familiar definition using elements rather than ideals is equivalent provided 𝑅 is commutative; see prmidl2 21627 and isprmidlc 21633. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.)
⊢ PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
Theorem	prmidlval 21623*	The class of prime ideals of a ring 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = {𝑖 ∈ (LIdeal‘𝑅) ∣ (𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
Theorem	isprmidl 21624*	The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃)))))
Theorem	prmidlnr 21625	A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ≠ 𝐵)
Theorem	prmidl 21626*	The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) ∧ ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐽 (𝑥 · 𝑦) ∈ 𝑃) → (𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃))
Theorem	prmidl2 21627*	A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 39097 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝑃 ∈ (LIdeal‘𝑅)) ∧ (𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))) → 𝑃 ∈ (PrmIdeal‘𝑅))
Theorem	idlmulssprm 21628	Let 𝑃 be a prime ideal containing the product (𝐼 × 𝐽) of two ideals 𝐼 and 𝐽. Then 𝐼 ⊆ 𝑃 or 𝐽 ⊆ 𝑃. (Contributed by Thierry Arnoux, 13-Apr-2024.)
⊢ × = (LSSum‘(mulGrp‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑃 ∈ (PrmIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → (𝐼 × 𝐽) ⊆ 𝑃)    ⇒   ⊢ (𝜑 → (𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃))
Theorem	pridln1 21629	A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ 1 ∈ 𝐼)
Theorem	prmidlidl 21630	A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.)
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ∈ (LIdeal‘𝑅))
Theorem	prmidlssidl 21631	Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) ⊆ (LIdeal‘𝑅))
Theorem	cringm4 21632	Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 · 𝑌) · (𝑍 · 𝑊)) = ((𝑋 · 𝑍) · (𝑌 · 𝑊)))
Theorem	isprmidlc 21633*	The predicate "is prime ideal" for commutative rings. Alternate definition for commutative rings. See definition in [Lang] p. 92. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))))
Theorem	prmidlc 21634	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 12-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ (𝐼 · 𝐽) ∈ 𝑃)) → (𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃))
Theorem	prmidlc2 21635	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by AV, 12-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (𝐵 ∖ 𝑃) ∧ 𝐽 ∈ 𝐵 ∧ (𝐼 · 𝐽) ∈ 𝑃)) → 𝐽 ∈ 𝑃)
Theorem	cmprmidlmcl 21636	The complement of a prime ideal is multiplicatively closed. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by AV, 12-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (𝐵 ∖ 𝑃) ∧ 𝐽 ∈ (𝐵 ∖ 𝑃))) → (𝐼 · 𝐽) ∈ (𝐵 ∖ 𝑃))
Theorem	prmidlprop 21637	Property of prime ideals. (Contributed by Thierry Arnoux, 6-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑃 ∈ (PrmIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑃 ∨ 𝑌 ∈ 𝑃))
Theorem	0ringprmidl 21638	The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (PrmIdeal‘𝑅) = ∅)
Theorem	prmidl0 21639	The zero ideal of a commutative ring 𝑅 is a prime ideal if and only if 𝑅 is an integral domain. (Contributed by Thierry Arnoux, 30-Jun-2024.)
⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ { 0 } ∈ (PrmIdeal‘𝑅)) ↔ 𝑅 ∈ IDomn)
Theorem	rhmpreimaprmidl 21640	The preimage of a prime ideal by a ring homomorphism is a prime ideal. (Contributed by Thierry Arnoux, 29-Jun-2024.)
⊢ 𝑃 = (PrmIdeal‘𝑅)    ⇒   ⊢ (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝐽 ∈ (PrmIdeal‘𝑆)) → (◡𝐹 “ 𝐽) ∈ 𝑃)
Theorem	qsidomlem1 21641	If the quotient ring of a commutative ring relative to an ideal is an integral domain, that ideal must be prime. (Contributed by Thierry Arnoux, 16-Jan-2024.)
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → 𝐼 ∈ (PrmIdeal‘𝑅))
Theorem	qsidomlem2 21642	A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.)
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ IDomn)
Theorem	qsidom 21643	An ideal 𝐼 in the commutative ring 𝑅 is prime if and only if the factor ring 𝑄 is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.)
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝑄 ∈ IDomn ↔ 𝐼 ∈ (PrmIdeal‘𝑅)))
Theorem	qsnzr 21644	A quotient of a nonzero ring by a proper ideal is a nonzero ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝑄 ∈ NzRing)
Theorem	ssdifidllem 21645*	Lemma for ssdifidl 21646: The set 𝑃 used in the proof of ssdifidl 21646 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)    &   ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}    &   ⊢ (𝜑 → 𝑍 ⊆ 𝑃)    &   ⊢ (𝜑 → 𝑍 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝑍)    ⇒   ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃)
Theorem	ssdifidl 21646*	Let 𝑅 be a ring, and let 𝐼 be an ideal of 𝑅 disjoint with a set 𝑆. Then there exists an ideal 𝑖, maximal among the set 𝑃 of ideals containing 𝐼 and disjoint with 𝑆. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)    &   ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)
Theorem	ssdifidlprm 21647*	If the set 𝑆 of ssdifidl 21646 is multiplicatively closed, then the ideal 𝑖 is prime. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀))    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)    &   ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))
Theorem	prmidlsubm 21648	The complement of a prime ideal is multiplicatively closed. Converse of ssdifidlprm 21647. (Contributed by Thierry Arnoux, 6-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑃 ∈ (PrmIdeal‘𝑅))    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑃) ∈ (SubMnd‘(mulGrp‘𝑅)))
10.7.4  Principal ideal rings. Divisibility in the integers
Syntax	clpidl 21649	Ring left-principal-ideal function.
class LPIdeal
Syntax	clpir 21650	Class of left principal ideal rings.
class LPIR
Definition	df-lpidl 21651*	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 21652	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 21653*	Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})})
Theorem	islpidl 21654*	Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔})))
Theorem	lpi0 21655	The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃)
Theorem	lpi1 21656	The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃)
Theorem	islpir 21657	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃))
Theorem	lpiss 21658	Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈)
Theorem	islpir2 21659	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃))
Theorem	lpirring 21660	Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring)
Theorem	drnglpir 21661	Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR)
Theorem	rspsn 21662*	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 21663*	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 21664*	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 21665	Class of principal ideal domains.
class PID
Definition	df-pid 21666	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 21667	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 21668	Extend class notation with the class of all extended metric spaces.
class ∞Met
Syntax	cmet 21669	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 21670	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 21671	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 21672	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 21673	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 21674	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 21675*	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 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +e (𝑤𝑑𝑧)))})
Definition	df-xmet 21676*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 21677, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +e (𝑤𝑑𝑧)))})
Definition	df-met 21677*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 24645. 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 24667, metgt0 24683, metsym 24674, and mettri 24676. (Contributed by NM, 25-Aug-2006.)
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
Definition	df-bl 21678*	Define the metric space ball function. See blval 24710 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 21679	Define a function whose value is the family of open sets of a metric space. See elmopn 24766 for its main property. (Contributed by NM, 1-Sep-2006.)
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
Definition	df-fbas 21680*	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 21681*	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 21682*	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 21683	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 21684*	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 21686, cnfldadd 21689, cnfldmul 21691, cnfldcj 21692, cnfldtset 21693, cnfldle 21694, cnfldds 21695, and cnfldbas 21687. 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 21685	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 21684. (Revised by GG, 31-Mar-2025.)
⊢ ℂfld Struct ⟨1, ;13⟩
Theorem	cnfldex 21686	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 5326. (Revised by GG, 16-Mar-2025.)
⊢ ℂfld ∈ V
Theorem	cnfldbas 21687	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 21684. (Revised by GG, 31-Mar-2025.)
⊢ ℂ = (Base‘ℂfld)
Theorem	mpocnfldadd 21688*	The addition operation of the field of complex numbers. Version of cnfldadd 21689 using maps-to notation, which does not require ax-addf 11282. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) = (+g‘ℂfld)
Theorem	cnfldadd 21689	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 21684. (Revised by GG, 27-Apr-2025.)
⊢ + = (+g‘ℂfld)
Theorem	mpocnfldmul 21690*	The multiplication operation of the field of complex numbers. Version of cnfldmul 21691 using maps-to notation, which does not require ax-mulf 11283. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (.r‘ℂfld)
Theorem	cnfldmul 21691	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 21684. (Revised by GG, 27-Apr-2025.)
⊢ · = (.r‘ℂfld)
Theorem	cnfldcj 21692	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 21684. (Revised by GG, 31-Mar-2025.)
⊢ ∗ = (*𝑟‘ℂfld)
Theorem	cnfldtset 21693	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 21684. (Revised by GG, 31-Mar-2025.)
⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld)
Theorem	cnfldle 21694	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 21684. (Revised by GG, 31-Mar-2025.)
⊢ ≤ = (le‘ℂfld)
Theorem	cnfldds 21695	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 21684. (Revised by GG, 31-Mar-2025.)
⊢ (abs ∘ − ) = (dist‘ℂfld)
Theorem	cnfldunif 21696	The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21684. (Revised by GG, 31-Mar-2025.)
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld)
Theorem	cnfldfun 21697	The field of complex numbers is a function. The proof is much shorter than the proof of cnfldfunALT 21698 by using cnfldstr 21685 and structn0fun 17334: in addition, it must be shown that ∅ ∉ ℂfld. (Contributed by AV, 18-Nov-2021.) Revise df-cnfld 21684. (Revised by GG, 31-Mar-2025.)
⊢ Fun ℂfld
Theorem	cnfldfunALT 21698	The field of complex numbers is a function. Alternate proof of cnfldfun 21697 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 21684. (Revised by GG, 31-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	xrsstr 21699	The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 Struct ⟨1, ;12⟩
Theorem	xrsex 21700	The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 ∈ V