Home | Metamath
Proof Explorer Theorem List (p. 193 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rlmsca2 19201 | Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ ( I ‘𝑅) = (Scalar‘(ringLMod‘𝑅)) | ||
Theorem | rlmvsca 19202 | Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (.r‘𝑅) = ( ·𝑠 ‘(ringLMod‘𝑅)) | ||
Theorem | rlmtopn 19203 | Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅)) | ||
Theorem | rlmds 19204 | Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (dist‘𝑅) = (dist‘(ringLMod‘𝑅)) | ||
Theorem | rlmlmod 19205 | The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.) |
⊢ (𝑅 ∈ Ring → (ringLMod‘𝑅) ∈ LMod) | ||
Theorem | rlmlvec 19206 | The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ DivRing → (ringLMod‘𝑅) ∈ LVec) | ||
Theorem | rlmvneg 19207 | Vector negation in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 5-Jun-2015.) |
⊢ (invg‘𝑅) = (invg‘(ringLMod‘𝑅)) | ||
Theorem | rlmscaf 19208 | Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (+𝑓‘(mulGrp‘𝑅)) = ( ·sf ‘(ringLMod‘𝑅)) | ||
Theorem | ixpsnbasval 19209* | The value of an infinite Cartesian product of the base of a left module over a ring with a singleton. (Contributed by AV, 3-Dec-2018.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅))}) | ||
Theorem | lidlss 19210 | An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐼 = (LIdeal‘𝑊) ⇒ ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵) | ||
Theorem | islidl 19211* | Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝐼 ∈ 𝑈 ↔ (𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐼 ((𝑥 · 𝑎) + 𝑏) ∈ 𝐼)) | ||
Theorem | lidl0cl 19212 | An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 0 ∈ 𝐼) | ||
Theorem | lidlacl 19213 | An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (𝑋 + 𝑌) ∈ 𝐼) | ||
Theorem | lidlnegcl 19214 | An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼) | ||
Theorem | lidlsubg 19215 | An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (SubGrp‘𝑅)) | ||
Theorem | lidlsubcl 19216 | An ideal is closed under subtraction. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ − = (-g‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (𝑋 − 𝑌) ∈ 𝐼) | ||
Theorem | lidlmcl 19217 | An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼)) → (𝑋 · 𝑌) ∈ 𝐼) | ||
Theorem | lidl1el 19218 | An ideal contains 1 iff it is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → ( 1 ∈ 𝐼 ↔ 𝐼 = 𝐵)) | ||
Theorem | lidl0 19219 | Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈) | ||
Theorem | lidl1 19220 | Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈) | ||
Theorem | lidlacs 19221 | The ideal system is an algebraic closure system on the base set. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐼 = (LIdeal‘𝑊) ⇒ ⊢ (𝑊 ∈ Ring → 𝐼 ∈ (ACS‘𝐵)) | ||
Theorem | rspcl 19222 | The span of a set of ring elements is an ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ 𝑈) | ||
Theorem | rspssid 19223 | The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) | ||
Theorem | rsp1 19224 | The span of the identity element is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐾‘{ 1 }) = 𝐵) | ||
Theorem | rsp0 19225 | The span of the zero element is the zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐾‘{ 0 }) = { 0 }) | ||
Theorem | rspssp 19226 | The ideal span of a set of elements in a ring is contained in any subring which contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ⊆ 𝐼) → (𝐾‘𝐺) ⊆ 𝐼) | ||
Theorem | mrcrsp 19227 | Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐹 = (mrCls‘𝑈) ⇒ ⊢ (𝑅 ∈ Ring → 𝐾 = 𝐹) | ||
Theorem | lidlnz 19228* | A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃𝑥 ∈ 𝐼 𝑥 ≠ 0 ) | ||
Theorem | drngnidl 19229 | A division ring has only the two trivial ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 𝑈 = {{ 0 }, 𝐵}) | ||
Theorem | lidlrsppropd 19230* | The left ideals and ring span of a ring depend only on the ring components. Here 𝑊 is expected to be either 𝐵 (when closure is available) or V (when strong equality is available). (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → ((LIdeal‘𝐾) = (LIdeal‘𝐿) ∧ (RSpan‘𝐾) = (RSpan‘𝐿))) | ||
Syntax | c2idl 19231 | Ring two-sided ideal function. |
class 2Ideal | ||
Definition | df-2idl 19232 | Define the class of two-sided ideals of a ring. A two-sided ideal is a left ideal which is also a right ideal (or a left ideal over the opposite ring). (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr‘𝑟)))) | ||
Theorem | 2idlval 19233 | Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐽 = (LIdeal‘𝑂) & ⊢ 𝑇 = (2Ideal‘𝑅) ⇒ ⊢ 𝑇 = (𝐼 ∩ 𝐽) | ||
Theorem | 2idlcpbl 19234 | The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝐸 = (𝑅 ~QG 𝑆) & ⊢ 𝐼 = (2Ideal‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷))) | ||
Theorem | qus1 19235 | The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆)) & ⊢ 𝐼 = (2Ideal‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → (𝑈 ∈ Ring ∧ [ 1 ](𝑅 ~QG 𝑆) = (1r‘𝑈))) | ||
Theorem | qusring 19236 | If 𝑆 is a two-sided ideal in 𝑅, then 𝑈 = 𝑅 / 𝑆 is a ring, called the quotient ring of 𝑅 by 𝑆. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆)) & ⊢ 𝐼 = (2Ideal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ Ring) | ||
Theorem | qusrhm 19237* | If 𝑆 is a two-sided ideal in 𝑅, then the "natural map" from elements to their cosets is a ring homomorphism from 𝑅 to 𝑅 / 𝑆. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆)) & ⊢ 𝐼 = (2Ideal‘𝑅) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝑅 ~QG 𝑆)) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑈)) | ||
Theorem | crngridl 19238 | In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐼 = (LIdeal‘𝑂)) | ||
Theorem | crng2idl 19239 | In a commutative ring, a two-sided ideal is the same as a left ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐼 = (2Ideal‘𝑅)) | ||
Theorem | quscrng 19240 | The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆)) & ⊢ 𝐼 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ CRing) | ||
Syntax | clpidl 19241 | Ring left-principal-ideal function. |
class LPIdeal | ||
Syntax | clpir 19242 | Class of left principal ideal rings. |
class LPIR | ||
Definition | df-lpidl 19243* | Define the class of left principal ideals of a ring, which are ideals with a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ LPIdeal = (𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})}) | ||
Definition | df-lpir 19244 | Define the class of left principal ideal rings, rings where every left ideal has a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ LPIR = {𝑤 ∈ Ring ∣ (LIdeal‘𝑤) = (LPIdeal‘𝑤)} | ||
Theorem | lpival 19245* | Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})}) | ||
Theorem | islpidl 19246* | Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔}))) | ||
Theorem | lpi0 19247 | The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃) | ||
Theorem | lpi1 19248 | The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃) | ||
Theorem | islpir 19249 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃)) | ||
Theorem | lpiss 19250 | Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈) | ||
Theorem | islpir2 19251 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃)) | ||
Theorem | lpirring 19252 | Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring) | ||
Theorem | drnglpir 19253 | Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR) | ||
Theorem | rspsn 19254* | Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → (𝐾‘{𝐺}) = {𝑥 ∣ 𝐺 ∥ 𝑥}) | ||
Theorem | lidldvgen 19255* | An element generates an ideal iff it is contained in the ideal and all elements are right-divided by it. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵) → (𝐼 = (𝐾‘{𝐺}) ↔ (𝐺 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 𝐺 ∥ 𝑥))) | ||
Theorem | lpigen 19256* | An ideal is principal iff it contains an element which right-divides all elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝑃 = (LPIdeal‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐼 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 𝑥 ∥ 𝑦)) | ||
Syntax | cnzr 19257 | The class of nonzero rings. |
class NzRing | ||
Definition | df-nzr 19258 | A nonzero or nontrivial ring is a ring with at least two values, or equivalently where 1 and 0 are different. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)} | ||
Theorem | isnzr 19259 | Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 ≠ 0 )) | ||
Theorem | nzrnz 19260 | One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 1 ≠ 0 ) | ||
Theorem | nzrring 19261 | A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) | ||
Theorem | drngnzr 19262 | All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) | ||
Theorem | isnzr2 19263 | Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 2𝑜 ≼ 𝐵)) | ||
Theorem | isnzr2hash 19264 | Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 19263. (Contributed by AV, 14-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 < (#‘𝐵))) | ||
Theorem | opprnzr 19265 | The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑂 ∈ NzRing) | ||
Theorem | ringelnzr 19266 | A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 13-Jun-2015.) |
⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ∖ { 0 })) → 𝑅 ∈ NzRing) | ||
Theorem | nzrunit 19267 | A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ 0 ) | ||
Theorem | subrgnzr 19268 | A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ NzRing) | ||
Theorem | 0ringnnzr 19269 | A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019.) |
⊢ (𝑅 ∈ Ring → ((#‘(Base‘𝑅)) = 1 ↔ ¬ 𝑅 ∈ NzRing)) | ||
Theorem | 0ring 19270 | If a ring has only one element, it is the zero ring. According to Wikipedia ("Zero ring", 14-Apr-2019, https://en.wikipedia.org/wiki/Zero_ring): "The zero ring, denoted {0} or simply 0, consists of the one-element set {0} with the operations + and * defined so that 0 + 0 = 0 and 0 * 0 = 0.". (Contributed by AV, 14-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (#‘𝐵) = 1) → 𝐵 = { 0 }) | ||
Theorem | 0ring01eq 19271 | In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (#‘𝐵) = 1) → 0 = 1 ) | ||
Theorem | 01eq0ring 19272 | If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 }) | ||
Theorem | 0ring01eqbi 19273 | In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by AV, 23-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐵 ≈ 1𝑜 ↔ 1 = 0 )) | ||
Theorem | rng1nnzr 19274 | The (smallest) structure representing a zero ring is not a nonzero ring. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉, 〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ⇒ ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ NzRing) | ||
Theorem | ring1zr 19275 | The only (unital) ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 7-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ∗ = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {〈〈𝑍, 𝑍〉, 𝑍〉} ∧ ∗ = {〈〈𝑍, 𝑍〉, 𝑍〉}))) | ||
Theorem | rngen1zr 19276 | The only (unital) ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ∗ = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 ≈ 1𝑜 ↔ ( + = {〈〈𝑍, 𝑍〉, 𝑍〉} ∧ ∗ = {〈〈𝑍, 𝑍〉, 𝑍〉}))) | ||
Theorem | ringen1zr 19277 | The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑍 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1𝑜 ↔ ( + = {〈〈𝑍, 𝑍〉, 𝑍〉} ∧ ∗ = {〈〈𝑍, 𝑍〉, 𝑍〉}))) | ||
Theorem | rng1nfld 19278 | The zero ring is not a field. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉, 〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ⇒ ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ Field) | ||
Syntax | crlreg 19279 | Set of left-regular elements in a ring. |
class RLReg | ||
Syntax | cdomn 19280 | Class of (ring theoretic) domains. |
class Domn | ||
Syntax | cidom 19281 | Class of integral domains. |
class IDomn | ||
Syntax | cpid 19282 | Class of principal ideal domains. |
class PID | ||
Definition | df-rlreg 19283* | Define the set of left-regular elements in a ring as those elements which are not left zero divisors, meaning that multiplying a nonzero element on the left by a left-regular element gives a nonzero product. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ RLReg = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))}) | ||
Definition | df-domn 19284* | A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))} | ||
Definition | df-idom 19285 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ IDomn = (CRing ∩ Domn) | ||
Definition | df-pid 19286 | A principal ideal domain is an integral domain satisfying the left principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ PID = (IDomn ∩ LPIR) | ||
Theorem | rrgval 19287* | Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} | ||
Theorem | isrrg 19288* | Membership in the set of left-regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((𝑋 · 𝑦) = 0 → 𝑦 = 0 ))) | ||
Theorem | rrgeq0i 19289 | Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 )) | ||
Theorem | rrgeq0 19290 | Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 ↔ 𝑌 = 0 )) | ||
Theorem | rrgsupp 19291 | Left multiplication by a left regular element does not change the support set of a vector. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Revised by AV, 20-Jul-2019.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌:𝐼⟶𝐵) ⇒ ⊢ (𝜑 → (((𝐼 × {𝑋}) ∘𝑓 · 𝑌) supp 0 ) = (𝑌 supp 0 )) | ||
Theorem | rrgss 19292 | Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐸 ⊆ 𝐵 | ||
Theorem | unitrrg 19293 | Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸) | ||
Theorem | isdomn 19294* | Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) | ||
Theorem | domnnzr 19295 | A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | ||
Theorem | domnring 19296 | A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) | ||
Theorem | domneq0 19297 | In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 ))) | ||
Theorem | domnmuln0 19298 | In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝑋 · 𝑌) ≠ 0 ) | ||
Theorem | isdomn2 19299 | A ring is a domain iff all nonzero elements are nonzero-divisors. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) ⊆ 𝐸)) | ||
Theorem | domnrrg 19300 | In a domain, any nonzero element is a nonzero-divisor. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐸) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |