![]() |
Metamath
Proof Explorer Theorem List (p. 209 of 475) | < 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-30034) |
![]() (30035-31557) |
![]() (31558-47500) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lidlrsppropd 20801* | 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 20802 | Ring two-sided ideal function. |
class 2Ideal | ||
Definition | df-2idl 20803 | 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 20804 | Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐽 = (LIdeal‘𝑂) & ⊢ 𝑇 = (2Ideal‘𝑅) ⇒ ⊢ 𝑇 = (𝐼 ∩ 𝐽) | ||
Theorem | 2idllidld 20805 | A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) ⇒ ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) | ||
Theorem | 2idlridld 20806 | A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑂)) | ||
Theorem | 2idlcpbl 20807 | 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 20808 | 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 20809 | 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 20810* | 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 | qusmul2 20811 | Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.) |
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ([𝑋](𝑅 ~QG 𝐼) × [𝑌](𝑅 ~QG 𝐼)) = [(𝑋 · 𝑌)](𝑅 ~QG 𝐼)) | ||
Theorem | crngridl 20812 | In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐼 = (LIdeal‘𝑂)) | ||
Theorem | crng2idl 20813 | 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 20814 | 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 20815 | Ring left-principal-ideal function. |
class LPIdeal | ||
Syntax | clpir 20816 | Class of left principal ideal rings. |
class LPIR | ||
Definition | df-lpidl 20817* | 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 20818 | 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 20819* | Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})}) | ||
Theorem | islpidl 20820* | Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔}))) | ||
Theorem | lpi0 20821 | The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃) | ||
Theorem | lpi1 20822 | The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃) | ||
Theorem | islpir 20823 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃)) | ||
Theorem | lpiss 20824 | Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈) | ||
Theorem | islpir2 20825 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃)) | ||
Theorem | lpirring 20826 | Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring) | ||
Theorem | drnglpir 20827 | Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR) | ||
Theorem | rspsn 20828* | 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 20829* | 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 20830* | 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 | crlreg 20831 | Set of left-regular elements in a ring. |
class RLReg | ||
Syntax | cdomn 20832 | Class of (ring theoretic) domains. |
class Domn | ||
Syntax | cidom 20833 | Class of integral domains. |
class IDomn | ||
Syntax | cpid 20834 | Class of principal ideal domains. |
class PID | ||
Definition | df-rlreg 20835* | 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 20836* | 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 20837 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ IDomn = (CRing ∩ Domn) | ||
Definition | df-pid 20838 | 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 20839* | 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 20840* | 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 20841 | Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 )) | ||
Theorem | rrgeq0 20842 | 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 20843 | 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 20844 | Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐸 ⊆ 𝐵 | ||
Theorem | unitrrg 20845 | Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸) | ||
Theorem | isdomn 20846* | Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) | ||
Theorem | domnnzr 20847 | A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | ||
Theorem | domnring 20848 | A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) | ||
Theorem | domneq0 20849 | 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 20850 | 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 20851 | 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 20852 | 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 20853 | The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn → 𝑂 ∈ Domn) | ||
Theorem | abvn0b 20854 | Another characterization of domains, hinted at in abvtriv 20398: a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅)) | ||
Theorem | drngdomn 20855 | A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn) | ||
Theorem | isidom 20856 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | ||
Theorem | fldidom 20857 | A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof shortened by SN, 11-Nov-2024.) |
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn) | ||
Theorem | fldidomOLD 20858 | Obsolete version of fldidom 20857 as of 11-Nov-2024. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn) | ||
Theorem | fidomndrnglem 20859* | Lemma for fidomndrng 20860. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 })) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴)) ⇒ ⊢ (𝜑 → 𝐴 ∥ 1 ) | ||
Theorem | fidomndrng 20860 | A finite domain is a division ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ Domn ↔ 𝑅 ∈ DivRing)) | ||
Theorem | fiidomfld 20861 | A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ IDomn ↔ 𝑅 ∈ Field)) | ||
Syntax | cpsmet 20862 | Extend class notation with the class of all pseudometric spaces. |
class PsMet | ||
Syntax | cxmet 20863 | Extend class notation with the class of all extended metric spaces. |
class ∞Met | ||
Syntax | cmet 20864 | Extend class notation with the class of all metrics. |
class Met | ||
Syntax | cbl 20865 | Extend class notation with the metric space ball function. |
class ball | ||
Syntax | cfbas 20866 | Extend class definition to include the class of filter bases. |
class fBas | ||
Syntax | cfg 20867 | Extend class definition to include the filter generating function. |
class filGen | ||
Syntax | cmopn 20868 | Extend class notation with a function mapping each metric space to the family of its open sets. |
class MetOpen | ||
Syntax | cmetu 20869 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
class metUnif | ||
Definition | df-psmet 20870* | 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 20871* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 20872, 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 20872* | Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 23756. 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 23778, metgt0 23794, metsym 23785, and mettri 23787. (Contributed by NM, 25-Aug-2006.) |
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) | ||
Definition | df-bl 20873* | Define the metric space ball function. See blval 23821 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 20874 | Define a function whose value is the family of open sets of a metric space. See elmopn 23877 for its main property. (Contributed by NM, 1-Sep-2006.) |
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) | ||
Definition | df-fbas 20875* | 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 20876* | 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 20877* | 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 20878 | Extend class notation with the field of complex numbers. |
class ℂfld | ||
Definition | df-cnfld 20879 |
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 20881, cnfldadd 20883, cnfldmul 20884, cnfldcj 20885, cnfldtset 20886, cnfldle 20887, cnfldds 20888, and cnfldbas 20882. 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 20880 | 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 20881 | 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 20882 | 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 20883 | 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 20884 | 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 20885 | 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 20886 | 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 20887 | 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) | ||
Theorem | cnfldds 20888 | 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.) |
⊢ (abs ∘ − ) = (dist‘ℂfld) | ||
Theorem | cnfldunif 20889 | The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld) | ||
Theorem | cnfldfun 20890 | The field of complex numbers is a function. The proof is much shorter than the proof of cnfldfunALT 20891 by using cnfldstr 20880 and structn0fun 17066: in addition, it must be shown that ∅ ∉ ℂfld. (Contributed by AV, 18-Nov-2021.) |
⊢ Fun ℂfld | ||
Theorem | cnfldfunALT 20891 | The field of complex numbers is a function. Alternate proof of cnfldfun 20890 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.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Fun ℂfld | ||
Theorem | cnfldfunALTOLD 20892 | Obsolete proof of cnfldfunALT 20891 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 20893 | The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 Struct 〈1, ;12〉 | ||
Theorem | xrsex 20894 | The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 ∈ V | ||
Theorem | xrsbas 20895 | The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ* = (Base‘ℝ*𝑠) | ||
Theorem | xrsadd 20896 | The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ +𝑒 = (+g‘ℝ*𝑠) | ||
Theorem | xrsmul 20897 | The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ·e = (.r‘ℝ*𝑠) | ||
Theorem | xrstset 20898 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠) | ||
Theorem | xrsle 20899 | The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ≤ = (le‘ℝ*𝑠) | ||
Theorem | cncrng 20900 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) |
⊢ ℂfld ∈ CRing |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |