![]() |
Metamath
Proof Explorer Theorem List (p. 208 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rhmsubclem1 20701 | Lemma 1 for rhmsubc 20705. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅)) | ||
Theorem | rhmsubclem2 20702 | Lemma 2 for rhmsubc 20705. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌)) | ||
Theorem | rhmsubclem3 20703* | Lemma 3 for rhmsubc 20705. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCat‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
Theorem | rhmsubclem4 20704* | Lemma 4 for rhmsubc 20705. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RngCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | ||
Theorem | rhmsubc 20705 | According to df-subc 17859, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17890 and subcss2 17893). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → 𝐻 ∈ (Subcat‘(RngCat‘𝑈))) | ||
Theorem | rhmsubccat 20706 | The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → ((RngCat‘𝑈) ↾cat 𝐻) ∈ Cat) | ||
Syntax | crlreg 20707 | Set of left-regular elements in a ring. |
class RLReg | ||
Syntax | cdomn 20708 | Class of (ring theoretic) domains. |
class Domn | ||
Syntax | cidom 20709 | Class of integral domains. |
class IDomn | ||
Definition | df-rlreg 20710* | 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 20711* | 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 20712 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ IDomn = (CRing ∩ Domn) | ||
Theorem | rrgval 20713* | 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 20714* | 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 20715 | Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 )) | ||
Theorem | rrgeq0 20716 | 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 20717 | 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 20718 | Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐸 ⊆ 𝐵 | ||
Theorem | unitrrg 20719 | Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸) | ||
Theorem | rrgnz 20720 | In a nonzero ring, the zero is a left zero divisor (that is, not a left-regular element). (Contributed by Thierry Arnoux, 6-May-2025.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → ¬ 0 ∈ 𝐸) | ||
Theorem | isdomn 20721* | Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) | ||
Theorem | domnnzr 20722 | A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | ||
Theorem | domnring 20723 | A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) | ||
Theorem | domneq0 20724 | 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 20725 | 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 | isdomn5 20726* | The equivalence between the right conjuncts in the right hand sides of isdomn 20721 and isdomn2 20727, in predicate calculus form. (Contributed by SN, 16-Sep-2024.) |
⊢ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 )) ↔ ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → 𝑏 = 0 )) | ||
Theorem | isdomn2 20727 | A ring is a domain iff all nonzero elements are regular elements. (Contributed by Mario Carneiro, 28-Mar-2015.) (Proof shortened by SN, 21-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) ⊆ 𝐸)) | ||
Theorem | isdomn2OLD 20728 | Obsolete version of isdomn2 20727 as of 21-Jun-2025. (Contributed by Mario Carneiro, 28-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) ⊆ 𝐸)) | ||
Theorem | domnrrg 20729 | In a domain, a nonzero element is a regular element. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐸) | ||
Theorem | isdomn6 20730 | A ring is a domain iff the regular elements are the nonzero elements. Compare isdomn2 20727, domnrrg 20729. (Contributed by Thierry Arnoux, 6-May-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) = 𝐸)) | ||
Theorem | isdomn3 20731 | Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈ (SubMnd‘𝑈))) | ||
Theorem | isdomn4 20732* | A ring is a domain iff it is nonzero and the left cancellation law for multiplication holds. (Contributed by SN, 15-Sep-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐))) | ||
Theorem | opprdomnb 20733 | A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn 20734. (Contributed by SN, 15-Jun-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ 𝑂 ∈ Domn) | ||
Theorem | opprdomn 20734 | The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn → 𝑂 ∈ Domn) | ||
Theorem | isdomn4r 20735* | A ring is a domain iff it is nonzero and the right cancellation law for multiplication holds. (Contributed by SN, 20-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ (𝐵 ∖ { 0 })((𝑎 · 𝑐) = (𝑏 · 𝑐) → 𝑎 = 𝑏))) | ||
Theorem | domnlcanb 20736 | Left-cancellation law for domains, biconditional version of domnlcan 20737. (Contributed by Thierry Arnoux, 8-Jun-2025.) Shorten this theorem and domnlcan 20737 overall. (Revised by SN, 21-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Domn) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = (𝑋 · 𝑍) ↔ 𝑌 = 𝑍)) | ||
Theorem | domnlcan 20737 | Left-cancellation law for domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof shortened by SN, 21-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 · 𝑍)) ⇒ ⊢ (𝜑 → 𝑌 = 𝑍) | ||
Theorem | domnrcanb 20738 | Right-cancellation law for domains, biconditional version of domnrcan 20739. (Contributed by SN, 21-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑅 ∈ Domn) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑍) = (𝑌 · 𝑍) ↔ 𝑋 = 𝑌)) | ||
Theorem | domnrcan 20739 | Right-cancellation law for domains. (Contributed by SN, 21-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | domneq0r 20740 | Right multiplication by a nonzero element does not change zeroness in a domain. Compare rrgeq0 20716. (Contributed by SN, 21-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑅 ∈ Domn) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑋 = 0 )) | ||
Theorem | isidom 20741 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | ||
Theorem | idomdomd 20742 | An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → 𝑅 ∈ Domn) | ||
Theorem | idomcringd 20743 | An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) Formerly subproof of idomringd 20744. (Proof shortened by SN, 14-May-2025.) |
⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → 𝑅 ∈ CRing) | ||
Theorem | idomringd 20744 | An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → 𝑅 ∈ Ring) | ||
Syntax | cdr 20745 | Extend class notation with class of all division rings. |
class DivRing | ||
Syntax | cfield 20746 | Class of fields. |
class Field | ||
Definition | df-drng 20747 | Define class of all division rings. A division ring is a ring in which the set of units is exactly the nonzero elements of the ring. (Contributed by NM, 18-Oct-2012.) |
⊢ DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)})} | ||
Definition | df-field 20748 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ Field = (DivRing ∩ CRing) | ||
Theorem | isdrng 20749 | The predicate "is a division ring". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 }))) | ||
Theorem | drngunit 20750 | Elementhood in the set of units when 𝑅 is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ))) | ||
Theorem | drngui 20751 | The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑅 ∈ DivRing ⇒ ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅) | ||
Theorem | drngring 20752 | A division ring is a ring. (Contributed by NM, 8-Sep-2011.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) | ||
Theorem | drngringd 20753 | A division ring is a ring. (Contributed by SN, 16-May-2024.) |
⊢ (𝜑 → 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑅 ∈ Ring) | ||
Theorem | drnggrpd 20754 | A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.) |
⊢ (𝜑 → 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑅 ∈ Grp) | ||
Theorem | drnggrp 20755 | A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Grp) | ||
Theorem | isfld 20756 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) | ||
Theorem | flddrngd 20757 | A field is a division ring. (Contributed by SN, 17-Jan-2025.) |
⊢ (𝜑 → 𝑅 ∈ Field) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | fldcrngd 20758 | A field is a commutative ring. (Contributed by SN, 23-Nov-2024.) |
⊢ (𝜑 → 𝑅 ∈ Field) ⇒ ⊢ (𝜑 → 𝑅 ∈ CRing) | ||
Theorem | isdrng2 20759 | A division ring can equivalently be defined as a ring such that the nonzero elements form a group under multiplication (from which it follows that this is the same group as the group of units). (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ⇒ ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ Grp)) | ||
Theorem | drngprop 20760 | If two structures have the same ring components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Mario Carneiro, 28-Dec-2014.) |
⊢ (Base‘𝐾) = (Base‘𝐿) & ⊢ (+g‘𝐾) = (+g‘𝐿) & ⊢ (.r‘𝐾) = (.r‘𝐿) ⇒ ⊢ (𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing) | ||
Theorem | drngmgp 20761 | A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ⇒ ⊢ (𝑅 ∈ DivRing → 𝐺 ∈ Grp) | ||
Theorem | drngid 20762 | A division ring's unity is the identity element of its multiplicative group. (Contributed by NM, 7-Sep-2011.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ⇒ ⊢ (𝑅 ∈ DivRing → 1 = (0g‘𝐺)) | ||
Theorem | drngunz 20763 | A division ring's unity is different from its zero. (Contributed by NM, 8-Sep-2011.) |
⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 1 ≠ 0 ) | ||
Theorem | drngnzr 20764 | A division ring is a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) | ||
Theorem | drngdomn 20765 | A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn) | ||
Theorem | drngmcl 20766 | The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011.) (Proof shortened by SN, 25-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ (𝐵 ∖ { 0 }) ∧ 𝑌 ∈ (𝐵 ∖ { 0 })) → (𝑋 · 𝑌) ∈ (𝐵 ∖ { 0 })) | ||
Theorem | drngmclOLD 20767 | Obsolete version of drngmcl 20766 as of 25-Jun-2025. The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ (𝐵 ∖ { 0 }) ∧ 𝑌 ∈ (𝐵 ∖ { 0 })) → (𝑋 · 𝑌) ∈ (𝐵 ∖ { 0 })) | ||
Theorem | drngid2 20768 | Properties showing that an element 𝐼 is the identity element of a division ring. (Contributed by Mario Carneiro, 11-Oct-2013.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → ((𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ∧ (𝐼 · 𝐼) = 𝐼) ↔ 1 = 𝐼)) | ||
Theorem | drnginvrcl 20769 | Closure of the multiplicative inverse in a division ring. (reccl 11926 analog). (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐵) | ||
Theorem | drnginvrn0 20770 | The multiplicative inverse in a division ring is nonzero. (recne0 11932 analog). (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ≠ 0 ) | ||
Theorem | drnginvrcld 20771 | Closure of the multiplicative inverse in a division ring. (reccld 12033 analog). (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ 𝐵) | ||
Theorem | drnginvrl 20772 | Property of the multiplicative inverse in a division ring. (recid2 11934 analog). (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ((𝐼‘𝑋) · 𝑋) = 1 ) | ||
Theorem | drnginvrr 20773 | Property of the multiplicative inverse in a division ring. (recid 11933 analog). (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑋 · (𝐼‘𝑋)) = 1 ) | ||
Theorem | drnginvrld 20774 | Property of the multiplicative inverse in a division ring. (recid2d 12036 analog). (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → ((𝐼‘𝑋) · 𝑋) = 1 ) | ||
Theorem | drnginvrrd 20775 | Property of the multiplicative inverse in a division ring. (recidd 12035 analog). (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 · (𝐼‘𝑋)) = 1 ) | ||
Theorem | drngmul0or 20776 | A product is zero iff one of its factors is zero. (Contributed by NM, 8-Oct-2014.) (Proof shortened by SN, 25-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 ))) | ||
Theorem | drngmul0orOLD 20777 | Obsolete version of drngmul0or 20776 as of 25-Jun-2025. (Contributed by NM, 8-Oct-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 ))) | ||
Theorem | drngmulne0 20778 | A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) ≠ 0 ↔ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ))) | ||
Theorem | drngmuleq0 20779 | An element is zero iff its product with a nonzero element is zero. (Contributed by NM, 8-Oct-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑋 = 0 )) | ||
Theorem | opprdrng 20780 | The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing ↔ 𝑂 ∈ DivRing) | ||
Theorem | isdrngd 20781* | Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element 𝑥 should have a left-inverse 𝐼(𝑥). See isdrngrd 20782 for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013.) Remove hypothesis. (Revised by SN, 19-Feb-2025.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 0 = (0g‘𝑅)) & ⊢ (𝜑 → 1 = (1r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) & ⊢ (𝜑 → 1 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 ) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | isdrngrd 20782* | Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element 𝑥 should have a right-inverse 𝐼(𝑥). See isdrngd 20781 for the characterization using left-inverses. (Contributed by NM, 10-Aug-2013.) Remove hypothesis. (Revised by SN, 19-Feb-2025.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 0 = (0g‘𝑅)) & ⊢ (𝜑 → 1 = (1r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) & ⊢ (𝜑 → 1 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝑥 · 𝐼) = 1 ) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | isdrngdOLD 20783* | Obsolete version of isdrngd 20781 as of 19-Feb-2025. (Contributed by NM, 2-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 0 = (0g‘𝑅)) & ⊢ (𝜑 → 1 = (1r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) & ⊢ (𝜑 → 1 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 ) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | isdrngrdOLD 20784* | Obsolete version of isdrngrd 20782 as of 19-Feb-2025. (Contributed by NM, 10-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 0 = (0g‘𝑅)) & ⊢ (𝜑 → 1 = (1r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) & ⊢ (𝜑 → 1 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝑥 · 𝐼) = 1 ) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | drngpropd 20785* | If two structures have the same group components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing)) | ||
Theorem | fldpropd 20786* | If two structures have the same group components (properties), one is a field iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Field ↔ 𝐿 ∈ Field)) | ||
Theorem | fldidom 20787 | A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof shortened by SN, 11-Nov-2024.) |
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn) | ||
Theorem | fldidomOLD 20788 | Obsolete version of fldidom 20787 as of 11-Nov-2024. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn) | ||
Theorem | fidomndrnglem 20789* | Lemma for fidomndrng 20790. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 })) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴)) ⇒ ⊢ (𝜑 → 𝐴 ∥ 1 ) | ||
Theorem | fidomndrng 20790 | A finite domain is a division ring. Note that Wedderburn's little theorem (not proved) states that finite division rings are fields. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ Domn ↔ 𝑅 ∈ DivRing)) | ||
Theorem | fiidomfld 20791 | A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ IDomn ↔ 𝑅 ∈ Field)) | ||
Theorem | rng1nnzr 20792 | 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 20793 | 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 20794 | 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 20795 | 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 20796 | The zero ring is not a field. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉, 〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ⇒ ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ Field) | ||
Theorem | issubdrg 20797* | Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → (𝑆 ∈ DivRing ↔ ∀𝑥 ∈ (𝐴 ∖ { 0 })(𝐼‘𝑥) ∈ 𝐴)) | ||
Theorem | drhmsubc 20798* | According to df-subc 17859, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17890 and subcss2 17893). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐶 = (𝑈 ∩ DivRing) & ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠)) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCat‘𝑈))) | ||
Theorem | drngcat 20799* | The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐶 = (𝑈 ∩ DivRing) & ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠)) ⇒ ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐽) ∈ Cat) | ||
Theorem | fldcat 20800* | The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐶 = (𝑈 ∩ DivRing) & ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠)) & ⊢ 𝐷 = (𝑈 ∩ Field) & ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠)) ⇒ ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐹) ∈ Cat) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |