![]() |
Metamath
Proof Explorer Theorem List (p. 331 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | erlbr2d 33001 | Deduce the ring localization equivalence relation. Pairs β¨πΈ, πΊβ© and β¨π Β· πΈ, π Β· πΊβ© for π β π are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ βΌ = (π ~RL π) & β’ (π β π β CRing) & β’ (π β π β (SubMndβ(mulGrpβπ ))) & β’ Β· = (.rβπ ) & β’ (π β π = β¨πΈ, πΊβ©) & β’ (π β π = β¨πΉ, π»β©) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π) & β’ (π β π» β π) & β’ (π β π β π) & β’ (π β πΉ = (π Β· πΈ)) & β’ (π β π» = (π Β· πΊ)) β β’ (π β π βΌ π) | ||
Theorem | erler 33002 | The relation used to build the ring localization is an equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ π = (π΅ Γ π) & β’ βΌ = (π ~RL π) & β’ (π β π β CRing) & β’ (π β π β (SubMndβ(mulGrpβπ ))) β β’ (π β βΌ Er π) | ||
Theorem | elrlocbasi 33003* | Membership in the basis of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ (π β π β ((π΅ Γ π) / βΌ )) β β’ (π β βπ β π΅ βπ β π π = [β¨π, πβ©] βΌ ) | ||
Theorem | rlocbas 33004 | The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ π = (π΅ Γ π) & β’ πΏ = (π RLocal π) & β’ βΌ = (π ~RL π) & β’ (π β π β π) & β’ (π β π β π΅) β β’ (π β (π / βΌ ) = (BaseβπΏ)) | ||
Theorem | rlocaddval 33005 | Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ + = (+gβπ ) & β’ πΏ = (π RLocal π) & β’ βΌ = (π ~RL π) & β’ (π β π β CRing) & β’ (π β π β (SubMndβ(mulGrpβπ ))) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π) & β’ (π β π» β π) & β’ β = (+gβπΏ) β β’ (π β ([β¨πΈ, πΊβ©] βΌ β [β¨πΉ, π»β©] βΌ ) = [β¨((πΈ Β· π») + (πΉ Β· πΊ)), (πΊ Β· π»)β©] βΌ ) | ||
Theorem | rlocmulval 33006 | Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ + = (+gβπ ) & β’ πΏ = (π RLocal π) & β’ βΌ = (π ~RL π) & β’ (π β π β CRing) & β’ (π β π β (SubMndβ(mulGrpβπ ))) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π) & β’ (π β π» β π) & β’ β = (.rβπΏ) β β’ (π β ([β¨πΈ, πΊβ©] βΌ β [β¨πΉ, π»β©] βΌ ) = [β¨(πΈ Β· πΉ), (πΊ Β· π»)β©] βΌ ) | ||
Theorem | rloccring 33007 | The ring localization πΏ of a commutative ring π by a multiplicatively closed set π is itself a commutative ring. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ + = (+gβπ ) & β’ πΏ = (π RLocal π) & β’ βΌ = (π ~RL π) & β’ (π β π β CRing) & β’ (π β π β (SubMndβ(mulGrpβπ ))) β β’ (π β πΏ β CRing) | ||
Theorem | rloc0g 33008 | The zero of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ πΏ = (π RLocal π) & β’ βΌ = (π ~RL π) & β’ (π β π β CRing) & β’ (π β π β (SubMndβ(mulGrpβπ ))) & β’ π = [β¨ 0 , 1 β©] βΌ β β’ (π β π = (0gβπΏ)) | ||
Theorem | rloc1r 33009 | The multiplicative identity of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ πΏ = (π RLocal π) & β’ βΌ = (π ~RL π) & β’ (π β π β CRing) & β’ (π β π β (SubMndβ(mulGrpβπ ))) & β’ πΌ = [β¨ 1 , 1 β©] βΌ β β’ (π β πΌ = (1rβπΏ)) | ||
Theorem | rlocf1 33010* | The embedding πΉ of a ring π into its localization πΏ. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) & β’ πΏ = (π RLocal π) & β’ βΌ = (π ~RL π) & β’ πΉ = (π₯ β π΅ β¦ [β¨π₯, 1 β©] βΌ ) & β’ (π β π β CRing) & β’ (π β π β (SubMndβ(mulGrpβπ ))) & β’ (π β π β (RLRegβπ )) β β’ (π β (πΉ:π΅β1-1β((π΅ Γ π) / βΌ ) β§ πΉ β (π RingHom πΏ))) | ||
Theorem | domnlcan 33011 | Left-cancellation law for domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β (π΅ β { 0 })) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β Domn) & β’ (π β (π Β· π) = (π Β· π)) β β’ (π β π = π) | ||
Theorem | idomrcan 33012 | Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β (π΅ β { 0 })) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β IDomn) & β’ (π β (π Β· π) = (π Β· π)) β β’ (π β π = π) | ||
Theorem | 1rrg 33013 | The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.) |
β’ 1 = (1rβπ ) & β’ πΈ = (RLRegβπ ) & β’ (π β π β Ring) β β’ (π β 1 β πΈ) | ||
Theorem | rrgnz 33014 | In a non-zero ring, the zero is not a nonzero-divisors. (Contributed by Thierry Arnoux, 6-May-2025.) |
β’ πΈ = (RLRegβπ ) & β’ 0 = (0gβπ ) β β’ (π β NzRing β Β¬ 0 β πΈ) | ||
Theorem | isdomn6 33015 | A ring is a domain iff nonzero-divisors are all the nonzero elements. (Contributed by Thierry Arnoux, 6-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ πΈ = (RLRegβπ ) & β’ 0 = (0gβπ ) β β’ (π β Domn β (π β NzRing β§ (π΅ β { 0 }) = πΈ)) | ||
Theorem | rrgsubm 33016 | The left regular elements of a ring form a submonoid of the multiplicative group. (Contributed by Thierry Arnoux, 10-May-2025.) |
β’ πΈ = (RLRegβπ ) & β’ π = (mulGrpβπ ) & β’ (π β π β Ring) β β’ (π β πΈ β (SubMndβπ)) | ||
Theorem | subrdom 33017 | A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
β’ (π β π β Domn) & β’ (π β π β (SubRingβπ )) β β’ (π β (π βΎs π) β Domn) | ||
Theorem | subridom 33018 | A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
β’ (π β π β IDomn) & β’ (π β π β (SubRingβπ )) β β’ (π β (π βΎs π) β IDomn) | ||
Theorem | subrfld 33019 | A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
β’ (π β π β Field) & β’ (π β π β (SubRingβπ )) β β’ (π β (π βΎs π) β IDomn) | ||
Syntax | ceuf 33020 | Declare the syntax for the Euclidean function index extractor. |
class EuclF | ||
Definition | df-euf 33021 | Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33023 instead. (New usage is discouraged.) |
β’ EuclF = Slot ;21 | ||
Theorem | eufndx 33022 | Index value of the Euclidean function slot. Use ndxarg 17159. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.) |
β’ (EuclFβndx) = ;21 | ||
Theorem | eufid 33023 | Utility theorem: index-independent form of df-euf 33021. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ EuclF = Slot (EuclFβndx) | ||
Syntax | cedom 33024 | Declare the syntax for the Euclidean Domain. |
class EDomn | ||
Definition | df-edom 33025* | Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ EDomn = {π β IDomn β£ [(EuclFβπ) / π][(Baseβπ) / π£](Fun π β§ (π β (π£ β {(0gβπ)})) β (0[,)+β) β§ βπ β π£ βπ β (π£ β {(0gβπ)})βπ β π£ βπ β π£ (π = ((π(.rβπ)π)(+gβπ)π) β§ (π = (0gβπ) β¨ (πβπ) < (πβπ))))} | ||
Theorem | ringinveu 33026 | If a ring unit element π admits both a left inverse π and a right inverse π, they are equal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ Β· = (.rβπ ) & β’ π = (Unitβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π Β· π) = 1 ) & β’ (π β (π Β· π) = 1 ) β β’ (π β π = π) | ||
Theorem | isdrng4 33027* | A division ring is a ring in which 1 β 0 and every nonzero element has a left and right inverse. (Contributed by Thierry Arnoux, 2-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ Β· = (.rβπ ) & β’ π = (Unitβπ ) & β’ (π β π β Ring) β β’ (π β (π β DivRing β ( 1 β 0 β§ βπ₯ β (π΅ β { 0 })βπ¦ β π΅ ((π₯ Β· π¦) = 1 β§ (π¦ Β· π₯) = 1 )))) | ||
Theorem | rndrhmcl 33028 | The image of a division ring by a ring homomorphism is a division ring. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ π = (π βΎs ran πΉ) & β’ 0 = (0gβπ) & β’ (π β πΉ β (π RingHom π)) & β’ (π β ran πΉ β { 0 }) & β’ (π β π β DivRing) β β’ (π β π β DivRing) | ||
Theorem | sdrgdvcl 33029 | A sub-division-ring is closed under the ring division operation. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
β’ / = (/rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π΄ β (SubDRingβπ )) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β 0 ) β β’ (π β (π / π) β π΄) | ||
Theorem | sdrginvcl 33030 | A sub-division-ring is closed under the ring inverse operation. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
β’ πΌ = (invrβπ ) & β’ 0 = (0gβπ ) β β’ ((π΄ β (SubDRingβπ ) β§ π β π΄ β§ π β 0 ) β (πΌβπ) β π΄) | ||
Theorem | primefldchr 33031 | The characteristic of a prime field is the same as the characteristic of the main field. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π = (π βΎs β© (SubDRingβπ )) β β’ (π β DivRing β (chrβπ) = (chrβπ )) | ||
Syntax | cfrac 33032 | Syntax for the field of fractions of a given integral domain. |
class Frac | ||
Definition | df-frac 33033 | Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.) |
β’ Frac = (π β V β¦ (π RLocal (RLRegβπ))) | ||
Theorem | fracval 33034 | Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.) |
β’ ( Frac βπ ) = (π RLocal (RLRegβπ )) | ||
Theorem | fracbas 33035 | The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ πΈ = (RLRegβπ ) & β’ πΉ = ( Frac βπ ) & β’ βΌ = (π ~RL πΈ) β β’ ((π΅ Γ πΈ) / βΌ ) = (BaseβπΉ) | ||
Theorem | fracerl 33036 | Rewrite the ring localization equivalence relation in the case of a field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ βΌ = (π ~RL (RLRegβπ )) & β’ (π β π β CRing) & β’ (π β πΈ β π΅) & β’ (π β πΊ β π΅) & β’ (π β πΉ β (RLRegβπ )) & β’ (π β π» β (RLRegβπ )) β β’ (π β (β¨πΈ, πΉβ© βΌ β¨πΊ, π»β© β (πΈ Β· π») = (πΊ Β· πΉ))) | ||
Theorem | fracf1 33037* | The embedding of a commutative ring π into its field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ πΈ = (RLRegβπ ) & β’ 1 = (1rβπ ) & β’ (π β π β CRing) & β’ βΌ = (π ~RL πΈ) & β’ πΉ = (π₯ β π΅ β¦ [β¨π₯, 1 β©] βΌ ) β β’ (π β (πΉ:π΅β1-1β((π΅ Γ πΈ) / βΌ ) β§ πΉ β (π RingHom ( Frac βπ )))) | ||
Theorem | fracfld 33038 | The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ (π β π β IDomn) β β’ (π β ( Frac βπ ) β Field) | ||
Theorem | idomsubr 33039* | Every integral domain is isomorphic with a subring of some field. (Proposed by Gerard Lang, 10-May-2025.) (Contributed by Thierry Arnoux, 10-May-2025.) |
β’ (π β π β IDomn) β β’ (π β βπ β Field βπ β (SubRingβπ)π βπ (π βΎs π )) | ||
Syntax | cfldgen 33040 | Syntax for a function generating sub-fields. |
class fldGen | ||
Definition | df-fldgen 33041* | Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg 33044). If the base structure is a field, this is a subfield (see fldgenfld 33050 and fldsdrgfld 20685). In general this will be used in the context of fields, hence the name fldGen. (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025.) |
β’ fldGen = (π β V, π β V β¦ β© {π β (SubDRingβπ) β£ π β π}) | ||
Theorem | fldgenval 33042* | Value of the field generating function: (πΉ fldGen π) is the smallest sub-division-ring of πΉ containing π. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β (πΉ fldGen π) = β© {π β (SubDRingβπΉ) β£ π β π}) | ||
Theorem | fldgenssid 33043 | The field generated by a set of elements contains those elements. See lspssid 20868. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β π β (πΉ fldGen π)) | ||
Theorem | fldgensdrg 33044 | A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β (πΉ fldGen π) β (SubDRingβπΉ)) | ||
Theorem | fldgenssv 33045 | A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β (πΉ fldGen π) β π΅) | ||
Theorem | fldgenss 33046 | Generated subfields preserve subset ordering. ( see lspss 20867 and spanss 31197) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) & β’ (π β π β π) β β’ (π β (πΉ fldGen π) β (πΉ fldGen π)) | ||
Theorem | fldgenidfld 33047 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β (SubDRingβπΉ)) β β’ (π β (πΉ fldGen π) = π) | ||
Theorem | fldgenssp 33048 | The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β (SubDRingβπΉ)) & β’ (π β π β π) β β’ (π β (πΉ fldGen π) β π) | ||
Theorem | fldgenid 33049 | The subfield of a field πΉ generated by the whole base set of πΉ is πΉ itself. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) β β’ (π β (πΉ fldGen π΅) = π΅) | ||
Theorem | fldgenfld 33050 | A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β Field) & β’ (π β π β π΅) β β’ (π β (πΉ βΎs (πΉ fldGen π)) β Field) | ||
Theorem | primefldgen1 33051 | The prime field of a division ring is the subfield generated by the multiplicative identity element. In general, we should write "prime division ring", but since most later usages are in the case where the ambient ring is commutative, we keep the term "prime field". (Contributed by Thierry Arnoux, 11-Jan-2025.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) & β’ (π β π β DivRing) β β’ (π β β© (SubDRingβπ ) = (π fldGen { 1 })) | ||
Theorem | 1fldgenq 33052 | The field of rational numbers β is generated by 1 in βfld, that is, β is the prime field of βfld. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
β’ (βfld fldGen {1}) = β | ||
Syntax | corng 33053 | Extend class notation with the class of all ordered rings. |
class oRing | ||
Syntax | cofld 33054 | Extend class notation with the class of all ordered fields. |
class oField | ||
Definition | df-orng 33055* | Define class of all ordered rings. An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ oRing = {π β (Ring β© oGrp) β£ [(Baseβπ) / π£][(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π))} | ||
Definition | df-ofld 33056 | Define class of all ordered fields. An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.) |
β’ oField = (Field β© oRing) | ||
Theorem | isorng 33057* | An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β€ = (leβπ ) β β’ (π β oRing β (π β Ring β§ π β oGrp β§ βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) | ||
Theorem | orngring 33058 | An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ (π β oRing β π β Ring) | ||
Theorem | orngogrp 33059 | An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ (π β oRing β π β oGrp) | ||
Theorem | isofld 33060 | An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ (πΉ β oField β (πΉ β Field β§ πΉ β oRing)) | ||
Theorem | orngmul 33061 | In an ordered ring, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ π΅ = (Baseβπ ) & β’ β€ = (leβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β oRing β§ (π β π΅ β§ 0 β€ π) β§ (π β π΅ β§ 0 β€ π)) β 0 β€ (π Β· π)) | ||
Theorem | orngsqr 33062 | In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ π΅ = (Baseβπ ) & β’ β€ = (leβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β oRing β§ π β π΅) β 0 β€ (π Β· π)) | ||
Theorem | ornglmulle 33063 | In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β oRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ β€ = (leβπ ) & β’ (π β π β€ π) & β’ (π β 0 β€ π) β β’ (π β (π Β· π) β€ (π Β· π)) | ||
Theorem | orngrmulle 33064 | In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β oRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ β€ = (leβπ ) & β’ (π β π β€ π) & β’ (π β 0 β€ π) β β’ (π β (π Β· π) β€ (π Β· π)) | ||
Theorem | ornglmullt 33065 | In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β oRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ < = (ltβπ ) & β’ (π β π β DivRing) & β’ (π β π < π) & β’ (π β 0 < π) β β’ (π β (π Β· π) < (π Β· π)) | ||
Theorem | orngrmullt 33066 | In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β oRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ < = (ltβπ ) & β’ (π β π β DivRing) & β’ (π β π < π) & β’ (π β 0 < π) β β’ (π β (π Β· π) < (π Β· π)) | ||
Theorem | orngmullt 33067 | In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ (π β π β oRing) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ (π β 0 < π) β β’ (π β 0 < (π Β· π)) | ||
Theorem | ofldfld 33068 | An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ (πΉ β oField β πΉ β Field) | ||
Theorem | ofldtos 33069 | An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ (πΉ β oField β πΉ β Toset) | ||
Theorem | orng0le1 33070 | In an ordered ring, the ring unity is positive. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ 0 = (0gβπΉ) & β’ 1 = (1rβπΉ) & β’ β€ = (leβπΉ) β β’ (πΉ β oRing β 0 β€ 1 ) | ||
Theorem | ofldlt1 33071 | In an ordered field, the ring unity is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ 0 = (0gβπΉ) & β’ 1 = (1rβπΉ) & β’ < = (ltβπΉ) β β’ (πΉ β oField β 0 < 1 ) | ||
Theorem | ofldchr 33072 | The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018.) (Proof shortened by AV, 6-Oct-2020.) |
β’ (πΉ β oField β (chrβπΉ) = 0) | ||
Theorem | suborng 33073 | Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ ((π β oRing β§ (π βΎs π΄) β Ring) β (π βΎs π΄) β oRing) | ||
Theorem | subofld 33074 | Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ ((πΉ β oField β§ (πΉ βΎs π΄) β Field) β (πΉ βΎs π΄) β oField) | ||
Theorem | isarchiofld 33075* | Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
β’ π΅ = (Baseβπ) & β’ π» = (β€RHomβπ) & β’ < = (ltβπ) β β’ (π β oField β (π β Archi β βπ₯ β π΅ βπ β β π₯ < (π»βπ))) | ||
Theorem | rhmdvd 33076 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
β’ π = (Unitβπ) & β’ π = (Baseβπ ) & β’ / = (/rβπ) & β’ Β· = (.rβπ ) β β’ ((πΉ β (π RingHom π) β§ (π΄ β π β§ π΅ β π β§ πΆ β π) β§ ((πΉβπ΅) β π β§ (πΉβπΆ) β π)) β ((πΉβπ΄) / (πΉβπ΅)) = ((πΉβ(π΄ Β· πΆ)) / (πΉβ(π΅ Β· πΆ)))) | ||
Theorem | kerunit 33077 | If a unit element lies in the kernel of a ring homomorphism, then 0 = 1, i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017.) |
β’ π = (Unitβπ ) & β’ 0 = (0gβπ) & β’ 1 = (1rβπ) β β’ ((πΉ β (π RingHom π) β§ (π β© (β‘πΉ β { 0 })) β β ) β 1 = 0 ) | ||
Syntax | cresv 33078 | Extend class notation with the scalar restriction operation. |
class βΎv | ||
Definition | df-resv 33079* | Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.) |
β’ βΎv = (π€ β V, π₯ β V β¦ if((Baseβ(Scalarβπ€)) β π₯, π€, (π€ sSet β¨(Scalarβndx), ((Scalarβπ€) βΎs π₯)β©))) | ||
Theorem | reldmresv 33080 | The scalar restriction is a proper operator, so it can be used with ovprc1 7452. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ Rel dom βΎv | ||
Theorem | resvval 33081 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((π β π β§ π΄ β π) β π = if(π΅ β π΄, π, (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©))) | ||
Theorem | resvid2 33082 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((π΅ β π΄ β§ π β π β§ π΄ β π) β π = π) | ||
Theorem | resvval2 33083 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((Β¬ π΅ β π΄ β§ π β π β§ π΄ β π) β π = (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©)) | ||
Theorem | resvsca 33084 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ (π΄ β π β (πΉ βΎs π΄) = (Scalarβπ )) | ||
Theorem | resvlem 33085 | Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π = (π βΎv π΄) & β’ πΆ = (πΈβπ) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (Scalarβndx) β β’ (π΄ β π β πΆ = (πΈβπ )) | ||
Theorem | resvlemOLD 33086 | Obsolete version of resvlem 33085 as of 31-Oct-2024. Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (π βΎv π΄) & β’ πΆ = (πΈβπ) & β’ πΈ = Slot π & β’ π β β & β’ π β 5 β β’ (π΄ β π β πΆ = (πΈβπ )) | ||
Theorem | resvbas 33087 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ = (Baseβπ»)) | ||
Theorem | resvbasOLD 33088 | Obsolete proof of resvbas 33087 as of 31-Oct-2024. Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (πΊ βΎv π΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ = (Baseβπ»)) | ||
Theorem | resvplusg 33089 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ + = (+gβπΊ) β β’ (π΄ β π β + = (+gβπ»)) | ||
Theorem | resvplusgOLD 33090 | Obsolete proof of resvplusg 33089 as of 31-Oct-2024. +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (πΊ βΎv π΄) & β’ + = (+gβπΊ) β β’ (π΄ β π β + = (+gβπ»)) | ||
Theorem | resvvsca 33091 | Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = ( Β·π βπΊ) β β’ (π΄ β π β Β· = ( Β·π βπ»)) | ||
Theorem | resvvscaOLD 33092 | Obsolete proof of resvvsca 33091 as of 31-Oct-2024. Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = ( Β·π βπΊ) β β’ (π΄ β π β Β· = ( Β·π βπ»)) | ||
Theorem | resvmulr 33093 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = (.rβπΊ) β β’ (π΄ β π β Β· = (.rβπ»)) | ||
Theorem | resvmulrOLD 33094 | Obsolete proof of resvmulr 33093 as of 31-Oct-2024. Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = (.rβπΊ) β β’ (π΄ β π β Β· = (.rβπ»)) | ||
Theorem | resv0g 33095 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π» = (πΊ βΎv π΄) & β’ 0 = (0gβπΊ) β β’ (π΄ β π β 0 = (0gβπ»)) | ||
Theorem | resv1r 33096 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π» = (πΊ βΎv π΄) & β’ 1 = (1rβπΊ) β β’ (π΄ β π β 1 = (1rβπ»)) | ||
Theorem | resvcmn 33097 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π» = (πΊ βΎv π΄) β β’ (π΄ β π β (πΊ β CMnd β π» β CMnd)) | ||
Theorem | gzcrng 33098 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
β’ (βfld βΎs β€[i]) β CRing | ||
Theorem | reofld 33099 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ βfld β oField | ||
Theorem | nn0omnd 33100 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ (βfld βΎs β0) β oMnd |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |