| Metamath
Proof Explorer Theorem List (p. 380 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | crngo 37901 | Extend class notation with the class of all unital rings. |
| class RingOps | ||
| Definition | df-rngo 37902* | 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 37903 | 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 37904* | 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 37905* | Conditions that determine a ring. (Changed label from isringd 20288 to isrngod 37905-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 37906* | 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 37907 | 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 37908 | 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 37909* | 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 37910* | 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 37911 | 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 37912 | 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 37913 | 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 37914* | 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 37915 | 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 37916 | In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
| ⊢ (〈𝐺, 𝐻〉 ∈ RingOps → 𝐺 ∈ AbelOp) | ||
| Theorem | rngogrpo 37917 | 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 37918 | The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → 𝑋 ≠ ∅) | ||
| Theorem | rngogcl 37919 | 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 37920 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) | ||
| Theorem | rngoaass 37921 | The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) | ||
| Theorem | rngoa32 37922 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵)) | ||
| Theorem | rngoa4 37923 | 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 37924 | 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 37925 | 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 37926 | A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → 𝑍 ∈ 𝑋) | ||
| Theorem | rngo0rid 37927 | 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 37928 | 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 37929 | 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 37930 | 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 37931 | Obsolete as of 25-Jan-2020. Use ring1zr 20777 or srg1zr 20212 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 37932 | Obsolete as of 25-Jan-2020. Use rngen1zr 20778 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 37933 | Obsolete as of 25-Jan-2020. Use ringen1zr 20779 or srgen1zr 20213 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 37934 | A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋) | ||
| Theorem | rngoaddneg1 37935 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑍) | ||
| Theorem | rngoaddneg2 37936 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑍) | ||
| Theorem | rngosub 37937 | Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁‘𝐵))) | ||
| Theorem | rngmgmbs4 37938* | 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 37939 | 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 37940 | 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 37941 | 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 37942 | 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 37943 | 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 37944 | 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 37945 | 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 37946 | 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 37947 | Obsolete as of 23-Jan-2020. Use 0ring01eqbi 20532 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 37948 | 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 37949 | 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 37950 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = ((𝑁‘𝐴)𝐻𝐵)) | ||
| Theorem | rngonegrmul 37951 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = (𝐴𝐻(𝑁‘𝐵))) | ||
| Theorem | rngosubdi 37952 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐷𝐶)) = ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶))) | ||
| Theorem | rngosubdir 37953 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶))) | ||
| Theorem | zerdivemp1x 37954* | In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv 20298. (Contributed by Jeff Madsen, 18-Apr-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ ∃𝑎 ∈ 𝑋 (𝑎𝐻𝐴) = 𝑈) → (𝐵 ∈ 𝑋 → ((𝐴𝐻𝐵) = 𝑍 → 𝐵 = 𝑍))) | ||
| Syntax | cdrng 37955 | Extend class notation with the class of all division rings. |
| class DivRingOps | ||
| Definition | df-drngo 37956* | 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 37957 | 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 37958 | 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 37959 | Obsolete as of 23-Jan-2020. Use mnd1id 18793 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 37960 | 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 37961 | 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 37962* | Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝐺:(𝑋 × 𝑋)⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ (𝜑 → 𝑈 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑈𝐺𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑛 ∈ 𝑋 (𝑛𝐺𝑥) = 𝑈) ⇒ ⊢ (𝜑 → 𝐺 ∈ GrpOp) | ||
| Theorem | isdrngo1 37963 | The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) | ||
| Theorem | divrngcl 37964 | The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ DivRingOps ∧ 𝐴 ∈ (𝑋 ∖ {𝑍}) ∧ 𝐵 ∈ (𝑋 ∖ {𝑍})) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ {𝑍})) | ||
| Theorem | isdrngo2 37965* | A division ring is a ring in which 1 ≠ 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))) | ||
| Theorem | isdrngo3 37966* | A division ring is a ring in which 1 ≠ 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))) | ||
| Syntax | crngohom 37967 | Extend class notation with the class of ring homomorphisms. |
| class RingOpsHom | ||
| Syntax | crngoiso 37968 | Extend class notation with the class of ring isomorphisms. |
| class RingOpsIso | ||
| Syntax | crisc 37969 | Extend class notation with the ring isomorphism relation. |
| class ≃𝑟 | ||
| Definition | df-rngohom 37970* | Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ RingOpsHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st ‘𝑠) ↑m ran (1st ‘𝑟)) ∣ ((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))))}) | ||
| Theorem | rngohomval 37971* | The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 22-Sep-2015.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝐾 = (2nd ‘𝑆) & ⊢ 𝑌 = ran 𝐽 & ⊢ 𝑉 = (GId‘𝐾) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsHom 𝑆) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))}) | ||
| Theorem | isrngohom 37972* | The predicate "is a ring homomorphism from 𝑅 to 𝑆". (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝐾 = (2nd ‘𝑆) & ⊢ 𝑌 = ran 𝐽 & ⊢ 𝑉 = (GId‘𝐾) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ↔ (𝐹:𝑋⟶𝑌 ∧ (𝐹‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦)))))) | ||
| Theorem | rngohomf 37973 | A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹:𝑋⟶𝑌) | ||
| Theorem | rngohomcl 37974 | Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ 𝑌) | ||
| Theorem | rngohom1 37975 | A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) & ⊢ 𝐾 = (2nd ‘𝑆) & ⊢ 𝑉 = (GId‘𝐾) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑈) = 𝑉) | ||
| Theorem | rngohomadd 37976 | Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐺𝐵)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵))) | ||
| Theorem | rngohommul 37977 | Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝐾 = (2nd ‘𝑆) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵))) | ||
| Theorem | rngogrphom 37978 | A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐽 = (1st ‘𝑆) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹 ∈ (𝐺 GrpOpHom 𝐽)) | ||
| Theorem | rngohom0 37979 | A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑊 = (GId‘𝐽) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑍) = 𝑊) | ||
| Theorem | rngohomsub 37980 | Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐻 = ( /𝑔 ‘𝐺) & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝐾 = ( /𝑔 ‘𝐽) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵))) | ||
| Theorem | rngohomco 37981 | The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇)) | ||
| Theorem | rngokerinj 37982 | A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑊 = (GId‘𝐺) & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 & ⊢ 𝑍 = (GId‘𝐽) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹:𝑋–1-1→𝑌 ↔ (◡𝐹 “ {𝑍}) = {𝑊})) | ||
| Definition | df-rngoiso 37983* | Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ RingOpsIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1st ‘𝑟)–1-1-onto→ran (1st ‘𝑠)}) | ||
| Theorem | rngoisoval 37984* | The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsIso 𝑆) = {𝑓 ∈ (𝑅 RingOpsHom 𝑆) ∣ 𝑓:𝑋–1-1-onto→𝑌}) | ||
| Theorem | isrngoiso 37985 | The predicate "is a ring isomorphism between 𝑅 and 𝑆". (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋–1-1-onto→𝑌))) | ||
| Theorem | rngoiso1o 37986 | A ring isomorphism is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹:𝑋–1-1-onto→𝑌) | ||
| Theorem | rngoisohom 37987 | A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) | ||
| Theorem | rngoisocnv 37988 | The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → ◡𝐹 ∈ (𝑆 RingOpsIso 𝑅)) | ||
| Theorem | rngoisoco 37989 | The composition of two ring isomorphisms is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsIso 𝑇)) | ||
| Definition | df-risc 37990* | Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ≃𝑟 = {〈𝑟, 𝑠〉 ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠))} | ||
| Theorem | isriscg 37991* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆)))) | ||
| Theorem | isrisc 37992* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑅 ∈ V & ⊢ 𝑆 ∈ V ⇒ ⊢ (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆))) | ||
| Theorem | risc 37993* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 ≃𝑟 𝑆 ↔ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆))) | ||
| Theorem | risci 37994 | Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝑅 ≃𝑟 𝑆) | ||
| Theorem | riscer 37995 | Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ≃𝑟 Er dom ≃𝑟 | ||
| Syntax | ccm2 37996 | Extend class notation with a class that adds commutativity to various flavors of rings. |
| class Com2 | ||
| Definition | df-com2 37997* | A device to add commutativity to various sorts of rings. I use ran 𝑔 because I suppose 𝑔 has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.) |
| ⊢ Com2 = {〈𝑔, ℎ〉 ∣ ∀𝑎 ∈ ran 𝑔∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎)} | ||
| Syntax | cfld 37998 | Extend class notation with the class of all fields. |
| class Fld | ||
| Definition | df-fld 37999 | Definition of a field. A field is a commutative division ring. (Contributed by FL, 6-Sep-2009.) (Revised by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.) |
| ⊢ Fld = (DivRingOps ∩ Com2) | ||
| Syntax | ccring 38000 | Extend class notation with the class of commutative rings. |
| class CRingOps | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |