Home | Metamath
Proof Explorer Theorem List (p. 206 of 466) | < 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: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lidlacs 20501 | The ideal system is an algebraic closure system on the base set. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐼 = (LIdeal‘𝑊) ⇒ ⊢ (𝑊 ∈ Ring → 𝐼 ∈ (ACS‘𝐵)) | ||
Theorem | rspcl 20502 | The span of a set of ring elements is an ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ 𝑈) | ||
Theorem | rspssid 20503 | The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) | ||
Theorem | rsp1 20504 | The span of the identity element is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐾‘{ 1 }) = 𝐵) | ||
Theorem | rsp0 20505 | The span of the zero element is the zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐾‘{ 0 }) = { 0 }) | ||
Theorem | rspssp 20506 | The ideal span of a set of elements in a ring is contained in any subring which contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ⊆ 𝐼) → (𝐾‘𝐺) ⊆ 𝐼) | ||
Theorem | mrcrsp 20507 | Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐹 = (mrCls‘𝑈) ⇒ ⊢ (𝑅 ∈ Ring → 𝐾 = 𝐹) | ||
Theorem | lidlnz 20508* | A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃𝑥 ∈ 𝐼 𝑥 ≠ 0 ) | ||
Theorem | drngnidl 20509 | A division ring has only the two trivial ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 𝑈 = {{ 0 }, 𝐵}) | ||
Theorem | lidlrsppropd 20510* | The left ideals and ring span of a ring depend only on the ring components. Here 𝑊 is expected to be either 𝐵 (when closure is available) or V (when strong equality is available). (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → ((LIdeal‘𝐾) = (LIdeal‘𝐿) ∧ (RSpan‘𝐾) = (RSpan‘𝐿))) | ||
Syntax | c2idl 20511 | Ring two-sided ideal function. |
class 2Ideal | ||
Definition | df-2idl 20512 | Define the class of two-sided ideals of a ring. A two-sided ideal is a left ideal which is also a right ideal (or a left ideal over the opposite ring). (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr‘𝑟)))) | ||
Theorem | 2idlval 20513 | Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐽 = (LIdeal‘𝑂) & ⊢ 𝑇 = (2Ideal‘𝑅) ⇒ ⊢ 𝑇 = (𝐼 ∩ 𝐽) | ||
Theorem | 2idlcpbl 20514 | The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝐸 = (𝑅 ~QG 𝑆) & ⊢ 𝐼 = (2Ideal‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷))) | ||
Theorem | qus1 20515 | The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆)) & ⊢ 𝐼 = (2Ideal‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → (𝑈 ∈ Ring ∧ [ 1 ](𝑅 ~QG 𝑆) = (1r‘𝑈))) | ||
Theorem | qusring 20516 | If 𝑆 is a two-sided ideal in 𝑅, then 𝑈 = 𝑅 / 𝑆 is a ring, called the quotient ring of 𝑅 by 𝑆. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆)) & ⊢ 𝐼 = (2Ideal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ Ring) | ||
Theorem | qusrhm 20517* | If 𝑆 is a two-sided ideal in 𝑅, then the "natural map" from elements to their cosets is a ring homomorphism from 𝑅 to 𝑅 / 𝑆. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆)) & ⊢ 𝐼 = (2Ideal‘𝑅) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝑅 ~QG 𝑆)) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑈)) | ||
Theorem | crngridl 20518 | In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐼 = (LIdeal‘𝑂)) | ||
Theorem | crng2idl 20519 | In a commutative ring, a two-sided ideal is the same as a left ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐼 = (2Ideal‘𝑅)) | ||
Theorem | quscrng 20520 | The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆)) & ⊢ 𝐼 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ CRing) | ||
Syntax | clpidl 20521 | Ring left-principal-ideal function. |
class LPIdeal | ||
Syntax | clpir 20522 | Class of left principal ideal rings. |
class LPIR | ||
Definition | df-lpidl 20523* | 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 20524 | 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 20525* | Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})}) | ||
Theorem | islpidl 20526* | Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔}))) | ||
Theorem | lpi0 20527 | The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃) | ||
Theorem | lpi1 20528 | The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃) | ||
Theorem | islpir 20529 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃)) | ||
Theorem | lpiss 20530 | Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈) | ||
Theorem | islpir2 20531 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃)) | ||
Theorem | lpirring 20532 | Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring) | ||
Theorem | drnglpir 20533 | Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR) | ||
Theorem | rspsn 20534* | 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 20535* | 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 20536* | 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 | cnzr 20537 | The class of nonzero rings. |
class NzRing | ||
Definition | df-nzr 20538 | A nonzero or nontrivial ring is a ring with at least two values, or equivalently where 1 and 0 are different. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)} | ||
Theorem | isnzr 20539 | Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 ≠ 0 )) | ||
Theorem | nzrnz 20540 | One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 1 ≠ 0 ) | ||
Theorem | nzrring 20541 | A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) | ||
Theorem | drngnzr 20542 | All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) | ||
Theorem | isnzr2 20543 | Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 2o ≼ 𝐵)) | ||
Theorem | isnzr2hash 20544 | Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 20543. (Contributed by AV, 14-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 < (♯‘𝐵))) | ||
Theorem | opprnzr 20545 | The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑂 ∈ NzRing) | ||
Theorem | ringelnzr 20546 | A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 13-Jun-2015.) |
⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ∖ { 0 })) → 𝑅 ∈ NzRing) | ||
Theorem | nzrunit 20547 | A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ 0 ) | ||
Theorem | subrgnzr 20548 | A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ NzRing) | ||
Theorem | 0ringnnzr 20549 | A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019.) |
⊢ (𝑅 ∈ Ring → ((♯‘(Base‘𝑅)) = 1 ↔ ¬ 𝑅 ∈ NzRing)) | ||
Theorem | 0ring 20550 | If a ring has only one element, it is the zero ring. According to Wikipedia ("Zero ring", 14-Apr-2019, https://en.wikipedia.org/wiki/Zero_ring): "The zero ring, denoted {0} or simply 0, consists of the one-element set {0} with the operations + and * defined so that 0 + 0 = 0 and 0 * 0 = 0.". (Contributed by AV, 14-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 𝐵 = { 0 }) | ||
Theorem | 0ring01eq 20551 | In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 0 = 1 ) | ||
Theorem | 01eq0ring 20552 | If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 }) | ||
Theorem | 0ring01eqbi 20553 | In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by AV, 23-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐵 ≈ 1o ↔ 1 = 0 )) | ||
Theorem | rng1nnzr 20554 | The (smallest) structure representing a zero ring is not a nonzero ring. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉, 〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ⇒ ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ NzRing) | ||
Theorem | ring1zr 20555 | The only (unital) ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 7-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ∗ = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {〈〈𝑍, 𝑍〉, 𝑍〉} ∧ ∗ = {〈〈𝑍, 𝑍〉, 𝑍〉}))) | ||
Theorem | rngen1zr 20556 | The only (unital) ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ∗ = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 ≈ 1o ↔ ( + = {〈〈𝑍, 𝑍〉, 𝑍〉} ∧ ∗ = {〈〈𝑍, 𝑍〉, 𝑍〉}))) | ||
Theorem | ringen1zr 20557 | The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑍 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1o ↔ ( + = {〈〈𝑍, 𝑍〉, 𝑍〉} ∧ ∗ = {〈〈𝑍, 𝑍〉, 𝑍〉}))) | ||
Theorem | rng1nfld 20558 | The zero ring is not a field. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉, 〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ⇒ ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ Field) | ||
Syntax | crlreg 20559 | Set of left-regular elements in a ring. |
class RLReg | ||
Syntax | cdomn 20560 | Class of (ring theoretic) domains. |
class Domn | ||
Syntax | cidom 20561 | Class of integral domains. |
class IDomn | ||
Syntax | cpid 20562 | Class of principal ideal domains. |
class PID | ||
Definition | df-rlreg 20563* | Define the set of left-regular elements in a ring as those elements which are not left zero divisors, meaning that multiplying a nonzero element on the left by a left-regular element gives a nonzero product. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ RLReg = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))}) | ||
Definition | df-domn 20564* | A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))} | ||
Definition | df-idom 20565 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ IDomn = (CRing ∩ Domn) | ||
Definition | df-pid 20566 | 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) | ||
Theorem | rrgval 20567* | Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} | ||
Theorem | isrrg 20568* | Membership in the set of left-regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((𝑋 · 𝑦) = 0 → 𝑦 = 0 ))) | ||
Theorem | rrgeq0i 20569 | Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 )) | ||
Theorem | rrgeq0 20570 | Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 ↔ 𝑌 = 0 )) | ||
Theorem | rrgsupp 20571 | Left multiplication by a left regular element does not change the support set of a vector. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Revised by AV, 20-Jul-2019.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌:𝐼⟶𝐵) ⇒ ⊢ (𝜑 → (((𝐼 × {𝑋}) ∘f · 𝑌) supp 0 ) = (𝑌 supp 0 )) | ||
Theorem | rrgss 20572 | Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐸 ⊆ 𝐵 | ||
Theorem | unitrrg 20573 | Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸) | ||
Theorem | isdomn 20574* | Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) | ||
Theorem | domnnzr 20575 | A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | ||
Theorem | domnring 20576 | A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) | ||
Theorem | domneq0 20577 | In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 ))) | ||
Theorem | domnmuln0 20578 | In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝑋 · 𝑌) ≠ 0 ) | ||
Theorem | isdomn2 20579 | A ring is a domain iff all nonzero elements are nonzero-divisors. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) ⊆ 𝐸)) | ||
Theorem | domnrrg 20580 | In a domain, any nonzero element is a nonzero-divisor. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐸) | ||
Theorem | opprdomn 20581 | The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn → 𝑂 ∈ Domn) | ||
Theorem | abvn0b 20582 | Another characterization of domains, hinted at in abvtriv 20110: a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅)) | ||
Theorem | drngdomn 20583 | A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn) | ||
Theorem | isidom 20584 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | ||
Theorem | fldidom 20585 | A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof shortened by SN, 11-Nov-2024.) |
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn) | ||
Theorem | fldidomOLD 20586 | Obsolete version of fldidom 20585 as of 11-Nov-2024. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn) | ||
Theorem | fidomndrnglem 20587* | Lemma for fidomndrng 20588. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 })) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴)) ⇒ ⊢ (𝜑 → 𝐴 ∥ 1 ) | ||
Theorem | fidomndrng 20588 | A finite domain is a division ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ Domn ↔ 𝑅 ∈ DivRing)) | ||
Theorem | fiidomfld 20589 | A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ IDomn ↔ 𝑅 ∈ Field)) | ||
Syntax | cpsmet 20590 | Extend class notation with the class of all pseudometric spaces. |
class PsMet | ||
Syntax | cxmet 20591 | Extend class notation with the class of all extended metric spaces. |
class ∞Met | ||
Syntax | cmet 20592 | Extend class notation with the class of all metrics. |
class Met | ||
Syntax | cbl 20593 | Extend class notation with the metric space ball function. |
class ball | ||
Syntax | cfbas 20594 | Extend class definition to include the class of filter bases. |
class fBas | ||
Syntax | cfg 20595 | Extend class definition to include the filter generating function. |
class filGen | ||
Syntax | cmopn 20596 | Extend class notation with a function mapping each metric space to the family of its open sets. |
class MetOpen | ||
Syntax | cmetu 20597 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
class metUnif | ||
Definition | df-psmet 20598* | 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 20599* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 20600, 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 20600* | Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 23483. 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 23505, metgt0 23521, metsym 23512, and mettri 23514. (Contributed by NM, 25-Aug-2006.) |
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |