![]() |
Metamath
Proof Explorer Theorem List (p. 201 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | qus1 20001 | 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 20002 | 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 20003* | 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 20004 | In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐼 = (LIdeal‘𝑂)) | ||
Theorem | crng2idl 20005 | 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 20006 | 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 20007 | Ring left-principal-ideal function. |
class LPIdeal | ||
Syntax | clpir 20008 | Class of left principal ideal rings. |
class LPIR | ||
Definition | df-lpidl 20009* | 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 20010 | 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 20011* | Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})}) | ||
Theorem | islpidl 20012* | Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔}))) | ||
Theorem | lpi0 20013 | The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃) | ||
Theorem | lpi1 20014 | The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃) | ||
Theorem | islpir 20015 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃)) | ||
Theorem | lpiss 20016 | Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈) | ||
Theorem | islpir2 20017 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃)) | ||
Theorem | lpirring 20018 | Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring) | ||
Theorem | drnglpir 20019 | Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR) | ||
Theorem | rspsn 20020* | 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 20021* | 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 20022* | 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 20023 | The class of nonzero rings. |
class NzRing | ||
Definition | df-nzr 20024 | 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 20025 | Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 ≠ 0 )) | ||
Theorem | nzrnz 20026 | 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 20027 | A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) | ||
Theorem | drngnzr 20028 | All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) | ||
Theorem | isnzr2 20029 | 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 20030 | Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 20029. (Contributed by AV, 14-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 < (♯‘𝐵))) | ||
Theorem | opprnzr 20031 | The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑂 ∈ NzRing) | ||
Theorem | ringelnzr 20032 | 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 20033 | A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ 0 ) | ||
Theorem | subrgnzr 20034 | A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ NzRing) | ||
Theorem | 0ringnnzr 20035 | 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 20036 | 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 20037 | 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 20038 | 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 20039 | 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 20040 | 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 20041 | 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 20042 | 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 20043 | 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 20044 | The zero ring is not a field. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉, 〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ⇒ ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ Field) | ||
Syntax | crlreg 20045 | Set of left-regular elements in a ring. |
class RLReg | ||
Syntax | cdomn 20046 | Class of (ring theoretic) domains. |
class Domn | ||
Syntax | cidom 20047 | Class of integral domains. |
class IDomn | ||
Syntax | cpid 20048 | Class of principal ideal domains. |
class PID | ||
Definition | df-rlreg 20049* | 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 20050* | 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 20051 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ IDomn = (CRing ∩ Domn) | ||
Definition | df-pid 20052 | 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 20053* | 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 20054* | 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 20055 | Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 )) | ||
Theorem | rrgeq0 20056 | 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 20057 | 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 20058 | Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐸 ⊆ 𝐵 | ||
Theorem | unitrrg 20059 | Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸) | ||
Theorem | isdomn 20060* | Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) | ||
Theorem | domnnzr 20061 | A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | ||
Theorem | domnring 20062 | A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) | ||
Theorem | domneq0 20063 | 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 20064 | 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 20065 | 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 20066 | 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 20067 | The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn → 𝑂 ∈ Domn) | ||
Theorem | abvn0b 20068 | Another characterization of domains, hinted at in abvtriv 19605: a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅)) | ||
Theorem | drngdomn 20069 | A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn) | ||
Theorem | isidom 20070 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | ||
Theorem | fldidom 20071 | A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn) | ||
Theorem | fidomndrnglem 20072* | Lemma for fidomndrng 20073. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 })) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴)) ⇒ ⊢ (𝜑 → 𝐴 ∥ 1 ) | ||
Theorem | fidomndrng 20073 | A finite domain is a division ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ Domn ↔ 𝑅 ∈ DivRing)) | ||
Theorem | fiidomfld 20074 | A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ IDomn ↔ 𝑅 ∈ Field)) | ||
Syntax | cpsmet 20075 | Extend class notation with the class of all pseudometric spaces. |
class PsMet | ||
Syntax | cxmet 20076 | Extend class notation with the class of all extended metric spaces. |
class ∞Met | ||
Syntax | cmet 20077 | Extend class notation with the class of all metrics. |
class Met | ||
Syntax | cbl 20078 | Extend class notation with the metric space ball function. |
class ball | ||
Syntax | cfbas 20079 | Extend class definition to include the class of filter bases. |
class fBas | ||
Syntax | cfg 20080 | Extend class definition to include the filter generating function. |
class filGen | ||
Syntax | cmopn 20081 | Extend class notation with a function mapping each metric space to the family of its open sets. |
class MetOpen | ||
Syntax | cmetu 20082 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
class metUnif | ||
Definition | df-psmet 20083* | 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 20084* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 20085, 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 20085* | Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 22928. 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 22950, metgt0 22966, metsym 22957, and mettri 22959. (Contributed by NM, 25-Aug-2006.) |
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) | ||
Definition | df-bl 20086* | Define the metric space ball function. See blval 22993 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 20087 | Define a function whose value is the family of open sets of a metric space. See elmopn 23049 for its main property. (Contributed by NM, 1-Sep-2006.) |
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) | ||
Definition | df-fbas 20088* | 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 20089* | 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 20090* | 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 20091 | Extend class notation with the field of complex numbers. |
class ℂfld | ||
Definition | df-cnfld 20092 |
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 20094, cnfldadd 20096, cnfldmul 20097, cnfldcj 20098, cnfldtset 20099, cnfldle 20100, cnfldds 20101, and cnfldbas 20095. 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.) (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 20093 | The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ ℂfld Struct 〈1, ;13〉 | ||
Theorem | cnfldex 20094 | 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.) |
⊢ ℂfld ∈ V | ||
Theorem | cnfldbas 20095 | 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.) |
⊢ ℂ = (Base‘ℂfld) | ||
Theorem | cnfldadd 20096 | 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.) |
⊢ + = (+g‘ℂfld) | ||
Theorem | cnfldmul 20097 | 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.) |
⊢ · = (.r‘ℂfld) | ||
Theorem | cnfldcj 20098 | 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.) |
⊢ ∗ = (*𝑟‘ℂfld) | ||
Theorem | cnfldtset 20099 | 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.) |
⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld) | ||
Theorem | cnfldle 20100 | 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.) |
⊢ ≤ = (le‘ℂfld) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |