HomeTheorem List (p. 380 of 489)
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. 380 of 489) | < 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-30950) |
Hilbert Space Explorer
(30951-32473) |
Users' Mathboxes
(32474-48899) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rngonegmn1l 37901 | 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 37902 | 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 37903 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = ((𝑁‘𝐴)𝐻𝐵)) | ||
| Theorem | rngonegrmul 37904 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = (𝐴𝐻(𝑁‘𝐵))) | ||
| Theorem | rngosubdi 37905 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐷𝐶)) = ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶))) | ||
| Theorem | rngosubdir 37906 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶))) | ||
| Theorem | zerdivemp1x 37907* | In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv 20324. (Contributed by Jeff Madsen, 18-Apr-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ ∃𝑎 ∈ 𝑋 (𝑎𝐻𝐴) = 𝑈) → (𝐵 ∈ 𝑋 → ((𝐴𝐻𝐵) = 𝑍 → 𝐵 = 𝑍))) | ||
| Syntax | cdrng 37908 | Extend class notation with the class of all division rings. |
| class DivRingOps | ||
| Definition | df-drngo 37909* | 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 37910 | 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 37911 | 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 37912 | Obsolete as of 23-Jan-2020. Use mnd1id 18815 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 37913 | 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 37914 | 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 37915* | Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝐺:(𝑋 × 𝑋)⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ (𝜑 → 𝑈 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑈𝐺𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑛 ∈ 𝑋 (𝑛𝐺𝑥) = 𝑈) ⇒ ⊢ (𝜑 → 𝐺 ∈ GrpOp) | ||
| Theorem | isdrngo1 37916 | The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) | ||
| Theorem | divrngcl 37917 | 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 37918* | 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 37919* | 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 37920 | Extend class notation with the class of ring homomorphisms. |
| class RingOpsHom | ||
| Syntax | crngoiso 37921 | Extend class notation with the class of ring isomorphisms. |
| class RingOpsIso | ||
| Syntax | crisc 37922 | Extend class notation with the ring isomorphism relation. |
| class ≃𝑟 | ||
| Definition | df-rngohom 37923* | 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 37924* | 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 37925* | 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 37926 | A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹:𝑋⟶𝑌) | ||
| Theorem | rngohomcl 37927 | Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ 𝑌) | ||
| Theorem | rngohom1 37928 | A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) & ⊢ 𝐾 = (2nd ‘𝑆) & ⊢ 𝑉 = (GId‘𝐾) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑈) = 𝑉) | ||
| Theorem | rngohomadd 37929 | Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐺𝐵)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵))) | ||
| Theorem | rngohommul 37930 | Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝐾 = (2nd ‘𝑆) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵))) | ||
| Theorem | rngogrphom 37931 | A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐽 = (1st ‘𝑆) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹 ∈ (𝐺 GrpOpHom 𝐽)) | ||
| Theorem | rngohom0 37932 | A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑊 = (GId‘𝐽) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑍) = 𝑊) | ||
| Theorem | rngohomsub 37933 | Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐻 = ( /𝑔 ‘𝐺) & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝐾 = ( /𝑔 ‘𝐽) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵))) | ||
| Theorem | rngohomco 37934 | 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 37935 | 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 37936* | 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 37937* | 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 37938 | 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 37939 | 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 37940 | A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) | ||
| Theorem | rngoisocnv 37941 | The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → ◡𝐹 ∈ (𝑆 RingOpsIso 𝑅)) | ||
| Theorem | rngoisoco 37942 | 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 37943* | Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ≃𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠))} | ||
| Theorem | isriscg 37944* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆)))) | ||
| Theorem | isrisc 37945* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑅 ∈ V & ⊢ 𝑆 ∈ V ⇒ ⊢ (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆))) | ||
| Theorem | risc 37946* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 ≃𝑟 𝑆 ↔ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆))) | ||
| Theorem | risci 37947 | Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝑅 ≃𝑟 𝑆) | ||
| Theorem | riscer 37948 | Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ≃𝑟 Er dom ≃𝑟 | ||
| Syntax | ccm2 37949 | Extend class notation with a class that adds commutativity to various flavors of rings. |
| class Com2 | ||
| Definition | df-com2 37950* | 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 37951 | Extend class notation with the class of all fields. |
| class Fld | ||
| Definition | df-fld 37952 | 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 37953 | Extend class notation with the class of commutative rings. |
| class CRingOps | ||
| Definition | df-crngo 37954 | Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ CRingOps = (RingOps ∩ Com2) | ||
| Theorem | iscom2 37955* | A device to add commutativity to various sorts of rings. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.) |
| ⊢ ((𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐵) → (⟨𝐺, 𝐻⟩ ∈ Com2 ↔ ∀𝑎 ∈ ran 𝐺∀𝑏 ∈ ran 𝐺(𝑎𝐻𝑏) = (𝑏𝐻𝑎))) | ||
| Theorem | iscrngo 37956 | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2)) | ||
| Theorem | iscrngo2 37957* | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) | ||
| Theorem | iscringd 37958* | Conditions that determine a commutative ring. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2013.) |
| ⊢ (𝜑 → 𝐺 ∈ AbelOp) & ⊢ (𝜑 → 𝑋 = ran 𝐺) & ⊢ (𝜑 → 𝐻:(𝑋 × 𝑋)⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧))) & ⊢ (𝜑 → 𝑈 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝑈) = 𝑦) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐻𝑦) = (𝑦𝐻𝑥)) ⇒ ⊢ (𝜑 → ⟨𝐺, 𝐻⟩ ∈ CRingOps) | ||
| Theorem | flddivrng 37959 | A field is a division ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| ⊢ (𝐾 ∈ Fld → 𝐾 ∈ DivRingOps) | ||
| Theorem | crngorngo 37960 | A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps) | ||
| Theorem | crngocom 37961 | The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) = (𝐵𝐻𝐴)) | ||
| Theorem | crngm23 37962 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐻𝐵)) | ||
| Theorem | crngm4 37963 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻(𝐶𝐻𝐷)) = ((𝐴𝐻𝐶)𝐻(𝐵𝐻𝐷))) | ||
| Theorem | fldcrngo 37964 | A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ (𝐾 ∈ Fld → 𝐾 ∈ CRingOps) | ||
| Theorem | isfld2 37965 | The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps)) | ||
| Theorem | crngohomfo 37966 | The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋–onto→𝑌)) → 𝑆 ∈ CRingOps) | ||
| Syntax | cidl 37967 | Extend class notation with the class of ideals. |
| class Idl | ||
| Syntax | cpridl 37968 | Extend class notation with the class of prime ideals. |
| class PrIdl | ||
| Syntax | cmaxidl 37969 | Extend class notation with the class of maximal ideals. |
| class MaxIdl | ||
| Definition | df-idl 37970* | Define the class of (two-sided) ideals of a ring 𝑅. A subset of 𝑅 is an ideal if it contains 0, is closed under addition, and is closed under multiplication on either side by any element of 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ Idl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ 𝒫 ran (1st ‘𝑟) ∣ ((GId‘(1st ‘𝑟)) ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥(1st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st ‘𝑟)((𝑧(2nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd ‘𝑟)𝑧) ∈ 𝑖)))}) | ||
| Definition | df-pridl 37971* | Define the class of prime ideals of a ring 𝑅. A proper ideal 𝐼 of 𝑅 is prime if whenever 𝐴𝐵 ⊆ 𝐼 for ideals 𝐴 and 𝐵, either 𝐴 ⊆ 𝐼 or 𝐵 ⊆ 𝐼. The more familiar definition using elements rather than ideals is equivalent provided 𝑅 is commutative; see ispridl2 37998 and ispridlc 38030. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Definition | df-maxidl 37972* | Define the class of maximal ideals of a ring 𝑅. A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ MaxIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))}) | ||
| Theorem | idlval 37973* | The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → (Idl‘𝑅) = {𝑖 ∈ 𝒫 𝑋 ∣ (𝑍 ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥𝐺𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝑖 ∧ (𝑥𝐻𝑧) ∈ 𝑖)))}) | ||
| Theorem | isidl 37974* | The predicate "is an ideal of the ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼))))) | ||
| Theorem | isidlc 37975* | The predicate "is an ideal of the commutative ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ CRingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 (𝑧𝐻𝑥) ∈ 𝐼)))) | ||
| Theorem | idlss 37976 | An ideal of 𝑅 is a subset of 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝐼 ⊆ 𝑋) | ||
| Theorem | idlcl 37977 | An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ 𝑋) | ||
| Theorem | idl0cl 37978 | An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝑍 ∈ 𝐼) | ||
| Theorem | idladdcl 37979 | An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐺𝐵) ∈ 𝐼) | ||
| Theorem | idllmulcl 37980 | An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐵𝐻𝐴) ∈ 𝐼) | ||
| Theorem | idlrmulcl 37981 | An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐻𝐵) ∈ 𝐼) | ||
| Theorem | idlnegcl 37982 | An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → (𝑁‘𝐴) ∈ 𝐼) | ||
| Theorem | idlsubcl 37983 | An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐷𝐵) ∈ 𝐼) | ||
| Theorem | rngoidl 37984 | A ring 𝑅 is an 𝑅 ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → 𝑋 ∈ (Idl‘𝑅)) | ||
| Theorem | 0idl 37985 | The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅)) | ||
| Theorem | 1idl 37986 | Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑈 ∈ 𝐼 ↔ 𝐼 = 𝑋)) | ||
| Theorem | 0rngo 37987 | In a ring, 0 = 1 iff the ring contains only 0. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ RingOps → (𝑍 = 𝑈 ↔ 𝑋 = {𝑍})) | ||
| Theorem | divrngidl 37988 | The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ DivRingOps → (Idl‘𝑅) = {{𝑍}, 𝑋}) | ||
| Theorem | intidl 37989 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶 ∈ (Idl‘𝑅)) | ||
| Theorem | inidl 37990 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝐽 ∈ (Idl‘𝑅)) → (𝐼 ∩ 𝐽) ∈ (Idl‘𝑅)) | ||
| Theorem | unichnidl 37991* | The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅)) | ||
| Theorem | keridl 37992 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑆) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅)) | ||
| Theorem | pridlval 37993* | The class of prime ideals of a ring 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (PrIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Theorem | ispridl 37994* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃))))) | ||
| Theorem | pridlidl 37995 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ∈ (Idl‘𝑅)) | ||
| Theorem | pridlnr 37996 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ≠ 𝑋) | ||
| Theorem | pridl 37997* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (Idl‘𝑅) ∧ 𝐵 ∈ (Idl‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ∈ 𝑃)) → (𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃)) | ||
| Theorem | ispridl2 37998* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 38030 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅)) | ||
| Theorem | maxidlval 37999* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (MaxIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝑋)))}) | ||
| Theorem | ismaxidl 38000* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑀 ∈ (MaxIdl‘𝑅) ↔ (𝑀 ∈ (Idl‘𝑅) ∧ 𝑀 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝑋))))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |