![]() |
Metamath
Proof Explorer Theorem List (p. 192 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43661) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | crh 19101 | Extend class notation with the ring homomorphisms. |
class RingHom | ||
Syntax | crs 19102 | Extend class notation with the ring isomorphisms. |
class RingIso | ||
Syntax | cric 19103 | Extend class notation with the ring isomorphism relation. |
class ≃𝑟 | ||
Definition | df-rnghom 19104* | Define the set of ring homomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}) | ||
Definition | df-rngiso 19105* | Define the set of ring isomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)}) | ||
Theorem | dfrhm2 19106* | The property of a ring homomorphism can be decomposed into separate homomorphic conditions for addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ((𝑟 GrpHom 𝑠) ∩ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠)))) | ||
Definition | df-ric 19107 | Define the ring isomorphism relation, analogous to df-gic 18086: Two (unital) rings are said to be isomorphic iff they are connected by at least one isomorphism. Isomorphic rings share all global ring properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by AV, 24-Dec-2019.) |
⊢ ≃𝑟 = (◡ RingIso “ (V ∖ 1o)) | ||
Theorem | rhmrcl1 19108 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) | ||
Theorem | rhmrcl2 19109 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring) | ||
Theorem | isrhm 19110 | A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) ↔ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ (𝑀 MndHom 𝑁)))) | ||
Theorem | rhmmhm 19111 | A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑀 MndHom 𝑁)) | ||
Theorem | isrim0 19112 | An isomorphism of rings is a homomorphism whose converse is also a homomorphism . (Contributed by AV, 22-Oct-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RingHom 𝑅)))) | ||
Theorem | rimrcl 19113 | Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019.) |
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V)) | ||
Theorem | rhmghm 19114 | A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | ||
Theorem | rhmf 19115 | A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐵⟶𝐶) | ||
Theorem | rhmmul 19116 | A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵))) | ||
Theorem | isrhm2d 19117* | Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (1r‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑆 ∈ Ring) & ⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) | ||
Theorem | isrhmd 19118* | Demonstration of ring homomorphism. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (1r‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑆 ∈ Ring) & ⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ⨣ = (+g‘𝑆) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) | ||
Theorem | rhm1 19119 | Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (1r‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘ 1 ) = 𝑁) | ||
Theorem | idrhm 19120 | The identity homomorphism on a ring. (Contributed by AV, 14-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → ( I ↾ 𝐵) ∈ (𝑅 RingHom 𝑅)) | ||
Theorem | rhmf1o 19121 | A ring homomorphism is bijective iff its converse is also a ring homomorphism. (Contributed by AV, 22-Oct-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 RingHom 𝑅))) | ||
Theorem | isrim 19122 | An isomorphism of rings is a bijective homomorphism. (Contributed by AV, 22-Oct-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶))) | ||
Theorem | rimf1o 19123 | An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Theorem | rimrhm 19124 | An isomorphism of rings is a homomorphism. (Contributed by AV, 22-Oct-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | ||
Theorem | rimgim 19125 | An isomorphism of rings is an isomorphism of their additive groups. (Contributed by AV, 24-Dec-2019.) |
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 GrpIso 𝑆)) | ||
Theorem | rhmco 19126 | The composition of ring homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ ((𝐹 ∈ (𝑇 RingHom 𝑈) ∧ 𝐺 ∈ (𝑆 RingHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RingHom 𝑈)) | ||
Theorem | pwsco1rhm 19127* | Right composition with a function on the index sets yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐴) & ⊢ 𝑍 = (𝑅 ↑s 𝐵) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 RingHom 𝑌)) | ||
Theorem | pwsco2rhm 19128* | Left composition with a ring homomorphism yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐴) & ⊢ 𝑍 = (𝑆 ↑s 𝐴) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) ⇒ ⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 RingHom 𝑍)) | ||
Theorem | f1ghm0to0 19129 | If a group homomorphism 𝐹 is injective, it maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.) |
⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑁 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑁 ↔ 𝑋 = 0 )) | ||
Theorem | f1rhm0to0OLD 19130 | Obsolete version of f1ghm0to0 19129 as of 13-May-2023. (Contributed by AV, 24-Oct-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑁 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑁 ↔ 𝑋 = 0 )) | ||
Theorem | f1rhm0to0ALT 19131 | Alternate proof for f1ghm0to0 19129. Using ghmf1 18073 does not make the proof shorter and requires disjoint variable restrictions! (Contributed by AV, 24-Oct-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑁 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑁 ↔ 𝑋 = 0 )) | ||
Theorem | gim0to0 19132 | A group isomorphism maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 23-May-2023.) |
⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑁 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑁 ↔ 𝑋 = 0 )) | ||
Theorem | rim0to0OLD 19133 | Obsolete version of gim0to0 19132 as of 13-May-2023. (Contributed by AV, 24-Oct-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑁 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingIso 𝑆) ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑁 ↔ 𝑋 = 0 )) | ||
Theorem | kerf1ghm 19134 | A group homomorphism 𝐹 is injective if and only if its kernel is the singleton {𝑁}. (Contributed by Thierry Arnoux, 27-Oct-2017.) (Proof shortened by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.) |
⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑁 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹:𝐴–1-1→𝐵 ↔ (◡𝐹 “ { 0 }) = {𝑁})) | ||
Theorem | kerf1hrmOLD 19135 | Obsolete version of kerf1ghm 19134 as of 13-May-2023. (Contributed by Thierry Arnoux, 27-Oct-2017.) (Proof shortened by AV, 24-Oct-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑁 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹:𝐴–1-1→𝐵 ↔ (◡𝐹 “ { 0 }) = {𝑁})) | ||
Theorem | brric 19136 | The relation "is isomorphic to" for (unital) rings. (Contributed by AV, 24-Dec-2019.) |
⊢ (𝑅 ≃𝑟 𝑆 ↔ (𝑅 RingIso 𝑆) ≠ ∅) | ||
Theorem | brric2 19137* | The relation "is isomorphic to" for (unital) rings. This theorem corresponds to the definition df-risc 34408 of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019.) |
⊢ (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingIso 𝑆))) | ||
Theorem | ricgic 19138 | If two rings are (ring) isomorphic, their additive groups are (group) isomorphic. (Contributed by AV, 24-Dec-2019.) |
⊢ (𝑅 ≃𝑟 𝑆 → 𝑅 ≃𝑔 𝑆) | ||
Syntax | cdr 19139 | Extend class notation with class of all division rings. |
class DivRing | ||
Syntax | cfield 19140 | Class of fields. |
class Field | ||
Definition | df-drng 19141 | Define class of all division rings. A division ring is a ring in which the set of units is exactly the nonzero elements of the ring. (Contributed by NM, 18-Oct-2012.) |
⊢ DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)})} | ||
Definition | df-field 19142 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ Field = (DivRing ∩ CRing) | ||
Theorem | isdrng 19143 | The predicate "is a division ring". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 }))) | ||
Theorem | drngunit 19144 | Elementhood in the set of units when 𝑅 is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ))) | ||
Theorem | drngui 19145 | The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑅 ∈ DivRing ⇒ ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅) | ||
Theorem | drngring 19146 | A division ring is a ring. (Contributed by NM, 8-Sep-2011.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) | ||
Theorem | drnggrp 19147 | A division ring is a group. (Contributed by NM, 8-Sep-2011.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Grp) | ||
Theorem | isfld 19148 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) | ||
Theorem | isdrng2 19149 | A division ring can equivalently be defined as a ring such that the nonzero elements form a group under multiplication (from which it follows that this is the same group as the group of units). (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ⇒ ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ Grp)) | ||
Theorem | drngprop 19150 | If two structures have the same ring components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Mario Carneiro, 28-Dec-2014.) |
⊢ (Base‘𝐾) = (Base‘𝐿) & ⊢ (+g‘𝐾) = (+g‘𝐿) & ⊢ (.r‘𝐾) = (.r‘𝐿) ⇒ ⊢ (𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing) | ||
Theorem | drngmgp 19151 | A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ⇒ ⊢ (𝑅 ∈ DivRing → 𝐺 ∈ Grp) | ||
Theorem | drngmcl 19152 | The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ (𝐵 ∖ { 0 }) ∧ 𝑌 ∈ (𝐵 ∖ { 0 })) → (𝑋 · 𝑌) ∈ (𝐵 ∖ { 0 })) | ||
Theorem | drngid 19153 | A division ring's unit is the identity element of its multiplicative group. (Contributed by NM, 7-Sep-2011.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ⇒ ⊢ (𝑅 ∈ DivRing → 1 = (0g‘𝐺)) | ||
Theorem | drngunz 19154 | A division ring's unit is different from its zero. (Contributed by NM, 8-Sep-2011.) |
⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 1 ≠ 0 ) | ||
Theorem | drngid2 19155 | Properties showing that an element 𝐼 is the identity element of a division ring. (Contributed by Mario Carneiro, 11-Oct-2013.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → ((𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ∧ (𝐼 · 𝐼) = 𝐼) ↔ 1 = 𝐼)) | ||
Theorem | drnginvrcl 19156 | Closure of the multiplicative inverse in a division ring. (reccl 11040 analog.) (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐵) | ||
Theorem | drnginvrn0 19157 | The multiplicative inverse in a division ring is nonzero. (recne0 11046 analog.) (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ≠ 0 ) | ||
Theorem | drnginvrl 19158 | Property of the multiplicative inverse in a division ring. (recid2 11048 analog.) (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ((𝐼‘𝑋) · 𝑋) = 1 ) | ||
Theorem | drnginvrr 19159 | Property of the multiplicative inverse in a division ring. (recid 11047 analog.) (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑋 · (𝐼‘𝑋)) = 1 ) | ||
Theorem | drngmul0or 19160 | A product is zero iff one of its factors is zero. (Contributed by NM, 8-Oct-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 ))) | ||
Theorem | drngmulne0 19161 | A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) ≠ 0 ↔ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ))) | ||
Theorem | drngmuleq0 19162 | An element is zero iff its product with a nonzero element is zero. (Contributed by NM, 8-Oct-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑋 = 0 )) | ||
Theorem | opprdrng 19163 | The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing ↔ 𝑂 ∈ DivRing) | ||
Theorem | isdrngd 19164* | Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element 𝑥 should have a left-inverse 𝐼(𝑥). See isdrngd 19164 for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 0 = (0g‘𝑅)) & ⊢ (𝜑 → 1 = (1r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) & ⊢ (𝜑 → 1 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 ) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | isdrngrd 19165* | Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element 𝑥 should have a right-inverse 𝐼(𝑥). See isdrngd 19164 for the characterization using left-inverses. (Contributed by NM, 10-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 0 = (0g‘𝑅)) & ⊢ (𝜑 → 1 = (1r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) & ⊢ (𝜑 → 1 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝑥 · 𝐼) = 1 ) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | drngpropd 19166* | If two structures have the same group components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing)) | ||
Theorem | fldpropd 19167* | If two structures have the same group components (properties), one is a field iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Field ↔ 𝐿 ∈ Field)) | ||
Syntax | csubrg 19168 | Extend class notation with all subrings of a ring. |
class SubRing | ||
Syntax | crgspn 19169 | Extend class notation with span of a set of elements over a ring. |
class RingSpan | ||
Definition | df-subrg 19170* |
Define a subring of a ring as a set of elements that is a ring in its
own right and contains the multiplicative identity.
The additional constraint is necessary because the multiplicative identity of a ring, unlike the additive identity of a ring/group or the multiplicative identity of a field, cannot be identified by a local property. Thus, it is possible for a subset of a ring to be a ring while not containing the true identity if it contains a false identity. For instance, the subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity 〈1, 0〉 which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ SubRing = (𝑤 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ((𝑤 ↾s 𝑠) ∈ Ring ∧ (1r‘𝑤) ∈ 𝑠)}) | ||
Definition | df-rgspn 19171* | The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡})) | ||
Theorem | issubrg 19172 | The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof shortened by AV, 12-Oct-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) | ||
Theorem | subrgss 19173 | A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵) | ||
Theorem | subrgid 19174 | Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅)) | ||
Theorem | subrgring 19175 | A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) | ||
Theorem | subrgcrng 19176 | A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ CRing) | ||
Theorem | subrgrcl 19177 | Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | ||
Theorem | subrgsubg 19178 | A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) | ||
Theorem | subrg0 19179 | A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 0 = (0g‘𝑆)) | ||
Theorem | subrg1cl 19180 | A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴) | ||
Theorem | subrgbas 19181 | Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) | ||
Theorem | subrg1 19182 | A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 = (1r‘𝑆)) | ||
Theorem | subrgacl 19183 | A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴) | ||
Theorem | subrgmcl 19184 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴) | ||
Theorem | subrgsubm 19185 | A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubMnd‘𝑀)) | ||
Theorem | subrgdvds 19186 | If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝐸 = (∥r‘𝑆) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐸 ⊆ ∥ ) | ||
Theorem | subrguss 19187 | A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ⊆ 𝑈) | ||
Theorem | subrginv 19188 | A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝐽 = (invr‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = (𝐽‘𝑋)) | ||
Theorem | subrgdv 19189 | A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ / = (/r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝐸 = (/r‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋𝐸𝑌)) | ||
Theorem | subrgunit 19190 | An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ (𝐼‘𝑋) ∈ 𝐴))) | ||
Theorem | subrgugrp 19191 | The units of a subring form a subgroup of the unit group of the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ∈ (SubGrp‘𝐺)) | ||
Theorem | issubrg2 19192* | Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴))) | ||
Theorem | opprsubrg 19193 | Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (SubRing‘𝑅) = (SubRing‘𝑂) | ||
Theorem | subrgint 19194 | The intersection of a nonempty collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubRing‘𝑅)) | ||
Theorem | subrgin 19195 | The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRing‘𝑅)) | ||
Theorem | subrgmre 19196 | The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (Moore‘𝐵)) | ||
Theorem | issubdrg 19197* | Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → (𝑆 ∈ DivRing ↔ ∀𝑥 ∈ (𝐴 ∖ { 0 })(𝐼‘𝑥) ∈ 𝐴)) | ||
Theorem | subsubrg 19198 | A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴))) | ||
Theorem | subsubrg2 19199 | The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (SubRing‘𝑆) = ((SubRing‘𝑅) ∩ 𝒫 𝐴)) | ||
Theorem | issubrg3 19200 | A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ 𝑆 ∈ (SubMnd‘𝑀)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |