![]() |
Metamath
Proof Explorer Theorem List (p. 204 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 0ringnnzr 20301 | 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 20302 | 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 20303 | 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 20304 | 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 20305 | Obsolete version of 01eq0ring 20304 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 20306 | 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 )) | ||
Syntax | clring 20307 | Extend class notation with class of all local rings. |
class LRing | ||
Definition | df-lring 20308* | 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 20309* | The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ 1 = (1rβπ ) & β’ π = (Unitβπ ) β β’ (π β LRing β (π β NzRing β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ + π¦) = 1 β (π₯ β π β¨ π¦ β π)))) | ||
Theorem | lringnzr 20310 | A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.) |
β’ (π β LRing β π β NzRing) | ||
Theorem | lringring 20311 | A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
β’ (π β LRing β π β Ring) | ||
Theorem | lringnz 20312 | 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 20313 | 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 | csubrg 20314 | Extend class notation with all subrings of a ring. |
class SubRing | ||
Syntax | crgspn 20315 | Extend class notation with span of a set of elements over a ring. |
class RingSpan | ||
Definition | df-subrg 20316* |
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 20317* | 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 20318 | 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 20319 | A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π΅ = (Baseβπ ) β β’ (π΄ β (SubRingβπ ) β π΄ β π΅) | ||
Theorem | subrgid 20320 | Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β π΅ β (SubRingβπ )) | ||
Theorem | subrgring 20321 | A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRingβπ ) β π β Ring) | ||
Theorem | subrgcrng 20322 | A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = (π βΎs π΄) β β’ ((π β CRing β§ π΄ β (SubRingβπ )) β π β CRing) | ||
Theorem | subrgrcl 20323 | Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ (π΄ β (SubRingβπ ) β π β Ring) | ||
Theorem | subrgsubg 20324 | A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ (π΄ β (SubRingβπ ) β π΄ β (SubGrpβπ )) | ||
Theorem | subrg0 20325 | A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π = (π βΎs π΄) & β’ 0 = (0gβπ ) β β’ (π΄ β (SubRingβπ ) β 0 = (0gβπ)) | ||
Theorem | subrg1cl 20326 | A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ 1 = (1rβπ ) β β’ (π΄ β (SubRingβπ ) β 1 β π΄) | ||
Theorem | subrgbas 20327 | Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRingβπ ) β π΄ = (Baseβπ)) | ||
Theorem | subrg1 20328 | A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π = (π βΎs π΄) & β’ 1 = (1rβπ ) β β’ (π΄ β (SubRingβπ ) β 1 = (1rβπ)) | ||
Theorem | subrgacl 20329 | A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ + = (+gβπ ) β β’ ((π΄ β (SubRingβπ ) β§ π β π΄ β§ π β π΄) β (π + π) β π΄) | ||
Theorem | subrgmcl 20330 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ Β· = (.rβπ ) β β’ ((π΄ β (SubRingβπ ) β§ π β π΄ β§ π β π΄) β (π Β· π) β π΄) | ||
Theorem | subrgsubm 20331 | A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (mulGrpβπ ) β β’ (π΄ β (SubRingβπ ) β π΄ β (SubMndβπ)) | ||
Theorem | subrgdvds 20332 | 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 20333 | 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 20334 | 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 20335 | 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 20336 | 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 20337 | 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 20338* | 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 20339 | Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
β’ π = (opprβπ ) β β’ (SubRingβπ ) = (SubRingβπ) | ||
Theorem | subrgnzr 20340 | A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (π βΎs π΄) β β’ ((π β NzRing β§ π΄ β (SubRingβπ )) β π β NzRing) | ||
Theorem | subrgint 20341 | 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 20342 | 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 20343 | The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β (SubRingβπ ) β (Mooreβπ΅)) | ||
Theorem | subsubrg 20344 | A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubRingβπ ) β (π΅ β (SubRingβπ) β (π΅ β (SubRingβπ ) β§ π΅ β π΄))) | ||
Theorem | subsubrg2 20345 | 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 20346 | 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 20347 | Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π RingHom π) β§ π β (SubRingβπ)) β (πΉ βΎ π) β (π RingHom π)) | ||
Theorem | resrhm2b 20348 | Restriction of the codomain of a (ring) homomorphism. resghm2b 19109 analog. (Contributed by SN, 7-Feb-2025.) |
β’ π = (π βΎs π) β β’ ((π β (SubRingβπ) β§ ran πΉ β π) β (πΉ β (π RingHom π) β πΉ β (π RingHom π))) | ||
Theorem | rhmeql 20349 | 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 20350 | 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 20351 | The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.) |
β’ (πΉ β (π RingHom π) β ran πΉ β (SubRingβπ)) | ||
Theorem | cntzsubr 20352 | 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 20353* | 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 20354* | 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 20355* | 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 π)) | ||
Syntax | cdr 20356 | Extend class notation with class of all division rings. |
class DivRing | ||
Syntax | cfield 20357 | Class of fields. |
class Field | ||
Definition | df-drng 20358 | 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 20359 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ Field = (DivRing β© CRing) | ||
Theorem | isdrng 20360 | 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 20361 | 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 20362 | The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π β DivRing β β’ (π΅ β { 0 }) = (Unitβπ ) | ||
Theorem | drngring 20363 | A division ring is a ring. (Contributed by NM, 8-Sep-2011.) |
β’ (π β DivRing β π β Ring) | ||
Theorem | drngringd 20364 | A division ring is a ring. (Contributed by SN, 16-May-2024.) |
β’ (π β π β DivRing) β β’ (π β π β Ring) | ||
Theorem | drnggrpd 20365 | A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.) |
β’ (π β π β DivRing) β β’ (π β π β Grp) | ||
Theorem | drnggrp 20366 | A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.) |
β’ (π β DivRing β π β Grp) | ||
Theorem | isfld 20367 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ (π β Field β (π β DivRing β§ π β CRing)) | ||
Theorem | flddrngd 20368 | A field is a division ring. (Contributed by SN, 17-Jan-2025.) |
β’ (π β π β Field) β β’ (π β π β DivRing) | ||
Theorem | fldcrngd 20369 | A field is a commutative ring. (Contributed by SN, 23-Nov-2024.) |
β’ (π β π β Field) β β’ (π β π β CRing) | ||
Theorem | isdrng2 20370 | 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 20371 | 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 20372 | A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs (π΅ β { 0 })) β β’ (π β DivRing β πΊ β Grp) | ||
Theorem | drngmcl 20373 | 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 20374 | A division ring's unity 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 20375 | A division ring's unity is different from its zero. (Contributed by NM, 8-Sep-2011.) |
β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ (π β DivRing β 1 β 0 ) | ||
Theorem | drngnzr 20376 | All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ (π β DivRing β π β NzRing) | ||
Theorem | drngid2 20377 | 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 20378 | Closure of the multiplicative inverse in a division ring. (reccl 11878 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β (πΌβπ) β π΅) | ||
Theorem | drnginvrn0 20379 | The multiplicative inverse in a division ring is nonzero. (recne0 11884 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β (πΌβπ) β 0 ) | ||
Theorem | drnginvrcld 20380 | Closure of the multiplicative inverse in a division ring. (reccld 11982 analog). (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β (πΌβπ) β π΅) | ||
Theorem | drnginvrl 20381 | Property of the multiplicative inverse in a division ring. (recid2 11886 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β ((πΌβπ) Β· π) = 1 ) | ||
Theorem | drnginvrr 20382 | Property of the multiplicative inverse in a division ring. (recid 11885 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β (π Β· (πΌβπ)) = 1 ) | ||
Theorem | drnginvrld 20383 | Property of the multiplicative inverse in a division ring. (recid2d 11985 analog). (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β ((πΌβπ) Β· π) = 1 ) | ||
Theorem | drnginvrrd 20384 | Property of the multiplicative inverse in a division ring. (recidd 11984 analog). (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β (π Β· (πΌβπ)) = 1 ) | ||
Theorem | drngmul0or 20385 | 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 20386 | 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 20387 | 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 20388 | The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.) |
β’ π = (opprβπ ) β β’ (π β DivRing β π β DivRing) | ||
Theorem | isdrngd 20389* | 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 isdrngrd 20390 for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013.) Remove hypothesis. (Revised by SN, 19-Feb-2025.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β 0 = (0gβπ )) & β’ (π β 1 = (1rβπ )) & β’ (π β π β Ring) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (π₯ Β· π¦) β 0 ) & β’ (π β 1 β 0 ) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β πΌ β π΅) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β (πΌ Β· π₯) = 1 ) β β’ (π β π β DivRing) | ||
Theorem | isdrngrd 20390* | 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 20389 for the characterization using left-inverses. (Contributed by NM, 10-Aug-2013.) Remove hypothesis. (Revised by SN, 19-Feb-2025.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β 0 = (0gβπ )) & β’ (π β 1 = (1rβπ )) & β’ (π β π β Ring) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (π₯ Β· π¦) β 0 ) & β’ (π β 1 β 0 ) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β πΌ β π΅) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β (π₯ Β· πΌ) = 1 ) β β’ (π β π β DivRing) | ||
Theorem | isdrngdOLD 20391* | Obsolete version of isdrngd 20389 as of 19-Feb-2025. (Contributed by NM, 2-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β 0 = (0gβπ )) & β’ (π β 1 = (1rβπ )) & β’ (π β π β Ring) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (π₯ Β· π¦) β 0 ) & β’ (π β 1 β 0 ) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β πΌ β π΅) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β πΌ β 0 ) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β (πΌ Β· π₯) = 1 ) β β’ (π β π β DivRing) | ||
Theorem | isdrngrdOLD 20392* | Obsolete version of isdrngrd 20390 as of 19-Feb-2025. (Contributed by NM, 10-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β 0 = (0gβπ )) & β’ (π β 1 = (1rβπ )) & β’ (π β π β Ring) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (π₯ Β· π¦) β 0 ) & β’ (π β 1 β 0 ) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β πΌ β π΅) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β πΌ β 0 ) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 )) β (π₯ Β· πΌ) = 1 ) β β’ (π β π β DivRing) | ||
Theorem | drngpropd 20393* | 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 20394* | 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)) | ||
Theorem | rng1nnzr 20395 | 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 20396 | 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 20397 | 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 (π΅ Γ π΅)) β§ π β π΅) β (π΅ β 1o β ( + = {β¨β¨π, πβ©, πβ©} β§ β = {β¨β¨π, πβ©, πβ©}))) | ||
Theorem | ringen1zr 20398 | 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 (π΅ Γ π΅)) β (π΅ β 1o β ( + = {β¨β¨π, πβ©, πβ©} β§ β = {β¨β¨π, πβ©, πβ©}))) | ||
Theorem | rng1nfld 20399 | The zero ring is not a field. (Contributed by AV, 29-Apr-2019.) |
β’ π = {β¨(Baseβndx), {π}β©, β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©, β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} β β’ (π β π β π β Field) | ||
Theorem | issubdrg 20400* | Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ π = (π βΎs π΄) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π΄ β (SubRingβπ )) β (π β DivRing β βπ₯ β (π΄ β { 0 })(πΌβπ₯) β π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |