![]() |
Metamath
Proof Explorer Theorem List (p. 206 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cdr 20501 | Extend class notation with class of all division rings. |
class DivRing | ||
Syntax | cfield 20502 | Class of fields. |
class Field | ||
Definition | df-drng 20503 | 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 20504 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ Field = (DivRing β© CRing) | ||
Theorem | isdrng 20505 | 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 20506 | 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 20507 | The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π β DivRing β β’ (π΅ β { 0 }) = (Unitβπ ) | ||
Theorem | drngring 20508 | A division ring is a ring. (Contributed by NM, 8-Sep-2011.) |
β’ (π β DivRing β π β Ring) | ||
Theorem | drngringd 20509 | A division ring is a ring. (Contributed by SN, 16-May-2024.) |
β’ (π β π β DivRing) β β’ (π β π β Ring) | ||
Theorem | drnggrpd 20510 | A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.) |
β’ (π β π β DivRing) β β’ (π β π β Grp) | ||
Theorem | drnggrp 20511 | A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.) |
β’ (π β DivRing β π β Grp) | ||
Theorem | isfld 20512 | A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ (π β Field β (π β DivRing β§ π β CRing)) | ||
Theorem | flddrngd 20513 | A field is a division ring. (Contributed by SN, 17-Jan-2025.) |
β’ (π β π β Field) β β’ (π β π β DivRing) | ||
Theorem | fldcrngd 20514 | A field is a commutative ring. (Contributed by SN, 23-Nov-2024.) |
β’ (π β π β Field) β β’ (π β π β CRing) | ||
Theorem | isdrng2 20515 | 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 20516 | 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 20517 | A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs (π΅ β { 0 })) β β’ (π β DivRing β πΊ β Grp) | ||
Theorem | drngmcl 20518 | 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 20519 | 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 20520 | 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 20521 | All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ (π β DivRing β π β NzRing) | ||
Theorem | drngid2 20522 | 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 20523 | Closure of the multiplicative inverse in a division ring. (reccl 11884 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β (πΌβπ) β π΅) | ||
Theorem | drnginvrn0 20524 | The multiplicative inverse in a division ring is nonzero. (recne0 11890 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β (πΌβπ) β 0 ) | ||
Theorem | drnginvrcld 20525 | Closure of the multiplicative inverse in a division ring. (reccld 11988 analog). (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β (πΌβπ) β π΅) | ||
Theorem | drnginvrl 20526 | Property of the multiplicative inverse in a division ring. (recid2 11892 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β ((πΌβπ) Β· π) = 1 ) | ||
Theorem | drnginvrr 20527 | Property of the multiplicative inverse in a division ring. (recid 11891 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π β π΅ β§ π β 0 ) β (π Β· (πΌβπ)) = 1 ) | ||
Theorem | drnginvrld 20528 | Property of the multiplicative inverse in a division ring. (recid2d 11991 analog). (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β ((πΌβπ) Β· π) = 1 ) | ||
Theorem | drnginvrrd 20529 | Property of the multiplicative inverse in a division ring. (recidd 11990 analog). (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β (π Β· (πΌβπ)) = 1 ) | ||
Theorem | drngmul0or 20530 | 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 20531 | 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 20532 | 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 20533 | The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.) |
β’ π = (opprβπ ) β β’ (π β DivRing β π β DivRing) | ||
Theorem | isdrngd 20534* | 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 20535 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 20535* | 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 20534 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 20536* | Obsolete version of isdrngd 20534 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 20537* | Obsolete version of isdrngrd 20535 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 20538* | 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 20539* | 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 20540 | 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 20541 | 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 20542 | 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 20543 | 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 20544 | The zero ring is not a field. (Contributed by AV, 29-Apr-2019.) |
β’ π = {β¨(Baseβndx), {π}β©, β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©, β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} β β’ (π β π β π β Field) | ||
Theorem | issubdrg 20545* | Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ π = (π βΎs π΄) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π΄ β (SubRingβπ )) β (π β DivRing β βπ₯ β (π΄ β { 0 })(πΌβπ₯) β π΄)) | ||
Syntax | csdrg 20546 | Syntax for subfields (sub-division-rings). |
class SubDRing | ||
Definition | df-sdrg 20547* | 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 20558), 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 20548 | Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
β’ (π β (SubDRingβπ ) β (π β DivRing β§ π β (SubRingβπ ) β§ (π βΎs π) β DivRing)) | ||
Theorem | sdrgrcl 20549 | Reverse closure for a sub-division-ring predicate. (Contributed by SN, 19-Feb-2025.) |
β’ (π΄ β (SubDRingβπ ) β π β DivRing) | ||
Theorem | sdrgdrng 20550 | A sub-division-ring is a division ring. (Contributed by SN, 19-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubDRingβπ ) β π β DivRing) | ||
Theorem | sdrgsubrg 20551 | A sub-division-ring is a subring. (Contributed by SN, 19-Feb-2025.) |
β’ (π΄ β (SubDRingβπ ) β π΄ β (SubRingβπ )) | ||
Theorem | sdrgid 20552 | Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π΅ = (Baseβπ ) β β’ (π β DivRing β π΅ β (SubDRingβπ )) | ||
Theorem | sdrgss 20553 | A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π΅ = (Baseβπ ) β β’ (π β (SubDRingβπ ) β π β π΅) | ||
Theorem | sdrgbas 20554 | Base set of a sub-division-ring structure. (Contributed by SN, 19-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubDRingβπ ) β π΄ = (Baseβπ)) | ||
Theorem | issdrg2 20555* | Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ πΌ = (invrβπ ) & β’ 0 = (0gβπ ) β β’ (π β (SubDRingβπ ) β (π β DivRing β§ π β (SubRingβπ ) β§ βπ₯ β (π β { 0 })(πΌβπ₯) β π)) | ||
Theorem | sdrgunit 20556 | 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 20557 | 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 20558 | 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 20559* | Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ ((π β π β§ βπ β π πΈ β π) β {π β π« π β£ βπ β (π β© π)πΈ β π} β (ACSβπ)) | ||
Theorem | subrgacs 20560 | Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β (SubRingβπ ) β (ACSβπ΅)) | ||
Theorem | sdrgacs 20561 | Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β DivRing β (SubDRingβπ ) β (ACSβπ΅)) | ||
Theorem | cntzsdrg 20562 | Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (mulGrpβπ ) & β’ π = (Cntzβπ) β β’ ((π β DivRing β§ π β π΅) β (πβπ) β (SubDRingβπ )) | ||
Theorem | subdrgint 20563* | 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 20564 | 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 20565 | 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 20566 | 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 20567 | 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 20568 | The set of absolute values on a ring. |
class AbsVal | ||
Definition | df-abv 20569* | Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 15188 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ AbsVal = (π β Ring β¦ {π β ((0[,)+β) βm (Baseβπ)) β£ βπ₯ β (Baseβπ)(((πβπ₯) = 0 β π₯ = (0gβπ)) β§ βπ¦ β (Baseβπ)((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦))))}) | ||
Theorem | abvfval 20570* | 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 20571* | 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 20572* | 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 20573 | Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) β β’ (πΉ β π΄ β π β Ring) | ||
Theorem | abvfge0 20574 | 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 20575 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ (πΉ β π΄ β πΉ:π΅βΆβ) | ||
Theorem | abvcl 20576 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ ((πΉ β π΄ β§ π β π΅) β (πΉβπ) β β) | ||
Theorem | abvge0 20577 | 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 20578 | 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 20579 | The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β 0 ) β (πΉβπ) β 0) | ||
Theorem | abvgt0 20580 | 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 20581 | An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β π΅) β (πΉβ(π Β· π)) = ((πΉβπ) Β· (πΉβπ))) | ||
Theorem | abvtri 20582 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β π΅) β (πΉβ(π + π)) β€ ((πΉβπ) + (πΉβπ))) | ||
Theorem | abv0 20583 | The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ 0 = (0gβπ ) β β’ (πΉ β π΄ β (πΉβ 0 ) = 0) | ||
Theorem | abv1z 20584 | The absolute value of one is one in a non-trivial ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ ((πΉ β π΄ β§ 1 β 0 ) β (πΉβ 1 ) = 1) | ||
Theorem | abv1 20585 | The absolute value of one is one in a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ 1 = (1rβπ ) β β’ ((π β DivRing β§ πΉ β π΄) β (πΉβ 1 ) = 1) | ||
Theorem | abvneg 20586 | The absolute value of a negative is the same as that of the positive. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ π = (invgβπ ) β β’ ((πΉ β π΄ β§ π β π΅) β (πΉβ(πβπ)) = (πΉβπ)) | ||
Theorem | abvsubtri 20587 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ β = (-gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β π΅) β (πΉβ(π β π)) β€ ((πΉβπ) + (πΉβπ))) | ||
Theorem | abvrec 20588 | The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ (((π β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β 0 )) β (πΉβ(πΌβπ)) = (1 / (πΉβπ))) | ||
Theorem | abvdiv 20589 | The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ / = (/rβπ ) β β’ (((π β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβ(π / π)) = ((πΉβπ) / (πΉβπ))) | ||
Theorem | abvdom 20590 | Any ring with an absolute value is a domain, which is to say that it contains no zero divisors. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) β β’ ((πΉ β π΄ β§ (π β π΅ β§ π β 0 ) β§ (π β π΅ β§ π β 0 )) β (π Β· π) β 0 ) | ||
Theorem | abvres 20591 | The restriction of an absolute value to a subring is an absolute value. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π = (π βΎs πΆ) & β’ π΅ = (AbsValβπ) β β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ )) β (πΉ βΎ πΆ) β π΅) | ||
Theorem | abvtrivd 20592* | The trivial absolute value. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΉ = (π₯ β π΅ β¦ if(π₯ = 0 , 0, 1)) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (π¦ Β· π§) β 0 ) β β’ (π β πΉ β π΄) | ||
Theorem | abvtriv 20593* | The trivial absolute value. (This theorem is true as long as π is a domain, but it is not true for rings with zero divisors, which violate the multiplication axiom; abvdom 20590 is the converse of this remark.) (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΉ = (π₯ β π΅ β¦ if(π₯ = 0 , 0, 1)) β β’ (π β DivRing β πΉ β π΄) | ||
Theorem | abvpropd 20594* | If two structures have the same ring components, they have the same collection of absolute values. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (AbsValβπΎ) = (AbsValβπΏ)) | ||
Syntax | cstf 20595 | Extend class notation with the functionalization of the *-ring involution. |
class *rf | ||
Syntax | csr 20596 | Extend class notation with class of all *-rings. |
class *-Ring | ||
Definition | df-staf 20597* | Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *π as an actual function we can state the principal properties of an involution much more cleanly. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ *rf = (π β V β¦ (π₯ β (Baseβπ) β¦ ((*πβπ)βπ₯))) | ||
Definition | df-srng 20598* | Define class of all star rings. A star ring is a ring with an involution (conjugation) function. Involution (unlike say the ring zero) is not unique and therefore must be added as a new component to the ring. For example, two possible involutions for complex numbers are the identity function and complex conjugation. Definition of involution in [Holland95] p. 204. (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.) |
β’ *-Ring = {π β£ [(*rfβπ) / π](π β (π RingHom (opprβπ)) β§ π = β‘π)} | ||
Theorem | staffval 20599* | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ β = (*πβπ ) & β’ β = (*rfβπ ) β β’ β = (π₯ β π΅ β¦ ( β βπ₯)) | ||
Theorem | stafval 20600 | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ β = (*πβπ ) & β’ β = (*rfβπ ) β β’ (π΄ β π΅ β ( β βπ΄) = ( β βπ΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |