![]() |
Metamath
Proof Explorer Theorem List (p. 207 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | srhmsubclem3 20601* | Lemma 3 for srhmsubc 20602. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ ((π β π β§ (π β πΆ β§ π β πΆ)) β (ππ½π) = (π(Hom β(RingCatβπ))π)) | ||
Theorem | srhmsubc 20602* | According to df-subc 17786, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17817 and subcss2 17820). Therefore, the set of special ring homomorphisms (i.e., ring homomorphisms from a special ring to another ring of that kind) is a subcategory of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | sringcat 20603* | The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | crhmsubc 20604* | According to df-subc 17786, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17817 and subcss2 17820). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | cringcat 20605* | The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | rngcrescrhm 20606 | The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β (πΆ βΎcat π») = ((πΆ βΎs π ) sSet β¨(Hom βndx), π»β©)) | ||
Theorem | rhmsubclem1 20607 | Lemma 1 for rhmsubc 20611. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» Fn (π Γ π )) | ||
Theorem | rhmsubclem2 20608 | Lemma 2 for rhmsubc 20611. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π β π β§ π β π ) β (ππ»π) = (π RingHom π)) | ||
Theorem | rhmsubclem3 20609* | Lemma 3 for rhmsubc 20611. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π₯ β π ) β ((Idβ(RngCatβπ))βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubclem4 20610* | Lemma 4 for rhmsubc 20611. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((((π β§ π₯ β π ) β§ (π¦ β π β§ π§ β π )) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubc 20611 | According to df-subc 17786, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17817 and subcss2 17820). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» β (Subcatβ(RngCatβπ))) | ||
Theorem | rhmsubccat 20612 | The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β ((RngCatβπ) βΎcat π») β Cat) | ||
Syntax | cdr 20613 | Extend class notation with class of all division rings. |
class DivRing | ||
Syntax | cfield 20614 | Class of fields. |
class Field | ||
Definition | df-drng 20615 | 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 20616 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ Field = (DivRing β© CRing) | ||
Theorem | isdrng 20617 | 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 20618 | 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 20619 | The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π β DivRing β β’ (π΅ β { 0 }) = (Unitβπ ) | ||
Theorem | drngring 20620 | A division ring is a ring. (Contributed by NM, 8-Sep-2011.) |
β’ (π β DivRing β π β Ring) | ||
Theorem | drngringd 20621 | A division ring is a ring. (Contributed by SN, 16-May-2024.) |
β’ (π β π β DivRing) β β’ (π β π β Ring) | ||
Theorem | drnggrpd 20622 | A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.) |
β’ (π β π β DivRing) β β’ (π β π β Grp) | ||
Theorem | drnggrp 20623 | A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.) |
β’ (π β DivRing β π β Grp) | ||
Theorem | isfld 20624 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ (π β Field β (π β DivRing β§ π β CRing)) | ||
Theorem | flddrngd 20625 | A field is a division ring. (Contributed by SN, 17-Jan-2025.) |
β’ (π β π β Field) β β’ (π β π β DivRing) | ||
Theorem | fldcrngd 20626 | A field is a commutative ring. (Contributed by SN, 23-Nov-2024.) |
β’ (π β π β Field) β β’ (π β π β CRing) | ||
Theorem | isdrng2 20627 | 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 20628 | 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 20629 | A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs (π΅ β { 0 })) β β’ (π β DivRing β πΊ β Grp) | ||
Theorem | drngmcl 20630 | 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 20631 | 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 20632 | 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 20633 | All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ (π β DivRing β π β NzRing) | ||
Theorem | drngid2 20634 | 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 20635 | Closure of the multiplicative inverse in a division ring. (reccl 11901 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β (πΌβπ) β π΅) | ||
Theorem | drnginvrn0 20636 | The multiplicative inverse in a division ring is nonzero. (recne0 11907 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β (πΌβπ) β 0 ) | ||
Theorem | drnginvrcld 20637 | Closure of the multiplicative inverse in a division ring. (reccld 12005 analog). (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β (πΌβπ) β π΅) | ||
Theorem | drnginvrl 20638 | Property of the multiplicative inverse in a division ring. (recid2 11909 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β ((πΌβπ) Β· π) = 1 ) | ||
Theorem | drnginvrr 20639 | Property of the multiplicative inverse in a division ring. (recid 11908 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β (π Β· (πΌβπ)) = 1 ) | ||
Theorem | drnginvrld 20640 | Property of the multiplicative inverse in a division ring. (recid2d 12008 analog). (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β ((πΌβπ) Β· π) = 1 ) | ||
Theorem | drnginvrrd 20641 | Property of the multiplicative inverse in a division ring. (recidd 12007 analog). (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β (π Β· (πΌβπ)) = 1 ) | ||
Theorem | drngmul0or 20642 | 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 20643 | 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 20644 | 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 20645 | The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.) |
β’ π = (opprβπ ) β β’ (π β DivRing β π β DivRing) | ||
Theorem | isdrngd 20646* | 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 20647 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 20647* | 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 20646 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 20648* | Obsolete version of isdrngd 20646 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 20649* | Obsolete version of isdrngrd 20647 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 20650* | 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 20651* | 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 20652 | 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 20653 | 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 20654 | 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 20655 | 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 20656 | The zero ring is not a field. (Contributed by AV, 29-Apr-2019.) |
β’ π = {β¨(Baseβndx), {π}β©, β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©, β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} β β’ (π β π β π β Field) | ||
Theorem | issubdrg 20657* | Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ π = (π βΎs π΄) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π΄ β (SubRingβπ )) β (π β DivRing β βπ₯ β (π΄ β { 0 })(πΌβπ₯) β π΄)) | ||
Theorem | drhmsubc 20658* | According to df-subc 17786, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17817 and subcss2 17820). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | drngcat 20659* | The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | fldcat 20660* | The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat πΉ) β Cat) | ||
Theorem | fldc 20661* | The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β (((RingCatβπ) βΎcat π½) βΎcat πΉ) β Cat) | ||
Theorem | fldhmsubc 20662* | According to df-subc 17786, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17817 and subcss2 17820). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β πΉ β (Subcatβ((RingCatβπ) βΎcat π½))) | ||
Syntax | csdrg 20663 | Syntax for subfields (sub-division-rings). |
class SubDRing | ||
Definition | df-sdrg 20664* | Define the function associating with a ring the set of its sub-division-rings. A sub-division-ring of a ring is a subset of its base set which is a division ring when equipped with the induced structure (sum, multiplication, zero, and unity). If a ring is commutative (resp., a field), then its sub-division-rings are commutative (resp., are fields) (fldsdrgfld 20675), so we do not make a specific definition for subfields. (Contributed by Stefan O'Rear, 3-Oct-2015.) TODO: extend this definition to a function with domain V or at least Ring and not only DivRing. |
β’ SubDRing = (π€ β DivRing β¦ {π β (SubRingβπ€) β£ (π€ βΎs π ) β DivRing}) | ||
Theorem | issdrg 20665 | Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
β’ (π β (SubDRingβπ ) β (π β DivRing β§ π β (SubRingβπ ) β§ (π βΎs π) β DivRing)) | ||
Theorem | sdrgrcl 20666 | Reverse closure for a sub-division-ring predicate. (Contributed by SN, 19-Feb-2025.) |
β’ (π΄ β (SubDRingβπ ) β π β DivRing) | ||
Theorem | sdrgdrng 20667 | A sub-division-ring is a division ring. (Contributed by SN, 19-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubDRingβπ ) β π β DivRing) | ||
Theorem | sdrgsubrg 20668 | A sub-division-ring is a subring. (Contributed by SN, 19-Feb-2025.) |
β’ (π΄ β (SubDRingβπ ) β π΄ β (SubRingβπ )) | ||
Theorem | sdrgid 20669 | Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π΅ = (Baseβπ ) β β’ (π β DivRing β π΅ β (SubDRingβπ )) | ||
Theorem | sdrgss 20670 | A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π΅ = (Baseβπ ) β β’ (π β (SubDRingβπ ) β π β π΅) | ||
Theorem | sdrgbas 20671 | Base set of a sub-division-ring structure. (Contributed by SN, 19-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubDRingβπ ) β π΄ = (Baseβπ)) | ||
Theorem | issdrg2 20672* | Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ πΌ = (invrβπ ) & β’ 0 = (0gβπ ) β β’ (π β (SubDRingβπ ) β (π β DivRing β§ π β (SubRingβπ ) β§ βπ₯ β (π β { 0 })(πΌβπ₯) β π)) | ||
Theorem | sdrgunit 20673 | A unit of a sub-division-ring is a nonzero element of the subring. (Contributed by SN, 19-Feb-2025.) |
β’ π = (π βΎs π΄) & β’ 0 = (0gβπ ) & β’ π = (Unitβπ) β β’ (π΄ β (SubDRingβπ ) β (π β π β (π β π΄ β§ π β 0 ))) | ||
Theorem | imadrhmcl 20674 | The image of a (nontrivial) division ring homomorphism is a division ring. (Contributed by SN, 17-Feb-2025.) |
β’ π = (π βΎs (πΉ β π)) & β’ 0 = (0gβπ) & β’ (π β πΉ β (π RingHom π)) & β’ (π β π β (SubDRingβπ)) & β’ (π β ran πΉ β { 0 }) β β’ (π β π β DivRing) | ||
Theorem | fldsdrgfld 20675 | A sub-division-ring of a field is itself a field, so it is a subfield. We can therefore use SubDRing to express subfields. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
β’ ((πΉ β Field β§ π΄ β (SubDRingβπΉ)) β (πΉ βΎs π΄) β Field) | ||
Theorem | acsfn1p 20676* | Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ ((π β π β§ βπ β π πΈ β π) β {π β π« π β£ βπ β (π β© π)πΈ β π} β (ACSβπ)) | ||
Theorem | subrgacs 20677 | Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β (SubRingβπ ) β (ACSβπ΅)) | ||
Theorem | sdrgacs 20678 | Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β DivRing β (SubDRingβπ ) β (ACSβπ΅)) | ||
Theorem | cntzsdrg 20679 | Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (mulGrpβπ ) & β’ π = (Cntzβπ) β β’ ((π β DivRing β§ π β π΅) β (πβπ) β (SubDRingβπ )) | ||
Theorem | subdrgint 20680* | The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ πΏ = (π βΎs β© π) & β’ (π β π β DivRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β β ) & β’ ((π β§ π β π) β (π βΎs π ) β DivRing) β β’ (π β πΏ β DivRing) | ||
Theorem | sdrgint 20681 | The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ ((π β DivRing β§ π β (SubDRingβπ ) β§ π β β ) β β© π β (SubDRingβπ )) | ||
Theorem | primefld 20682 | The smallest sub division ring of a division ring, here named π, is a field, called the Prime Field of π . (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π = (π βΎs β© (SubDRingβπ )) β β’ (π β DivRing β π β Field) | ||
Theorem | primefld0cl 20683 | The prime field contains the zero element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.) |
β’ 0 = (0gβπ ) β β’ (π β DivRing β 0 β β© (SubDRingβπ )) | ||
Theorem | primefld1cl 20684 | The prime field contains the unity element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.) |
β’ 1 = (1rβπ ) β β’ (π β DivRing β 1 β β© (SubDRingβπ )) | ||
Syntax | cabv 20685 | The set of absolute values on a ring. |
class AbsVal | ||
Definition | df-abv 20686* | Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 15207 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ AbsVal = (π β Ring β¦ {π β ((0[,)+β) βm (Baseβπ)) β£ βπ₯ β (Baseβπ)(((πβπ₯) = 0 β π₯ = (0gβπ)) β§ βπ¦ β (Baseβπ)((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦))))}) | ||
Theorem | abvfval 20687* | Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β π΄ = {π β ((0[,)+β) βm π΅) β£ βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))}) | ||
Theorem | isabv 20688* | Elementhood in the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β (πΉ β π΄ β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))))) | ||
Theorem | isabvd 20689* | Properties that determine an absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 4-Dec-2014.) |
β’ (π β π΄ = (AbsValβπ )) & β’ (π β π΅ = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β 0 = (0gβπ )) & β’ (π β π β Ring) & β’ (π β πΉ:π΅βΆβ) & β’ (π β (πΉβ 0 ) = 0) & β’ ((π β§ π₯ β π΅ β§ π₯ β 0 ) β 0 < (πΉβπ₯)) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) β β’ (π β πΉ β π΄) | ||
Theorem | abvrcl 20690 | Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) β β’ (πΉ β π΄ β π β Ring) | ||
Theorem | abvfge0 20691 | An absolute value is a function from the ring to the nonnegative real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ (πΉ β π΄ β πΉ:π΅βΆ(0[,)+β)) | ||
Theorem | abvf 20692 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ (πΉ β π΄ β πΉ:π΅βΆβ) | ||
Theorem | abvcl 20693 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ ((πΉ β π΄ β§ π β π΅) β (πΉβπ) β β) | ||
Theorem | abvge0 20694 | The absolute value of a number is greater than or equal to zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ ((πΉ β π΄ β§ π β π΅) β 0 β€ (πΉβπ)) | ||
Theorem | abveq0 20695 | The value of an absolute value is zero iff the argument is zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((πΉ β π΄ β§ π β π΅) β ((πΉβπ) = 0 β π = 0 )) | ||
Theorem | abvne0 20696 | The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β 0 ) β (πΉβπ) β 0) | ||
Theorem | abvgt0 20697 | The absolute value of a nonzero number is strictly positive. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β 0 ) β 0 < (πΉβπ)) | ||
Theorem | abvmul 20698 | An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β π΅) β (πΉβ(π Β· π)) = ((πΉβπ) Β· (πΉβπ))) | ||
Theorem | abvtri 20699 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β π΅) β (πΉβ(π + π)) β€ ((πΉβπ) + (πΉβπ))) | ||
Theorem | abv0 20700 | The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ 0 = (0gβπ ) β β’ (πΉ β π΄ β (πΉβ 0 ) = 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |