![]() |
Metamath
Proof Explorer Theorem List (p. 205 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rhmopp 20401 | A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
β’ (πΉ β (π RingHom π) β πΉ β ((opprβπ ) RingHom (opprβπ))) | ||
Theorem | elrhmunit 20402 | Ring homomorphisms preserve unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
β’ ((πΉ β (π RingHom π) β§ π΄ β (Unitβπ )) β (πΉβπ΄) β (Unitβπ)) | ||
Theorem | rhmunitinv 20403 | Ring homomorphisms preserve the inverse of unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
β’ ((πΉ β (π RingHom π) β§ π΄ β (Unitβπ )) β (πΉβ((invrβπ )βπ΄)) = ((invrβπ)β(πΉβπ΄))) | ||
Syntax | cnzr 20404 | The class of nonzero rings. |
class NzRing | ||
Definition | df-nzr 20405 | 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 20406 | Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ (π β NzRing β (π β Ring β§ 1 β 0 )) | ||
Theorem | nzrnz 20407 | 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 20408 | A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.) |
β’ (π β NzRing β π β Ring) | ||
Theorem | nzrringOLD 20409 | Obsolete version of nzrring 20408 as of 23-Feb-2025. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β NzRing β π β Ring) | ||
Theorem | isnzr2 20410 | Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β NzRing β (π β Ring β§ 2o βΌ π΅)) | ||
Theorem | isnzr2hash 20411 | Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 20410. (Contributed by AV, 14-Apr-2019.) |
β’ π΅ = (Baseβπ ) β β’ (π β NzRing β (π β Ring β§ 1 < (β―βπ΅))) | ||
Theorem | opprnzr 20412 | The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ π = (opprβπ ) β β’ (π β NzRing β π β NzRing) | ||
Theorem | ringelnzr 20413 | 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 20414 | A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) β β’ ((π β NzRing β§ π΄ β π) β π΄ β 0 ) | ||
Theorem | 0ringnnzr 20415 | 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 20416 | 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 | 0ringdif 20417 | A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (π β (Ring β NzRing) β (π β Ring β§ π΅ = { 0 })) | ||
Theorem | 0ringbas 20418 | The base set of a zero ring, a ring which is not a nonzero ring, is the singleton of the zero element. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (π β (Ring β NzRing) β π΅ = { 0 }) | ||
Theorem | 0ring01eq 20419 | 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 20420 | 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.) (Proof shortened by SN, 23-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ 0 = 1 ) β π΅ = { 0 }) | ||
Theorem | 01eq0ringOLD 20421 | Obsolete version of 01eq0ring 20420 as of 23-Feb-2025. (Contributed by AV, 16-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ 0 = 1 ) β π΅ = { 0 }) | ||
Theorem | 0ring01eqbi 20422 | 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 β (π΅ β 1o β 1 = 0 )) | ||
Theorem | 0ring1eq0 20423 | In a zero ring, a ring which is not a nonzero ring, the ring unity equals the zero element. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ (π β (Ring β NzRing) β 1 = 0 ) | ||
Theorem | c0rhm 20424* | The constant mapping to zero is a ring homomorphism from any ring to the zero ring. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π₯ β π΅ β¦ 0 ) β β’ ((π β Ring β§ π β (Ring β NzRing)) β π» β (π RingHom π)) | ||
Theorem | c0rnghm 20425* | The constant mapping to zero is a non-unital ring homomorphism from any non-unital ring to the zero ring. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π₯ β π΅ β¦ 0 ) β β’ ((π β Rng β§ π β (Ring β NzRing)) β π» β (π RngHom π)) | ||
Theorem | zrrnghm 20426* | The constant mapping to zero is a non-unital ring homomorphism from the zero ring to any non-unital ring. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π₯ β π΅ β¦ 0 ) β β’ ((π β Rng β§ π β (Ring β NzRing)) β π» β (π RngHom π)) | ||
Syntax | clring 20427 | Extend class notation with class of all local rings. |
class LRing | ||
Definition | df-lring 20428* | A local ring is a nonzero ring where for any two elements summing to one, at least one is invertible. Any field is a local ring; the ring of integers is an example of a ring which is not a local ring. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
β’ LRing = {π β NzRing β£ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = (1rβπ) β (π₯ β (Unitβπ) β¨ π¦ β (Unitβπ)))} | ||
Theorem | islring 20429* | The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ 1 = (1rβπ ) & β’ π = (Unitβπ ) β β’ (π β LRing β (π β NzRing β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ + π¦) = 1 β (π₯ β π β¨ π¦ β π)))) | ||
Theorem | lringnzr 20430 | A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.) |
β’ (π β LRing β π β NzRing) | ||
Theorem | lringring 20431 | A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
β’ (π β LRing β π β Ring) | ||
Theorem | lringnz 20432 | A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ (π β LRing β 1 β 0 ) | ||
Theorem | lringuplu 20433 | If the sum of two elements of a local ring is invertible, then at least one of the summands must be invertible. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β π = (Unitβπ )) & β’ (π β + = (+gβπ )) & β’ (π β π β LRing) & β’ (π β (π + π) β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β π β¨ π β π)) | ||
Syntax | csubrng 20434 | Extend class notation with all subrings of a non-unital ring. |
class SubRng | ||
Definition | df-subrng 20435* | Define a subring of a non-unital ring as a set of elements that is a non-unital ring in its own right. In this section, a subring of a non-unital ring is simply called "subring", unless it causes any ambiguity with SubRing. (Contributed by AV, 14-Feb-2025.) |
β’ SubRng = (π€ β Rng β¦ {π β π« (Baseβπ€) β£ (π€ βΎs π ) β Rng}) | ||
Theorem | issubrng 20436 | The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.) |
β’ π΅ = (Baseβπ ) β β’ (π΄ β (SubRngβπ ) β (π β Rng β§ (π βΎs π΄) β Rng β§ π΄ β π΅)) | ||
Theorem | subrngss 20437 | A subring is a subset. (Contributed by AV, 14-Feb-2025.) |
β’ π΅ = (Baseβπ ) β β’ (π΄ β (SubRngβπ ) β π΄ β π΅) | ||
Theorem | subrngid 20438 | Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.) |
β’ π΅ = (Baseβπ ) β β’ (π β Rng β π΅ β (SubRngβπ )) | ||
Theorem | subrngrng 20439 | A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRngβπ ) β π β Rng) | ||
Theorem | subrngrcl 20440 | Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.) |
β’ (π΄ β (SubRngβπ ) β π β Rng) | ||
Theorem | subrngsubg 20441 | A subring is a subgroup. (Contributed by AV, 14-Feb-2025.) |
β’ (π΄ β (SubRngβπ ) β π΄ β (SubGrpβπ )) | ||
Theorem | subrngringnsg 20442 | A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.) |
β’ (π΄ β (SubRngβπ ) β π΄ β (NrmSGrpβπ )) | ||
Theorem | subrngbas 20443 | Base set of a subring structure. (Contributed by AV, 14-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRngβπ ) β π΄ = (Baseβπ)) | ||
Theorem | subrng0 20444 | A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.) |
β’ π = (π βΎs π΄) & β’ 0 = (0gβπ ) β β’ (π΄ β (SubRngβπ ) β 0 = (0gβπ)) | ||
Theorem | subrngacl 20445 | A subring is closed under addition. (Contributed by AV, 14-Feb-2025.) |
β’ + = (+gβπ ) β β’ ((π΄ β (SubRngβπ ) β§ π β π΄ β§ π β π΄) β (π + π) β π΄) | ||
Theorem | subrngmcl 20446 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 20475. (Revised by AV, 14-Feb-2025.) |
β’ Β· = (.rβπ ) β β’ ((π΄ β (SubRngβπ ) β§ π β π΄ β§ π β π΄) β (π Β· π) β π΄) | ||
Theorem | issubrng2 20447* | Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Rng β (π΄ β (SubRngβπ ) β (π΄ β (SubGrpβπ ) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ Β· π¦) β π΄))) | ||
Theorem | opprsubrng 20448 | Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.) |
β’ π = (opprβπ ) β β’ (SubRngβπ ) = (SubRngβπ) | ||
Theorem | subrngint 20449 | The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
β’ ((π β (SubRngβπ ) β§ π β β ) β β© π β (SubRngβπ )) | ||
Theorem | subrngin 20450 | The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
β’ ((π΄ β (SubRngβπ ) β§ π΅ β (SubRngβπ )) β (π΄ β© π΅) β (SubRngβπ )) | ||
Theorem | subrngmre 20451 | The subrings of a non-unital ring are a Moore system. (Contributed by AV, 15-Feb-2025.) |
β’ π΅ = (Baseβπ ) β β’ (π β Rng β (SubRngβπ ) β (Mooreβπ΅)) | ||
Theorem | subsubrng 20452 | A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRngβπ ) β (π΅ β (SubRngβπ) β (π΅ β (SubRngβπ ) β§ π΅ β π΄))) | ||
Theorem | subsubrng2 20453 | The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRngβπ ) β (SubRngβπ) = ((SubRngβπ ) β© π« π΄)) | ||
Theorem | rhmimasubrnglem 20454* | Lemma for rhmimasubrng 20455: Modified part of mhmima 18743. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 16-Feb-2025.) |
β’ π = (mulGrpβπ ) β β’ ((πΉ β (π MndHom π) β§ π β (SubRngβπ )) β βπ₯ β (πΉ β π)βπ¦ β (πΉ β π)(π₯(+gβπ)π¦) β (πΉ β π)) | ||
Theorem | rhmimasubrng 20455 | The homomorphic image of a subring is a subring. (Contributed by AV, 16-Feb-2025.) |
β’ ((πΉ β (π RingHom π) β§ π β (SubRngβπ)) β (πΉ β π) β (SubRngβπ)) | ||
Theorem | cntzsubrng 20456 | Centralizers in a non-unital ring are subrings. (Contributed by AV, 17-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ π = (mulGrpβπ ) & β’ π = (Cntzβπ) β β’ ((π β Rng β§ π β π΅) β (πβπ) β (SubRngβπ )) | ||
Theorem | subrngpropd 20457* | If two structures have the same ring components (properties), they have the same set of subrings. (Contributed by AV, 17-Feb-2025.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (SubRngβπΎ) = (SubRngβπΏ)) | ||
Syntax | csubrg 20458 | Extend class notation with all subrings of a ring. |
class SubRing | ||
Syntax | crgspn 20459 | Extend class notation with span of a set of elements over a ring. |
class RingSpan | ||
Definition | df-subrg 20460* |
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 20461* | 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 20462 | 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 20463 | A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π΅ = (Baseβπ ) β β’ (π΄ β (SubRingβπ ) β π΄ β π΅) | ||
Theorem | subrgid 20464 | Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β π΅ β (SubRingβπ )) | ||
Theorem | subrgring 20465 | A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRingβπ ) β π β Ring) | ||
Theorem | subrgcrng 20466 | A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = (π βΎs π΄) β β’ ((π β CRing β§ π΄ β (SubRingβπ )) β π β CRing) | ||
Theorem | subrgrcl 20467 | Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ (π΄ β (SubRingβπ ) β π β Ring) | ||
Theorem | subrgsubg 20468 | A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ (π΄ β (SubRingβπ ) β π΄ β (SubGrpβπ )) | ||
Theorem | subrgsubrng 20469 | A subring of a unital ring is a subring of a non-unital ring. (Contributed by AV, 30-Mar-2025.) |
β’ (π΄ β (SubRingβπ ) β π΄ β (SubRngβπ )) | ||
Theorem | subrg0 20470 | A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π = (π βΎs π΄) & β’ 0 = (0gβπ ) β β’ (π΄ β (SubRingβπ ) β 0 = (0gβπ)) | ||
Theorem | subrg1cl 20471 | A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ 1 = (1rβπ ) β β’ (π΄ β (SubRingβπ ) β 1 β π΄) | ||
Theorem | subrgbas 20472 | Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRingβπ ) β π΄ = (Baseβπ)) | ||
Theorem | subrg1 20473 | A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π = (π βΎs π΄) & β’ 1 = (1rβπ ) β β’ (π΄ β (SubRingβπ ) β 1 = (1rβπ)) | ||
Theorem | subrgacl 20474 | A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ + = (+gβπ ) β β’ ((π΄ β (SubRingβπ ) β§ π β π΄ β§ π β π΄) β (π + π) β π΄) | ||
Theorem | subrgmcl 20475 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) (Proof shortened by AV, 30-Mar-2025.) |
β’ Β· = (.rβπ ) β β’ ((π΄ β (SubRingβπ ) β§ π β π΄ β§ π β π΄) β (π Β· π) β π΄) | ||
Theorem | subrgsubm 20476 | A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (mulGrpβπ ) β β’ (π΄ β (SubRingβπ ) β π΄ β (SubMndβπ)) | ||
Theorem | subrgdvds 20477 | 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 20478 | 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 20479 | 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 20480 | 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 20481 | 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 20482 | 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 20483* | 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 20484 | Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
β’ π = (opprβπ ) β β’ (SubRingβπ ) = (SubRingβπ) | ||
Theorem | subrgnzr 20485 | A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (π βΎs π΄) β β’ ((π β NzRing β§ π΄ β (SubRingβπ )) β π β NzRing) | ||
Theorem | subrgint 20486 | 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 20487 | 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 20488 | The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β (SubRingβπ ) β (Mooreβπ΅)) | ||
Theorem | subsubrg 20489 | A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRingβπ ) β (π΅ β (SubRingβπ) β (π΅ β (SubRingβπ ) β§ π΅ β π΄))) | ||
Theorem | subsubrg2 20490 | 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 20491 | A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π = (mulGrpβπ ) β β’ (π β Ring β (π β (SubRingβπ ) β (π β (SubGrpβπ ) β§ π β (SubMndβπ)))) | ||
Theorem | resrhm 20492 | Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π RingHom π) β§ π β (SubRingβπ)) β (πΉ βΎ π) β (π RingHom π)) | ||
Theorem | resrhm2b 20493 | Restriction of the codomain of a (ring) homomorphism. resghm2b 19149 analog. (Contributed by SN, 7-Feb-2025.) |
β’ π = (π βΎs π) β β’ ((π β (SubRingβπ) β§ ran πΉ β π) β (πΉ β (π RingHom π) β πΉ β (π RingHom π))) | ||
Theorem | rhmeql 20494 | The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β dom (πΉ β© πΊ) β (SubRingβπ)) | ||
Theorem | rhmima 20495 | The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ ((πΉ β (π RingHom π) β§ π β (SubRingβπ)) β (πΉ β π) β (SubRingβπ)) | ||
Theorem | rnrhmsubrg 20496 | The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.) |
β’ (πΉ β (π RingHom π) β ran πΉ β (SubRingβπ)) | ||
Theorem | cntzsubr 20497 | Centralizers in a ring are subrings. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (Baseβπ ) & β’ π = (mulGrpβπ ) & β’ π = (Cntzβπ) β β’ ((π β Ring β§ π β π΅) β (πβπ) β (SubRingβπ )) | ||
Theorem | pwsdiagrhm 20498* | Diagonal homomorphism into a structure power (Rings). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ πΉ = (π₯ β π΅ β¦ (πΌ Γ {π₯})) β β’ ((π β Ring β§ πΌ β π) β πΉ β (π RingHom π)) | ||
Theorem | subrgpropd 20499* | If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (SubRingβπΎ) = (SubRingβπΏ)) | ||
Theorem | rhmpropd 20500* | Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ (π β π΅ = (Baseβπ½)) & β’ (π β πΆ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β πΆ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ½)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπ½)π¦) = (π₯(.rβπΏ)π¦)) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπ)π¦)) β β’ (π β (π½ RingHom πΎ) = (πΏ RingHom π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |