HomeTheorem List (p. 330 of 482)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 330 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: | Metamath Proof Explorer
(1-30715) |
Hilbert Space Explorer
(30716-32238) |
Users' Mathboxes
(32239-48161) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | slmdvsdir 32901 | Distributive law for scalar product. (ax-hvdistr1 30805 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) β β’ ((π β SLMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π ⨣ π ) Β· π) = ((π Β· π) + (π Β· π))) | ||
| Theorem | slmdvsass 32902 | Associative law for scalar product. (ax-hvmulass 30804 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ Γ = (.rβπΉ) β β’ ((π β SLMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Γ π ) Β· π) = (π Β· (π Β· π))) | ||
| Theorem | slmd0cl 32903 | The ring zero in a semimodule belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπΉ) β β’ (π β SLMod β 0 β πΎ) | ||
| Theorem | slmd1cl 32904 | The ring unity in a semiring left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ 1 = (1rβπΉ) β β’ (π β SLMod β 1 β πΎ) | ||
| Theorem | slmdvs1 32905 | Scalar product with ring unity. (ax-hvmulid 30803 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπΉ) β β’ ((π β SLMod β§ π β π) β ( 1 Β· π) = π) | ||
| Theorem | slmd0vcl 32906 | The zero vector is a vector. (ax-hv0cl 30800 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ (π β SLMod β 0 β π) | ||
| Theorem | slmd0vlid 32907 | Left identity law for the zero vector. (hvaddlid 30820 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β SLMod β§ π β π) β ( 0 + π) = π) | ||
| Theorem | slmd0vrid 32908 | Right identity law for the zero vector. (ax-hvaddid 30801 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β SLMod β§ π β π) β (π + 0 ) = π) | ||
| Theorem | slmd0vs 32909 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 30807 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (0gβπΉ) & β’ 0 = (0gβπ) β β’ ((π β SLMod β§ π β π) β (π Β· π) = 0 ) | ||
| Theorem | slmdvs0 32910 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 30821 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπ) β β’ ((π β SLMod β§ π β πΎ) β (π Β· 0 ) = 0 ) | ||
| Theorem | gsumvsca1 32911* | Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018.) |
| β’ π΅ = (Baseβπ) & β’ πΊ = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ (π β πΎ β (BaseβπΊ)) & β’ (π β π΄ β Fin) & β’ (π β π β SLMod) & β’ (π β π β πΎ) & β’ ((π β§ π β π΄) β π β π΅) β β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))) | ||
| Theorem | gsumvsca2 32912* | Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018.) (Proof shortened by AV, 12-Dec-2019.) |
| β’ π΅ = (Baseβπ) & β’ πΊ = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ (π β πΎ β (BaseβπΊ)) & β’ (π β π΄ β Fin) & β’ (π β π β SLMod) & β’ (π β π β π΅) & β’ ((π β§ π β π΄) β π β πΎ) β β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = ((πΊ Ξ£g (π β π΄ β¦ π)) Β· π)) | ||
| Theorem | prmsimpcyc 32913 | A group of prime order is cyclic if and only if it is simple. This is the first family of finite simple groups. (Contributed by Thierry Arnoux, 21-Sep-2023.) |
| β’ π΅ = (BaseβπΊ) β β’ ((β―βπ΅) β β β (πΊ β SimpGrp β πΊ β CycGrp)) | ||
| Theorem | domnlcan 32914 | Left-cancellation law for domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β (π΅ β { 0 })) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β Domn) & β’ (π β (π Β· π) = (π Β· π)) β β’ (π β π = π) | ||
| Theorem | idomrcan 32915 | Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β (π΅ β { 0 })) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β IDomn) & β’ (π β (π Β· π) = (π Β· π)) β β’ (π β π = π) | ||
| Theorem | urpropd 32916* | Sufficient condition for ring unities to be equal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΅ = (Baseβπ)) & β’ (((π β§ π₯ β π΅) β§ π¦ β π΅) β (π₯(.rβπ)π¦) = (π₯(.rβπ)π¦)) β β’ (π β (1rβπ) = (1rβπ)) | ||
| Theorem | 0ringsubrg 32917 | A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| β’ π΅ = (Baseβπ ) & β’ (π β π β Ring) & β’ (π β (β―βπ΅) = 1) & β’ (π β π β (SubRingβπ )) β β’ (π β (β―βπ) = 1) | ||
| Theorem | frobrhm 32918* | In a commutative ring with prime characteristic, the Frobenius function πΉ is a ring endomorphism, thus named the Frobenius endomorphism. (Contributed by Thierry Arnoux, 31-May-2024.) |
| β’ π΅ = (Baseβπ ) & β’ π = (chrβπ ) & β’ β = (.gβ(mulGrpβπ )) & β’ πΉ = (π₯ β π΅ β¦ (π β π₯)) & β’ (π β π β CRing) & β’ (π β π β β) β β’ (π β πΉ β (π RingHom π )) | ||
| Theorem | ress1r 32919 | 1r is unaffected by restriction. This is a bit more generic than subrg1 20510. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ 1 β π΄ β§ π΄ β π΅) β 1 = (1rβπ)) | ||
| Theorem | ringinvval 32920* | The ring inverse expressed in terms of multiplication. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
| β’ π΅ = (Baseβπ ) & β’ β = (.rβπ ) & β’ 1 = (1rβπ ) & β’ π = (invrβπ ) & β’ π = (Unitβπ ) β β’ ((π β Ring β§ π β π) β (πβπ) = (β©π¦ β π (π¦ β π) = 1 )) | ||
| Theorem | dvrcan5 32921 | Cancellation law for common factor in ratio. (divcan5 11938 analog.) (Contributed by Thierry Arnoux, 26-Oct-2016.) |
| β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β· π) / (π Β· π)) = (π / π)) | ||
| Theorem | subrgchr 32922 | If π΄ is a subring of π , then they have the same characteristic. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
| β’ (π΄ β (SubRingβπ ) β (chrβ(π βΎs π΄)) = (chrβπ )) | ||
| Theorem | rmfsupp2 32923* | A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by Thierry Arnoux, 3-Jun-2023.) |
| β’ π = (Baseβπ) & β’ (π β π β Ring) & β’ (π β π β π) & β’ ((π β§ π£ β π) β πΆ β π ) & β’ (π β π΄:πβΆπ ) & β’ (π β π΄ finSupp (0gβπ)) β β’ (π β (π£ β π β¦ ((π΄βπ£)(.rβπ)πΆ)) finSupp (0gβπ)) | ||
| Theorem | unitnz 32924 | In a nonzero ring, a unit cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β NzRing) & β’ (π β π β π) β β’ (π β π β 0 ) | ||
| Syntax | ceuf 32925 | Declare the syntax for the Euclidean function index extractor. |
| class EuclF | ||
| Definition | df-euf 32926 | Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 32928 instead. (New usage is discouraged.) |
| β’ EuclF = Slot ;21 | ||
| Theorem | eufndx 32927 | Index value of the Euclidean function slot. Use ndxarg 17156. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.) |
| β’ (EuclFβndx) = ;21 | ||
| Theorem | eufid 32928 | Utility theorem: index-independent form of df-euf 32926. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ EuclF = Slot (EuclFβndx) | ||
| Syntax | cedom 32929 | Declare the syntax for the Euclidean Domain. |
| class EDomn | ||
| Definition | df-edom 32930* | Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ EDomn = {π β IDomn β£ [(EuclFβπ) / π][(Baseβπ) / π£](Fun π β§ (π β (π£ β {(0gβπ)})) β (0[,)+β) β§ βπ β π£ βπ β (π£ β {(0gβπ)})βπ β π£ βπ β π£ (π = ((π(.rβπ)π)(+gβπ)π) β§ (π = (0gβπ) β¨ (πβπ) < (πβπ))))} | ||
| Theorem | ringinveu 32931 | 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 32932* | 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 32933 | 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 32934 | 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 32935 | 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 32936 | 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 | cfldgen 32937 | Syntax for a function generating sub-fields. |
| class fldGen | ||
| Definition | df-fldgen 32938* | 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 32941). If the base structure is a field, this is a subfield (see fldgenfld 32947 and fldsdrgfld 20675). 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 32939* | 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 32940 | The field generated by a set of elements contains those elements. See lspssid 20858. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β π β (πΉ fldGen π)) | ||
| Theorem | fldgensdrg 32941 | A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β (πΉ fldGen π) β (SubDRingβπΉ)) | ||
| Theorem | fldgenssv 32942 | A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β (πΉ fldGen π) β π΅) | ||
| Theorem | fldgenss 32943 | Generated subfields preserve subset ordering. ( see lspss 20857 and spanss 31145) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) & β’ (π β π β π) β β’ (π β (πΉ fldGen π) β (πΉ fldGen π)) | ||
| Theorem | fldgenidfld 32944 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β (SubDRingβπΉ)) β β’ (π β (πΉ fldGen π) = π) | ||
| Theorem | fldgenssp 32945 | 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 32946 | 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 32947 | A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β Field) & β’ (π β π β π΅) β β’ (π β (πΉ βΎs (πΉ fldGen π)) β Field) | ||
| Theorem | primefldgen1 32948 | 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 32949 | 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 32950 | Extend class notation with the class of all ordered rings. |
| class oRing | ||
| Syntax | cofld 32951 | Extend class notation with the class of all ordered fields. |
| class oField | ||
| Definition | df-orng 32952* | 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 32953 | 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 32954* | 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 32955 | An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ (π β oRing β π β Ring) | ||
| Theorem | orngogrp 32956 | An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ (π β oRing β π β oGrp) | ||
| Theorem | isofld 32957 | 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 32958 | 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 32959 | In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ π΅ = (Baseβπ ) & β’ β€ = (leβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β oRing β§ π β π΅) β 0 β€ (π Β· π)) | ||
| Theorem | ornglmulle 32960 | 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 32961 | 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 32962 | 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 32963 | 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 32964 | 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 32965 | An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ (πΉ β oField β πΉ β Field) | ||
| Theorem | ofldtos 32966 | An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ (πΉ β oField β πΉ β Toset) | ||
| Theorem | orng0le1 32967 | 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 32968 | 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 32969 | 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 32970 | 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 32971 | 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 32972* | 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 32973 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| β’ π = (Unitβπ) & β’ π = (Baseβπ ) & β’ / = (/rβπ) & β’ Β· = (.rβπ ) β β’ ((πΉ β (π RingHom π) β§ (π΄ β π β§ π΅ β π β§ πΆ β π) β§ ((πΉβπ΅) β π β§ (πΉβπΆ) β π)) β ((πΉβπ΄) / (πΉβπ΅)) = ((πΉβ(π΄ Β· πΆ)) / (πΉβ(π΅ Β· πΆ)))) | ||
| Theorem | kerunit 32974 | 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 32975 | Extend class notation with the scalar restriction operation. |
| class βΎv | ||
| Definition | df-resv 32976* | 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 32977 | The scalar restriction is a proper operator, so it can be used with ovprc1 7453. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ Rel dom βΎv | ||
| Theorem | resvval 32978 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((π β π β§ π΄ β π) β π = if(π΅ β π΄, π, (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©))) | ||
| Theorem | resvid2 32979 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((π΅ β π΄ β§ π β π β§ π΄ β π) β π = π) | ||
| Theorem | resvval2 32980 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((Β¬ π΅ β π΄ β§ π β π β§ π΄ β π) β π = (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©)) | ||
| Theorem | resvsca 32981 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ (π΄ β π β (πΉ βΎs π΄) = (Scalarβπ )) | ||
| Theorem | resvlem 32982 | 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 32983 | Obsolete version of resvlem 32982 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 32984 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| β’ π» = (πΊ βΎv π΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ = (Baseβπ»)) | ||
| Theorem | resvbasOLD 32985 | Obsolete proof of resvbas 32984 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 32986 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| β’ π» = (πΊ βΎv π΄) & β’ + = (+gβπΊ) β β’ (π΄ β π β + = (+gβπ»)) | ||
| Theorem | resvplusgOLD 32987 | Obsolete proof of resvplusg 32986 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 32988 | Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
| β’ π» = (πΊ βΎv π΄) & β’ Β· = ( Β·π βπΊ) β β’ (π΄ β π β Β· = ( Β·π βπ»)) | ||
| Theorem | resvvscaOLD 32989 | Obsolete proof of resvvsca 32988 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 32990 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| β’ π» = (πΊ βΎv π΄) & β’ Β· = (.rβπΊ) β β’ (π΄ β π β Β· = (.rβπ»)) | ||
| Theorem | resvmulrOLD 32991 | Obsolete proof of resvmulr 32990 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 32992 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π» = (πΊ βΎv π΄) & β’ 0 = (0gβπΊ) β β’ (π΄ β π β 0 = (0gβπ»)) | ||
| Theorem | resv1r 32993 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π» = (πΊ βΎv π΄) & β’ 1 = (1rβπΊ) β β’ (π΄ β π β 1 = (1rβπ»)) | ||
| Theorem | resvcmn 32994 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π» = (πΊ βΎv π΄) β β’ (π΄ β π β (πΊ β CMnd β π» β CMnd)) | ||
| Theorem | gzcrng 32995 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
| β’ (βfld βΎs β€[i]) β CRing | ||
| Theorem | reofld 32996 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| β’ βfld β oField | ||
| Theorem | nn0omnd 32997 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ (βfld βΎs β0) β oMnd | ||
| Theorem | rearchi 32998 | The field of the real numbers is Archimedean. See also arch 12491. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| β’ βfld β Archi | ||
| Theorem | nn0archi 32999 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
| β’ (βfld βΎs β0) β Archi | ||
| Theorem | xrge0slmod 33000 | The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ πΊ = (β*π βΎs (0[,]+β)) & β’ π = (πΊ βΎv (0[,)+β)) β β’ π β SLMod | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |