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