![]() |
Metamath
Proof Explorer Theorem List (p. 344 of 435) | < 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-28326) |
![]() (28327-29851) |
![]() (29852-43457) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isrngohom 34301* | 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) → (𝐹 ∈ (𝑅 RngHom 𝑆) ↔ (𝐹:𝑋⟶𝑌 ∧ (𝐹‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦)))))) | ||
Theorem | rngohomf 34302 | A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:𝑋⟶𝑌) | ||
Theorem | rngohomcl 34303 | Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ 𝑌) | ||
Theorem | rngohom1 34304 | A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.) |
⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) & ⊢ 𝐾 = (2nd ‘𝑆) & ⊢ 𝑉 = (GId‘𝐾) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘𝑈) = 𝑉) | ||
Theorem | rngohomadd 34305 | Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐺𝐵)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵))) | ||
Theorem | rngohommul 34306 | Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝐾 = (2nd ‘𝑆) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵))) | ||
Theorem | rngogrphom 34307 | A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐽 = (1st ‘𝑆) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹 ∈ (𝐺 GrpOpHom 𝐽)) | ||
Theorem | rngohom0 34308 | A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑊 = (GId‘𝐽) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘𝑍) = 𝑊) | ||
Theorem | rngohomsub 34309 | Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐻 = ( /𝑔 ‘𝐺) & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝐾 = ( /𝑔 ‘𝐽) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵))) | ||
Theorem | rngohomco 34310 | The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RngHom 𝑇)) | ||
Theorem | rngokerinj 34311 | 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 ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹:𝑋–1-1→𝑌 ↔ (◡𝐹 “ {𝑍}) = {𝑊})) | ||
Definition | df-rngoiso 34312* | Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ RngIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st ‘𝑟)–1-1-onto→ran (1st ‘𝑠)}) | ||
Theorem | rngoisoval 34313* | The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RngIso 𝑆) = {𝑓 ∈ (𝑅 RngHom 𝑆) ∣ 𝑓:𝑋–1-1-onto→𝑌}) | ||
Theorem | isrngoiso 34314 | The predicate "is a ring isomorphism between 𝑅 and 𝑆". (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RngIso 𝑆) ↔ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:𝑋–1-1-onto→𝑌))) | ||
Theorem | rngoiso1o 34315 | A ring isomorphism is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngIso 𝑆)) → 𝐹:𝑋–1-1-onto→𝑌) | ||
Theorem | rngoisohom 34316 | A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngIso 𝑆)) → 𝐹 ∈ (𝑅 RngHom 𝑆)) | ||
Theorem | rngoisocnv 34317 | The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngIso 𝑆)) → ◡𝐹 ∈ (𝑆 RngIso 𝑅)) | ||
Theorem | rngoisoco 34318 | The composition of two ring isomorphisms is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngIso 𝑆) ∧ 𝐺 ∈ (𝑆 RngIso 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RngIso 𝑇)) | ||
Definition | df-risc 34319* | Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ≃𝑟 = {〈𝑟, 𝑠〉 ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))} | ||
Theorem | isriscg 34320* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RngIso 𝑆)))) | ||
Theorem | isrisc 34321* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝑅 ∈ V & ⊢ 𝑆 ∈ V ⇒ ⊢ (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RngIso 𝑆))) | ||
Theorem | risc 34322* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 ≃𝑟 𝑆 ↔ ∃𝑓 𝑓 ∈ (𝑅 RngIso 𝑆))) | ||
Theorem | risci 34323 | Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngIso 𝑆)) → 𝑅 ≃𝑟 𝑆) | ||
Theorem | riscer 34324 | Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ≃𝑟 Er dom ≃𝑟 | ||
Syntax | ccm2 34325 | Extend class notation with a class that adds commutativity to various flavors of rings. |
class Com2 | ||
Definition | df-com2 34326* | 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 34327 | Extend class notation with the class of all fields. |
class Fld | ||
Definition | df-fld 34328 | 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 34329 | Extend class notation with the class of commutative rings. |
class CRingOps | ||
Definition | df-crngo 34330 | Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.) |
⊢ CRingOps = (RingOps ∩ Com2) | ||
Theorem | iscom2 34331* | 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 34332 | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2)) | ||
Theorem | iscrngo2 34333* | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) | ||
Theorem | iscringd 34334* | 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 34335 | 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 34336 | A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps) | ||
Theorem | crngocom 34337 | The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) = (𝐵𝐻𝐴)) | ||
Theorem | crngm23 34338 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐻𝐵)) | ||
Theorem | crngm4 34339 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻(𝐶𝐻𝐷)) = ((𝐴𝐻𝐶)𝐻(𝐵𝐻𝐷))) | ||
Theorem | fldcrng 34340 | A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) |
⊢ (𝐾 ∈ Fld → 𝐾 ∈ CRingOps) | ||
Theorem | isfld2 34341 | The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps)) | ||
Theorem | crngohomfo 34342 | The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐽 = (1st ‘𝑆) & ⊢ 𝑌 = ran 𝐽 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:𝑋–onto→𝑌)) → 𝑆 ∈ CRingOps) | ||
Syntax | cidl 34343 | Extend class notation with the class of ideals. |
class Idl | ||
Syntax | cpridl 34344 | Extend class notation with the class of prime ideals. |
class PrIdl | ||
Syntax | cmaxidl 34345 | Extend class notation with the class of maximal ideals. |
class MaxIdl | ||
Definition | df-idl 34346* | 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 34347* | 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 34374 and ispridlc 34406. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
Definition | df-maxidl 34348* | 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 34349* | The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → (Idl‘𝑅) = {𝑖 ∈ 𝒫 𝑋 ∣ (𝑍 ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥𝐺𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝑖 ∧ (𝑥𝐻𝑧) ∈ 𝑖)))}) | ||
Theorem | isidl 34350* | The predicate "is an ideal of the ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼))))) | ||
Theorem | isidlc 34351* | The predicate "is an ideal of the commutative ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ CRingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 (𝑧𝐻𝑥) ∈ 𝐼)))) | ||
Theorem | idlss 34352 | An ideal of 𝑅 is a subset of 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝐼 ⊆ 𝑋) | ||
Theorem | idlcl 34353 | An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ 𝑋) | ||
Theorem | idl0cl 34354 | An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝑍 ∈ 𝐼) | ||
Theorem | idladdcl 34355 | An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐺𝐵) ∈ 𝐼) | ||
Theorem | idllmulcl 34356 | An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐵𝐻𝐴) ∈ 𝐼) | ||
Theorem | idlrmulcl 34357 | An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐻𝐵) ∈ 𝐼) | ||
Theorem | idlnegcl 34358 | An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → (𝑁‘𝐴) ∈ 𝐼) | ||
Theorem | idlsubcl 34359 | An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐷𝐵) ∈ 𝐼) | ||
Theorem | rngoidl 34360 | A ring 𝑅 is an 𝑅 ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → 𝑋 ∈ (Idl‘𝑅)) | ||
Theorem | 0idl 34361 | The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅)) | ||
Theorem | 1idl 34362 | Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑈 ∈ 𝐼 ↔ 𝐼 = 𝑋)) | ||
Theorem | 0rngo 34363 | 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 34364 | 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 34365 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶 ∈ (Idl‘𝑅)) | ||
Theorem | inidl 34366 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝐽 ∈ (Idl‘𝑅)) → (𝐼 ∩ 𝐽) ∈ (Idl‘𝑅)) | ||
Theorem | unichnidl 34367* | The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅)) | ||
Theorem | keridl 34368 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑆) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅)) | ||
Theorem | pridlval 34369* | 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 34370* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃))))) | ||
Theorem | pridlidl 34371 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ∈ (Idl‘𝑅)) | ||
Theorem | pridlnr 34372 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ≠ 𝑋) | ||
Theorem | pridl 34373* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (Idl‘𝑅) ∧ 𝐵 ∈ (Idl‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ∈ 𝑃)) → (𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃)) | ||
Theorem | ispridl2 34374* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 34406 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅)) | ||
Theorem | maxidlval 34375* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (MaxIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝑋)))}) | ||
Theorem | ismaxidl 34376* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑀 ∈ (MaxIdl‘𝑅) ↔ (𝑀 ∈ (Idl‘𝑅) ∧ 𝑀 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝑋))))) | ||
Theorem | maxidlidl 34377 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ∈ (Idl‘𝑅)) | ||
Theorem | maxidlnr 34378 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ≠ 𝑋) | ||
Theorem | maxidlmax 34379 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) ∧ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝑋)) | ||
Theorem | maxidln1 34380 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → ¬ 𝑈 ∈ 𝑀) | ||
Theorem | maxidln0 34381 | A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑈 ≠ 𝑍) | ||
Syntax | cprrng 34382 | Extend class notation with the class of prime rings. |
class PrRing | ||
Syntax | cdmn 34383 | Extend class notation with the class of domains. |
class Dmn | ||
Definition | df-prrngo 34384 | Define the class of prime rings. A ring is prime if the zero ideal is a prime ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ PrRing = {𝑟 ∈ RingOps ∣ {(GId‘(1st ‘𝑟))} ∈ (PrIdl‘𝑟)} | ||
Definition | df-dmn 34385 | Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ Dmn = (PrRing ∩ Com2) | ||
Theorem | isprrngo 34386 | The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅))) | ||
Theorem | prrngorngo 34387 | A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ PrRing → 𝑅 ∈ RingOps) | ||
Theorem | smprngopr 34388 | A simple ring (one whose only ideals are 0 and 𝑅) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing) | ||
Theorem | divrngpr 34389 | A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ (𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing) | ||
Theorem | isdmn 34390 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2)) | ||
Theorem | isdmn2 34391 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps)) | ||
Theorem | dmncrng 34392 | A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ CRingOps) | ||
Theorem | dmnrngo 34393 | A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps) | ||
Theorem | flddmn 34394 | A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝐾 ∈ Fld → 𝐾 ∈ Dmn) | ||
Syntax | cigen 34395 | Extend class notation with the ideal generation function. |
class IdlGen | ||
Definition | df-igen 34396* | Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}) | ||
Theorem | igenval 34397* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof shortened by Mario Carneiro, 20-Dec-2013.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗}) | ||
Theorem | igenss 34398 | A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑅 IdlGen 𝑆)) | ||
Theorem | igenidl 34399 | The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) ∈ (Idl‘𝑅)) | ||
Theorem | igenmin 34400 | The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼) → (𝑅 IdlGen 𝑆) ⊆ 𝐼) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |