| Metamath
Proof Explorer Theorem List (p. 214 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rngqiprnglinlem1 21301 | Lemma 1 for rngqiprnglin 21312. (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 21302 | Lemma 2 for rngqiprnglin 21312. (Contributed by AV, 28-Feb-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ (𝜑 → 𝐽 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → [(𝐴 · 𝐶)] ∼ = ([𝐴] ∼ (.r‘𝑄)[𝐶] ∼ )) | ||
| Theorem | rngqiprnglinlem3 21303 | Lemma 3 for rngqiprnglin 21312. (Contributed by AV, 28-Feb-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ (𝜑 → 𝐽 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → ([𝐴] ∼ (.r‘𝑄)[𝐶] ∼ ) ∈ (Base‘𝑄)) | ||
| Theorem | rngqiprngimf1lem 21304 | Lemma for rngqiprngimf1 21310. (Contributed by AV, 7-Mar-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ (𝜑 → 𝐽 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → (([𝐴] ∼ = (0g‘𝑄) ∧ ( 1 · 𝐴) = (0g‘𝐽)) → 𝐴 = (0g‘𝑅))) | ||
| Theorem | rngqipbas 21305 | 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 21306 | 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 21307* | 𝐹 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 21273, (Base‘𝐽) = 𝐼!) (Contributed by AV, 21-Feb-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ (𝜑 → 𝐽 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ 𝑃 = (𝑄 ×s 𝐽) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈[𝑥] ∼ , ( 1 · 𝑥)〉) ⇒ ⊢ (𝜑 → 𝐹:𝐵⟶(𝐶 × 𝐼)) | ||
| Theorem | rngqiprngimfv 21308* | 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 21309* | 𝐹 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 21310* | 𝐹 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 21311* | 𝐹 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 21312* | 𝐹 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 21313* | 𝐹 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 21314* | 𝐹 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 21315 | 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 21307) is an isomorphism. In our proof, however we show that 𝐹 is linear regarding the multiplication (rngqiprnglin 21312) via rngqiprnglinlem1 21301 instead. (Contributed by AV, 13-Feb-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ (𝜑 → 𝐽 ∈ Ring) & ⊢ 1 = (1r‘𝐽) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝜑 → 1 ∈ (Cntr‘𝑀)) | ||
| Theorem | rngringbdlem1 21316 | 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 21317 | 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 21318 | 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 21319* | 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 21320* | 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 21321* | Lemma 1 for rngqiprngfu 21327 (and lemma for rngqiprngu 21328). (Contributed by AV, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ (𝜑 → 𝐽 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) & ⊢ (𝜑 → 𝑄 ∈ Ring) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 (1r‘𝑄) = [𝑥] ∼ ) | ||
| Theorem | rngqiprngfulem2 21322 | Lemma 2 for rngqiprngfu 21327 (and lemma for rngqiprngu 21328). (Contributed by AV, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ (𝜑 → 𝐽 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) & ⊢ (𝜑 → 𝑄 ∈ Ring) & ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄)) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝐵) | ||
| Theorem | rngqiprngfulem3 21323 | Lemma 3 for rngqiprngfu 21327 (and lemma for rngqiprngu 21328). (Contributed by AV, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ (𝜑 → 𝐽 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) & ⊢ (𝜑 → 𝑄 ∈ Ring) & ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄)) & ⊢ − = (-g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 ) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝐵) | ||
| Theorem | rngqiprngfulem4 21324 | Lemma 4 for rngqiprngfu 21327. (Contributed by AV, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ (𝜑 → 𝐽 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) & ⊢ (𝜑 → 𝑄 ∈ Ring) & ⊢ (𝜑 → 𝐸 ∈ (1r‘𝑄)) & ⊢ − = (-g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝑈 = ((𝐸 − ( 1 · 𝐸)) + 1 ) ⇒ ⊢ (𝜑 → [𝑈] ∼ = [𝐸] ∼ ) | ||
| Theorem | rngqiprngfulem5 21325 | Lemma 5 for rngqiprngfu 21327. (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 21326 | 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 21327* | 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 21328 | 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 21329 | 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 ))) | ||
| Syntax | clpidl 21330 | Ring left-principal-ideal function. |
| class LPIdeal | ||
| Syntax | clpir 21331 | Class of left principal ideal rings. |
| class LPIR | ||
| Definition | df-lpidl 21332* | 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 21333 | 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 21334* | Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
| ⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})}) | ||
| Theorem | islpidl 21335* | Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
| ⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔}))) | ||
| Theorem | lpi0 21336 | The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
| ⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃) | ||
| Theorem | lpi1 21337 | The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
| ⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃) | ||
| Theorem | islpir 21338 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
| ⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃)) | ||
| Theorem | lpiss 21339 | Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
| ⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈) | ||
| Theorem | islpir2 21340 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
| ⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃)) | ||
| Theorem | lpirring 21341 | Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring) | ||
| Theorem | drnglpir 21342 | Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
| ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR) | ||
| Theorem | rspsn 21343* | 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 21344* | 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 21345* | 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 ∧ 𝐼 ∈ 𝑈) → (𝐼 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 𝑥 ∥ 𝑦)) | ||
| Syntax | cpid 21346 | Class of principal ideal domains. |
| class PID | ||
| Definition | df-pid 21347 | 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) | ||
| Syntax | cpsmet 21348 | Extend class notation with the class of all pseudometric spaces. |
| class PsMet | ||
| Syntax | cxmet 21349 | Extend class notation with the class of all extended metric spaces. |
| class ∞Met | ||
| Syntax | cmet 21350 | Extend class notation with the class of all metrics. |
| class Met | ||
| Syntax | cbl 21351 | Extend class notation with the metric space ball function. |
| class ball | ||
| Syntax | cfbas 21352 | Extend class definition to include the class of filter bases. |
| class fBas | ||
| Syntax | cfg 21353 | Extend class definition to include the filter generating function. |
| class filGen | ||
| Syntax | cmopn 21354 | Extend class notation with a function mapping each metric space to the family of its open sets. |
| class MetOpen | ||
| Syntax | cmetu 21355 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
| class metUnif | ||
| Definition | df-psmet 21356* | 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 21357* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 21358, 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 21358* | Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 24331. 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 24353, metgt0 24369, metsym 24360, and mettri 24362. (Contributed by NM, 25-Aug-2006.) |
| ⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) | ||
| Definition | df-bl 21359* | Define the metric space ball function. See blval 24396 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 21360 | Define a function whose value is the family of open sets of a metric space. See elmopn 24452 for its main property. (Contributed by NM, 1-Sep-2006.) |
| ⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) | ||
| Definition | df-fbas 21361* | 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 21362* | 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 21363* | 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 21364 | Extend class notation with the field of complex numbers. |
| class ℂfld | ||
| Definition | df-cnfld 21365* |
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 21367, cnfldadd 21370, cnfldmul 21372, cnfldcj 21373, cnfldtset 21374, cnfldle 21375, cnfldds 21376, and cnfldbas 21368. 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 21366 | 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 21365. (Revised by GG, 31-Mar-2025.) |
| ⊢ ℂfld Struct 〈1, ;13〉 | ||
| Theorem | cnfldex 21367 | 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 5365. (Revised by GG, 16-Mar-2025.) |
| ⊢ ℂfld ∈ V | ||
| Theorem | cnfldbas 21368 | 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 21365. (Revised by GG, 31-Mar-2025.) |
| ⊢ ℂ = (Base‘ℂfld) | ||
| Theorem | mpocnfldadd 21369* | The addition operation of the field of complex numbers. Version of cnfldadd 21370 using maps-to notation, which does not require ax-addf 11234. (Contributed by GG, 31-Mar-2025.) |
| ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) = (+g‘ℂfld) | ||
| Theorem | cnfldadd 21370 | 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 21365. (Revised by GG, 27-Apr-2025.) |
| ⊢ + = (+g‘ℂfld) | ||
| Theorem | mpocnfldmul 21371* | The multiplication operation of the field of complex numbers. Version of cnfldmul 21372 using maps-to notation, which does not require ax-mulf 11235. (Contributed by GG, 31-Mar-2025.) |
| ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (.r‘ℂfld) | ||
| Theorem | cnfldmul 21372 | 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 21365. (Revised by GG, 27-Apr-2025.) |
| ⊢ · = (.r‘ℂfld) | ||
| Theorem | cnfldcj 21373 | 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 21365. (Revised by GG, 31-Mar-2025.) |
| ⊢ ∗ = (*𝑟‘ℂfld) | ||
| Theorem | cnfldtset 21374 | 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 21365. (Revised by GG, 31-Mar-2025.) |
| ⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld) | ||
| Theorem | cnfldle 21375 | 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 21365. (Revised by GG, 31-Mar-2025.) |
| ⊢ ≤ = (le‘ℂfld) | ||
| Theorem | cnfldds 21376 | 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 21365. (Revised by GG, 31-Mar-2025.) |
| ⊢ (abs ∘ − ) = (dist‘ℂfld) | ||
| Theorem | cnfldunif 21377 | The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21365. (Revised by GG, 31-Mar-2025.) |
| ⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld) | ||
| Theorem | cnfldfun 21378 | The field of complex numbers is a function. The proof is much shorter than the proof of cnfldfunALT 21379 by using cnfldstr 21366 and structn0fun 17188: in addition, it must be shown that ∅ ∉ ℂfld. (Contributed by AV, 18-Nov-2021.) Revise df-cnfld 21365. (Revised by GG, 31-Mar-2025.) |
| ⊢ Fun ℂfld | ||
| Theorem | cnfldfunALT 21379 | The field of complex numbers is a function. Alternate proof of cnfldfun 21378 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 21365. (Revised by GG, 31-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Fun ℂfld | ||
| Theorem | dfcnfldOLD 21380 | Obsolete version of df-cnfld 21365 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 21381 | Obsolete version of cnfldstr 21366 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 21382 | Obsolete version of cnfldex 21367 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 21383 | Obsolete version of cnfldbas 21368 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 21384 | Obsolete version of cnfldadd 21370 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 21385 | Obsolete version of cnfldmul 21372 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 21386 | Obsolete version of cnfldcj 21373 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 21387 | Obsolete version of cnfldtset 21374 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 21388 | Obsolete version of cnfldle 21375 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 21389 | Obsolete version of cnfldds 21376 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 21390 | Obsolete version of cnfldunif 21377 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 21391 | Obsolete version of cnfldfun 21378 as of 27-Apr-2025. (Contributed by AV, 18-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Fun ℂfld | ||
| Theorem | cnfldfunALTOLD 21392 | Obsolete version of cnfldfunALT 21379 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 | cnfldfunALTOLDOLD 21393 | Obsolete version of cnfldfunALTOLD 21392 as of 10-Nov-2024. The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Fun ℂfld | ||
| Theorem | xrsstr 21394 | The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ ℝ*𝑠 Struct 〈1, ;12〉 | ||
| Theorem | xrsex 21395 | The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ ℝ*𝑠 ∈ V | ||
| Theorem | xrsbas 21396 | The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ ℝ* = (Base‘ℝ*𝑠) | ||
| Theorem | xrsadd 21397 | The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ +𝑒 = (+g‘ℝ*𝑠) | ||
| Theorem | xrsmul 21398 | The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ ·e = (.r‘ℝ*𝑠) | ||
| Theorem | xrstset 21399 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠) | ||
| Theorem | xrsle 21400 | The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ ≤ = (le‘ℝ*𝑠) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |