HomeTheorem List (p. 382 of 502)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 382 of 502) | < 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-31005) |
Hilbert Space Explorer
(31006-32528) |
Users' Mathboxes
(32529-50158) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | exidu1 38101* | Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) | ||
| Theorem | idrval 38102* | The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝐴 → 𝑈 = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))) | ||
| Theorem | iorlid 38103 | A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝑈 ∈ 𝑋) | ||
| Theorem | cmpidelt 38104 | A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ 𝑋) → ((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴)) | ||
| Syntax | csem 38105 | Extend class notation with the class of all semigroups. |
| class SemiGrp | ||
| Definition | df-sgrOLD 38106 | Obsolete version of df-sgrp 18656 as of 3-Feb-2020. A semigroup is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ SemiGrp = (Magma ∩ Ass) | ||
| Theorem | smgrpismgmOLD 38107 | Obsolete version of sgrpmgm 18661 as of 3-Feb-2020. A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐺 ∈ SemiGrp → 𝐺 ∈ Magma) | ||
| Theorem | issmgrpOLD 38108* | Obsolete version of issgrp 18657 as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ SemiGrp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))) | ||
| Theorem | smgrpmgm 38109 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ SemiGrp → 𝐺:(𝑋 × 𝑋)⟶𝑋) | ||
| Theorem | smgrpassOLD 38110* | Obsolete version of sgrpass 18662 as of 3-Feb-2020. A semigroup is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ SemiGrp → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) | ||
| Syntax | cmndo 38111 | Extend class notation with the class of all monoids. |
| class MndOp | ||
| Definition | df-mndo 38112 | A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ MndOp = (SemiGrp ∩ ExId ) | ||
| Theorem | mndoissmgrpOLD 38113 | Obsolete version of mndsgrp 18677 as of 3-Feb-2020. A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ SemiGrp) | ||
| Theorem | mndoisexid 38114 | A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ ExId ) | ||
| Theorem | mndoismgmOLD 38115 | Obsolete version of mndmgm 18678 as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ Magma) | ||
| Theorem | mndomgmid 38116 | A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ (Magma ∩ ExId )) | ||
| Theorem | ismndo 38117* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺 ∈ SemiGrp ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦)))) | ||
| Theorem | ismndo1 38118* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦)))) | ||
| Theorem | ismndo2 38119* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦)))) | ||
| Theorem | grpomndo 38120 | A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ (𝐺 ∈ GrpOp → 𝐺 ∈ MndOp) | ||
| Theorem | exidcl 38121 | Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||
| Theorem | exidreslem 38122* | Lemma for exidres 38123 and exidresid 38124. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑈 ∈ dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) | ||
| Theorem | exidres 38123 | The restriction of a binary operation with identity to a subset containing the identity has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → 𝐻 ∈ ExId ) | ||
| Theorem | exidresid 38124 | The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) ⇒ ⊢ (((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (GId‘𝐻) = 𝑈) | ||
| Theorem | ablo4pnp 38125 | A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹))) | ||
| Theorem | grpoeqdivid 38126 | Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 = 𝐵 ↔ (𝐴𝐷𝐵) = 𝑈)) | ||
| Theorem | grposnOLD 38127 | The group operation for the singleton group. Obsolete, use grp1 18989. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∈ GrpOp | ||
| Syntax | cghomOLD 38128 | Obsolete version of cghm 19153 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.) |
| class GrpOpHom | ||
| Definition | df-ghomOLD 38129* | Obsolete version of df-ghm 19154 as of 15-Mar-2020. Define the set of group homomorphisms from 𝑔 to ℎ. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
| ⊢ GrpOpHom = (𝑔 ∈ GrpOp, ℎ ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))}) | ||
| Theorem | elghomlem1OLD 38130* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 38132. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))} ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆) | ||
| Theorem | elghomlem2OLD 38131* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 38132. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))} ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) | ||
| Theorem | elghomOLD 38132* | Obsolete version of isghm 19156 as of 15-Mar-2020. Membership in the set of group homomorphisms from 𝐺 to 𝐻. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑊 = ran 𝐻 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝐹:𝑋⟶𝑊 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) | ||
| Theorem | ghomlinOLD 38133 | Obsolete version of ghmlin 19162 as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴)𝐻(𝐹‘𝐵)) = (𝐹‘(𝐴𝐺𝐵))) | ||
| Theorem | ghomidOLD 38134 | Obsolete version of ghmid 19163 as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑇 = (GId‘𝐻) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹‘𝑈) = 𝑇) | ||
| Theorem | ghomf 38135 | Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑊 = ran 𝐻 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋⟶𝑊) | ||
| Theorem | ghomco 38136 | The composition of two group homomorphisms is a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) ∧ (𝑆 ∈ (𝐺 GrpOpHom 𝐻) ∧ 𝑇 ∈ (𝐻 GrpOpHom 𝐾))) → (𝑇 ∘ 𝑆) ∈ (𝐺 GrpOpHom 𝐾)) | ||
| Theorem | ghomdiv 38137 | Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) & ⊢ 𝐶 = ( /𝑔 ‘𝐻) ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐷𝐵)) = ((𝐹‘𝐴)𝐶(𝐹‘𝐵))) | ||
| Theorem | grpokerinj 38138 | A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑊 = (GId‘𝐺) & ⊢ 𝑌 = ran 𝐻 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹:𝑋–1-1→𝑌 ↔ (◡𝐹 “ {𝑈}) = {𝑊})) | ||
| Syntax | crngo 38139 | Extend class notation with the class of all unital rings. |
| class RingOps | ||
| Definition | df-rngo 38140* | Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.) |
| ⊢ RingOps = {⟨𝑔, ℎ⟩ ∣ ((𝑔 ∈ AbelOp ∧ ℎ:(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))) ∧ ∃𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)))} | ||
| Theorem | relrngo 38141 | The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ Rel RingOps | ||
| Theorem | isrngo 38142* | The predicate "is a (unital) ring." Definition of "ring with unit" in [Schechter] p. 187. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐻 ∈ 𝐴 → (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))) | ||
| Theorem | isrngod 38143* | Conditions that determine a ring. (Changed label from isringd 20238 to isrngod 38143-NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐺 ∈ AbelOp) & ⊢ (𝜑 → 𝑋 = ran 𝐺) & ⊢ (𝜑 → 𝐻:(𝑋 × 𝑋)⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) & ⊢ (𝜑 → 𝑈 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐻𝑦) = 𝑦) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝑈) = 𝑦) ⇒ ⊢ (𝜑 → ⟨𝐺, 𝐻⟩ ∈ RingOps) | ||
| Theorem | rngoi 38144* | The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))) | ||
| Theorem | rngosm 38145 | Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → 𝐻:(𝑋 × 𝑋)⟶𝑋) | ||
| Theorem | rngocl 38146 | Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) ∈ 𝑋) | ||
| Theorem | rngoid 38147* | The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑢 ∈ 𝑋 ((𝑢𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑢) = 𝐴)) | ||
| Theorem | rngoideu 38148* | The unity element of a ring is unique. (Contributed by NM, 4-Apr-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) | ||
| Theorem | rngodi 38149 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐺𝐶)) = ((𝐴𝐻𝐵)𝐺(𝐴𝐻𝐶))) | ||
| Theorem | rngodir 38150 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐺(𝐵𝐻𝐶))) | ||
| Theorem | rngoass 38151 | Associative law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = (𝐴𝐻(𝐵𝐻𝐶))) | ||
| Theorem | rngo2 38152* | A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝑋 (𝐴𝐺𝐴) = ((𝑥𝐺𝑥)𝐻𝐴)) | ||
| Theorem | rngoablo 38153 | A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ AbelOp) | ||
| Theorem | rngoablo2 38154 | In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
| ⊢ (⟨𝐺, 𝐻⟩ ∈ RingOps → 𝐺 ∈ AbelOp) | ||
| Theorem | rngogrpo 38155 | A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp) | ||
| Theorem | rngone0 38156 | The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → 𝑋 ≠ ∅) | ||
| Theorem | rngogcl 38157 | Closure law for the addition (group) operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||
| Theorem | rngocom 38158 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) | ||
| Theorem | rngoaass 38159 | The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) | ||
| Theorem | rngoa32 38160 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵)) | ||
| Theorem | rngoa4 38161 | Rearrangement of 4 terms in a sum of ring elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷))) | ||
| Theorem | rngorcan 38162 | Right cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | rngolcan 38163 | Left cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | rngo0cl 38164 | A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → 𝑍 ∈ 𝑋) | ||
| Theorem | rngo0rid 38165 | The additive identity of a ring is a right identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴) | ||
| Theorem | rngo0lid 38166 | The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑍𝐺𝐴) = 𝐴) | ||
| Theorem | rngolz 38167 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
| ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑍𝐻𝐴) = 𝑍) | ||
| Theorem | rngorz 38168 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
| ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻𝑍) = 𝑍) | ||
| Theorem | rngosn3 38169 | Obsolete as of 25-Jan-2020. Use ring1zr 20721 or srg1zr 20162 instead. The only unital ring with a base set consisting in one element is the zero ring. (Contributed by FL, 13-Feb-2010.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ 𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩)) | ||
| Theorem | rngosn4 38170 | Obsolete as of 25-Jan-2020. Use rngen1zr 20722 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑋 ≈ 1o ↔ 𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩)) | ||
| Theorem | rngosn6 38171 | Obsolete as of 25-Jan-2020. Use ringen1zr 20723 or srgen1zr 20163 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o ↔ 𝑅 = ⟨{⟨⟨𝑍, 𝑍⟩, 𝑍⟩}, {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩)) | ||
| Theorem | rngonegcl 38172 | A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋) | ||
| Theorem | rngoaddneg1 38173 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑍) | ||
| Theorem | rngoaddneg2 38174 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑍) | ||
| Theorem | rngosub 38175 | Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁‘𝐵))) | ||
| Theorem | rngmgmbs4 38176* | The range of an internal operation with a left and right identity element equals its base set. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ ((𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) → ran 𝐺 = 𝑋) | ||
| Theorem | rngodm1dm2 38177 | In a unital ring the domain of the first variable of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → dom dom 𝐺 = dom dom 𝐻) | ||
| Theorem | rngorn1 38178 | In a unital ring the range of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → ran 𝐺 = dom dom 𝐻) | ||
| Theorem | rngorn1eq 38179 | In a unital ring the range of the addition equals the range of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → ran 𝐺 = ran 𝐻) | ||
| Theorem | rngomndo 38180 | In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → 𝐻 ∈ MndOp) | ||
| Theorem | rngoidmlem 38181 | The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran (1st ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)) | ||
| Theorem | rngolidm 38182 | The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran (1st ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑈𝐻𝐴) = 𝐴) | ||
| Theorem | rngoridm 38183 | The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran (1st ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻𝑈) = 𝐴) | ||
| Theorem | rngo1cl 38184 | The unity element of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋) | ||
| Theorem | rngoueqz 38185 | Obsolete as of 23-Jan-2020. Use 0ring01eqbi 20477 instead. In a unital ring the zero equals the ring unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o ↔ 𝑈 = 𝑍)) | ||
| Theorem | rngonegmn1l 38186 | Negation in a ring is the same as left multiplication by -1. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = ((𝑁‘𝑈)𝐻𝐴)) | ||
| Theorem | rngonegmn1r 38187 | Negation in a ring is the same as right multiplication by -1. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈))) | ||
| Theorem | rngoneglmul 38188 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = ((𝑁‘𝐴)𝐻𝐵)) | ||
| Theorem | rngonegrmul 38189 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = (𝐴𝐻(𝑁‘𝐵))) | ||
| Theorem | rngosubdi 38190 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐷𝐶)) = ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶))) | ||
| Theorem | rngosubdir 38191 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶))) | ||
| Theorem | zerdivemp1x 38192* | In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv 20248. (Contributed by Jeff Madsen, 18-Apr-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ ∃𝑎 ∈ 𝑋 (𝑎𝐻𝐴) = 𝑈) → (𝐵 ∈ 𝑋 → ((𝐴𝐻𝐵) = 𝑍 → 𝐵 = 𝑍))) | ||
| Syntax | cdrng 38193 | Extend class notation with the class of all division rings. |
| class DivRingOps | ||
| Definition | df-drngo 38194* | Define the class of all division rings (sometimes called skew fields). A division ring is a unital ring where every element except the additive identity has a multiplicative inverse. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.) |
| ⊢ DivRingOps = {⟨𝑔, ℎ⟩ ∣ (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} | ||
| Theorem | isdivrngo 38195 | The predicate "is a division ring". (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ 𝐴 → (⟨𝐺, 𝐻⟩ ∈ DivRingOps ↔ (⟨𝐺, 𝐻⟩ ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) | ||
| Theorem | drngoi 38196 | The properties of a division ring. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) | ||
| Theorem | gidsn 38197 | Obsolete as of 23-Jan-2020. Use mnd1id 18717 instead. The identity element of the trivial group. (Contributed by FL, 21-Jun-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (GId‘{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}) = 𝐴 | ||
| Theorem | zrdivrng 38198 | The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ¬ ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩ ∈ DivRingOps | ||
| Theorem | dvrunz 38199 | In a division ring the ring unit is different from the zero. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ DivRingOps → 𝑈 ≠ 𝑍) | ||
| Theorem | isgrpda 38200* | Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝐺:(𝑋 × 𝑋)⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ (𝜑 → 𝑈 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑈𝐺𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑛 ∈ 𝑋 (𝑛𝐺𝑥) = 𝑈) ⇒ ⊢ (𝜑 → 𝐺 ∈ GrpOp) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |