![]() |
Metamath
Proof Explorer Theorem List (p. 211 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnsubrglem 21001* | Lemma for resubdrg 21167 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ (π₯ β π΄ β π₯ β β) & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ + π¦) β π΄) & β’ (π₯ β π΄ β -π₯ β π΄) & β’ 1 β π΄ & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ Β· π¦) β π΄) β β’ π΄ β (SubRingββfld) | ||
Theorem | cnsubdrglem 21002* | Lemma for resubdrg 21167 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ (π₯ β π΄ β π₯ β β) & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ + π¦) β π΄) & β’ (π₯ β π΄ β -π₯ β π΄) & β’ 1 β π΄ & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ Β· π¦) β π΄) & β’ ((π₯ β π΄ β§ π₯ β 0) β (1 / π₯) β π΄) β β’ (π΄ β (SubRingββfld) β§ (βfld βΎs π΄) β DivRing) | ||
Theorem | qsubdrg 21003 | The rational numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ (β β (SubRingββfld) β§ (βfld βΎs β) β DivRing) | ||
Theorem | zsubrg 21004 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ β€ β (SubRingββfld) | ||
Theorem | gzsubrg 21005 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ β€[i] β (SubRingββfld) | ||
Theorem | nn0subm 21006 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ β0 β (SubMndββfld) | ||
Theorem | rege0subm 21007 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (0[,)+β) β (SubMndββfld) | ||
Theorem | absabv 21008 | The regular absolute value function on the complex numbers is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ abs β (AbsValββfld) | ||
Theorem | zsssubrg 21009 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β (SubRingββfld) β β€ β π ) | ||
Theorem | qsssubdrg 21010 | The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π β (SubRingββfld) β§ (βfld βΎs π ) β DivRing) β β β π ) | ||
Theorem | cnsubrg 21011 | There are no subrings of the complex numbers strictly between β and β. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π β (SubRingββfld) β§ β β π ) β π β {β, β}) | ||
Theorem | cnmgpabl 21012 | The unit group of the complex numbers is an abelian group. (Contributed by Mario Carneiro, 21-Jun-2015.) |
β’ π = ((mulGrpββfld) βΎs (β β {0})) β β’ π β Abel | ||
Theorem | cnmgpid 21013 | The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007.) (Revised by AV, 26-Aug-2021.) |
β’ π = ((mulGrpββfld) βΎs (β β {0})) β β’ (0gβπ) = 1 | ||
Theorem | cnmsubglem 21014* | Lemma for rpmsubg 21015 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.) |
β’ π = ((mulGrpββfld) βΎs (β β {0})) & β’ (π₯ β π΄ β π₯ β β) & β’ (π₯ β π΄ β π₯ β 0) & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ Β· π¦) β π΄) & β’ 1 β π΄ & β’ (π₯ β π΄ β (1 / π₯) β π΄) β β’ π΄ β (SubGrpβπ) | ||
Theorem | rpmsubg 21015 | The positive reals form a multiplicative subgroup of the complex numbers. (Contributed by Mario Carneiro, 21-Jun-2015.) |
β’ π = ((mulGrpββfld) βΎs (β β {0})) β β’ β+ β (SubGrpβπ) | ||
Theorem | gzrngunitlem 21016 | Lemma for gzrngunit 21017. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (βfld βΎs β€[i]) β β’ (π΄ β (Unitβπ) β 1 β€ (absβπ΄)) | ||
Theorem | gzrngunit 21017 | The units on β€[i] are the gaussian integers with norm 1. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (βfld βΎs β€[i]) β β’ (π΄ β (Unitβπ) β (π΄ β β€[i] β§ (absβπ΄) = 1)) | ||
Theorem | gsumfsum 21018* | Relate a group sum on βfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (βfld Ξ£g (π β π΄ β¦ π΅)) = Ξ£π β π΄ π΅) | ||
Theorem | regsumfsum 21019* | Relate a group sum on (βfld βΎs β) to a finite sum on the reals. Cf. gsumfsum 21018. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β ((βfld βΎs β) Ξ£g (π β π΄ β¦ π΅)) = Ξ£π β π΄ π΅) | ||
Theorem | expmhm 21020* | Exponentiation is a monoid homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π = (βfld βΎs β0) & β’ π = (mulGrpββfld) β β’ (π΄ β β β (π₯ β β0 β¦ (π΄βπ₯)) β (π MndHom π)) | ||
Theorem | nn0srg 21021 | The nonnegative integers form a semiring (commutative by subcmn 19707). (Contributed by Thierry Arnoux, 1-May-2018.) |
β’ (βfld βΎs β0) β SRing | ||
Theorem | rge0srg 21022 | The nonnegative real numbers form a semiring (commutative by subcmn 19707). (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ (βfld βΎs (0[,)+β)) β SRing | ||
According to Wikipedia ("Integer", 25-May-2019, https://en.wikipedia.org/wiki/Integer) "The integers form a unital ring which is the most basic one, in the following sense: for any unital ring, there is a unique ring homomorphism from the integers into this ring. This universal property, namely to be an initial object in the category of [unital] rings, characterizes the ring π." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by (βfld βΎs β€), the field of complex numbers restricted to the integers. In zringring 21026 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 21043), and zringbas 21029 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 21024 of the ring of integers. Remark: Instead of using the symbol "ZZrng" analogous to βfld used for the field of complex numbers, we have chosen the version with an "i" to indicate that the ring of integers is a unital ring, see also Wikipedia ("Rng (algebra)", 9-Jun-2019, https://en.wikipedia.org/wiki/Rng_(algebra) 21024). | ||
Syntax | czring 21023 | Extend class notation with the (unital) ring of integers. |
class β€ring | ||
Definition | df-zring 21024 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
β’ β€ring = (βfld βΎs β€) | ||
Theorem | zringcrng 21025 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
β’ β€ring β CRing | ||
Theorem | zringring 21026 | The ring of integers is a ring. (Contributed by AV, 20-May-2019.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 13-Jun-2019.) |
β’ β€ring β Ring | ||
Theorem | zringabl 21027 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
β’ β€ring β Abel | ||
Theorem | zringgrp 21028 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
β’ β€ring β Grp | ||
Theorem | zringbas 21029 | The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.) |
β’ β€ = (Baseββ€ring) | ||
Theorem | zringplusg 21030 | The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
β’ + = (+gββ€ring) | ||
Theorem | zringsub 21031 | The subtraction of elements in the ring of integers. (Contributed by AV, 24-Mar-2025.) |
β’ β = (-gββ€ring) β β’ ((π β β€ β§ π β β€) β (π β π) = (π β π)) | ||
Theorem | zringmulg 21032 | The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.) |
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄(.gββ€ring)π΅) = (π΄ Β· π΅)) | ||
Theorem | zringmulr 21033 | The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
β’ Β· = (.rββ€ring) | ||
Theorem | zring0 21034 | The zero element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
β’ 0 = (0gββ€ring) | ||
Theorem | zring1 21035 | The unity element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
β’ 1 = (1rββ€ring) | ||
Theorem | zringnzr 21036 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
β’ β€ring β NzRing | ||
Theorem | dvdsrzring 21037 | Ring divisibility in the ring of integers corresponds to ordinary divisibility in β€. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) |
β’ β₯ = (β₯rββ€ring) | ||
Theorem | zringlpirlem1 21038 | Lemma for zringlpir 21043. A nonzero ideal of integers contains some positive integers. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) |
β’ (π β πΌ β (LIdealββ€ring)) & β’ (π β πΌ β {0}) β β’ (π β (πΌ β© β) β β ) | ||
Theorem | zringlpirlem2 21039 | Lemma for zringlpir 21043. A nonzero ideal of integers contains the least positive element. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Revised by AV, 27-Sep-2020.) |
β’ (π β πΌ β (LIdealββ€ring)) & β’ (π β πΌ β {0}) & β’ πΊ = inf((πΌ β© β), β, < ) β β’ (π β πΊ β πΌ) | ||
Theorem | zringlpirlem3 21040 | Lemma for zringlpir 21043. All elements of a nonzero ideal of integers are divided by the least one. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 27-Sep-2020.) |
β’ (π β πΌ β (LIdealββ€ring)) & β’ (π β πΌ β {0}) & β’ πΊ = inf((πΌ β© β), β, < ) & β’ (π β π β πΌ) β β’ (π β πΊ β₯ π) | ||
Theorem | zringinvg 21041 | The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ (π΄ β β€ β -π΄ = ((invgββ€ring)βπ΄)) | ||
Theorem | zringunit 21042 | The units of β€ are the integers with norm 1, i.e. 1 and -1. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
β’ (π΄ β (Unitββ€ring) β (π΄ β β€ β§ (absβπ΄) = 1)) | ||
Theorem | zringlpir 21043 | The integers are a principal ideal ring. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 27-Sep-2020.) |
β’ β€ring β LPIR | ||
Theorem | zringndrg 21044 | The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.) |
β’ β€ring β DivRing | ||
Theorem | zringcyg 21045 | The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.) |
β’ β€ring β CycGrp | ||
Theorem | zringsubgval 21046 | Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.) |
β’ β = (-gββ€ring) β β’ ((π β β€ β§ π β β€) β (π β π) = (π β π)) | ||
Theorem | zringmpg 21047 | The multiplicative group of the ring of integers is the restriction of the multiplicative group of the complex numbers to the integers. (Contributed by AV, 15-Jun-2019.) |
β’ ((mulGrpββfld) βΎs β€) = (mulGrpββ€ring) | ||
Theorem | prmirredlem 21048 | A positive integer is irreducible over β€ iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
β’ πΌ = (Irredββ€ring) β β’ (π΄ β β β (π΄ β πΌ β π΄ β β)) | ||
Theorem | dfprm2 21049 | The positive irreducible elements of β€ are the prime numbers. This is an alternative way to define β. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
β’ πΌ = (Irredββ€ring) β β’ β = (β β© πΌ) | ||
Theorem | prmirred 21050 | The irreducible elements of β€ are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
β’ πΌ = (Irredββ€ring) β β’ (π΄ β πΌ β (π΄ β β€ β§ (absβπ΄) β β)) | ||
Theorem | expghm 21051* | Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) |
β’ π = (mulGrpββfld) & β’ π = (π βΎs (β β {0})) β β’ ((π΄ β β β§ π΄ β 0) β (π₯ β β€ β¦ (π΄βπ₯)) β (β€ring GrpHom π)) | ||
Theorem | mulgghm2 21052* | The powers of a group element give a homomorphism from β€ to a group. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ Β· = (.gβπ ) & β’ πΉ = (π β β€ β¦ (π Β· 1 )) & β’ π΅ = (Baseβπ ) β β’ ((π β Grp β§ 1 β π΅) β πΉ β (β€ring GrpHom π )) | ||
Theorem | mulgrhm 21053* | The powers of the element 1 give a ring homomorphism from β€ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ Β· = (.gβπ ) & β’ πΉ = (π β β€ β¦ (π Β· 1 )) & β’ 1 = (1rβπ ) β β’ (π β Ring β πΉ β (β€ring RingHom π )) | ||
Theorem | mulgrhm2 21054* | The powers of the element 1 give the unique ring homomorphism from β€ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ Β· = (.gβπ ) & β’ πΉ = (π β β€ β¦ (π Β· 1 )) & β’ 1 = (1rβπ ) β β’ (π β Ring β (β€ring RingHom π ) = {πΉ}) | ||
Syntax | czrh 21055 | Map the rationals into a field, or the integers into a ring. |
class β€RHom | ||
Syntax | czlm 21056 | Augment an abelian group with vector space operations to turn it into a β€-module. |
class β€Mod | ||
Syntax | cchr 21057 | Syntax for ring characteristic. |
class chr | ||
Syntax | czn 21058 | The ring of integers modulo π. |
class β€/nβ€ | ||
Definition | df-zrh 21059 | Define the unique homomorphism from the integers into a ring. This encodes the usual notation of π = 1r + 1r + ... + 1r for integers (see also df-mulg 18953). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ β€RHom = (π β V β¦ βͺ (β€ring RingHom π)) | ||
Definition | df-zlm 21060 | Augment an abelian group with vector space operations to turn it into a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
β’ β€Mod = (π β V β¦ ((π sSet β¨(Scalarβndx), β€ringβ©) sSet β¨( Β·π βndx), (.gβπ)β©)) | ||
Definition | df-chr 21061 | The characteristic of a ring is the smallest positive integer which is equal to 0 when interpreted in the ring, or 0 if there is no such positive integer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ chr = (π β V β¦ ((odβπ)β(1rβπ))) | ||
Definition | df-zn 21062* | Define the ring of integers mod π. This is literally the quotient ring of β€ by the ideal πβ€, but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ β€/nβ€ = (π β β0 β¦ β¦β€ring / π§β¦β¦(π§ /s (π§ ~QG ((RSpanβπ§)β{π}))) / π β¦(π sSet β¨(leβndx), β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©)) | ||
Theorem | zrhval 21063 | Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ πΏ = (β€RHomβπ ) β β’ πΏ = βͺ (β€ring RingHom π ) | ||
Theorem | zrhval2 21064* | Alternate value of the β€RHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ πΏ = (β€RHomβπ ) & β’ Β· = (.gβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β πΏ = (π β β€ β¦ (π Β· 1 ))) | ||
Theorem | zrhmulg 21065 | Value of the β€RHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ πΏ = (β€RHomβπ ) & β’ Β· = (.gβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β β€) β (πΏβπ) = (π Β· 1 )) | ||
Theorem | zrhrhmb 21066 | The β€RHom homomorphism is the unique ring homomorphism from π. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ πΏ = (β€RHomβπ ) β β’ (π β Ring β (πΉ β (β€ring RingHom π ) β πΉ = πΏ)) | ||
Theorem | zrhrhm 21067 | The β€RHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ πΏ = (β€RHomβπ ) β β’ (π β Ring β πΏ β (β€ring RingHom π )) | ||
Theorem | zrh1 21068 | Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ πΏ = (β€RHomβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β (πΏβ1) = 1 ) | ||
Theorem | zrh0 21069 | Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ πΏ = (β€RHomβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β (πΏβ0) = 0 ) | ||
Theorem | zrhpropd 21070* | The β€ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (β€RHomβπΎ) = (β€RHomβπΏ)) | ||
Theorem | zlmval 21071 | Augment an abelian group with vector space operations to turn it into a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
β’ π = (β€ModβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β π β π = ((πΊ sSet β¨(Scalarβndx), β€ringβ©) sSet β¨( Β·π βndx), Β· β©)) | ||
Theorem | zlmlem 21072 | Lemma for zlmbas 21074 and zlmplusg 21076. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
β’ π = (β€ModβπΊ) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (Scalarβndx) & β’ (πΈβndx) β ( Β·π βndx) β β’ (πΈβπΊ) = (πΈβπ) | ||
Theorem | zlmlemOLD 21073 | Obsolete version of zlmlem 21072 as of 3-Nov-2024. Lemma for zlmbas 21074 and zlmplusg 21076. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (β€ModβπΊ) & β’ πΈ = Slot π & β’ π β β & β’ π < 5 β β’ (πΈβπΊ) = (πΈβπ) | ||
Theorem | zlmbas 21074 | Base set of a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
β’ π = (β€ModβπΊ) & β’ π΅ = (BaseβπΊ) β β’ π΅ = (Baseβπ) | ||
Theorem | zlmbasOLD 21075 | Obsolete version of zlmbas 21074 as of 3-Nov-2024. Base set of a β€ -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (β€ModβπΊ) & β’ π΅ = (BaseβπΊ) β β’ π΅ = (Baseβπ) | ||
Theorem | zlmplusg 21076 | Group operation of a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
β’ π = (β€ModβπΊ) & β’ + = (+gβπΊ) β β’ + = (+gβπ) | ||
Theorem | zlmplusgOLD 21077 | Obsolete version of zlmbas 21074 as of 3-Nov-2024. Group operation of a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (β€ModβπΊ) & β’ + = (+gβπΊ) β β’ + = (+gβπ) | ||
Theorem | zlmmulr 21078 | Ring operation of a β€-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
β’ π = (β€ModβπΊ) & β’ Β· = (.rβπΊ) β β’ Β· = (.rβπ) | ||
Theorem | zlmmulrOLD 21079 | Obsolete version of zlmbas 21074 as of 3-Nov-2024. Ring operation of a β€-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (β€ModβπΊ) & β’ Β· = (.rβπΊ) β β’ Β· = (.rβπ) | ||
Theorem | zlmsca 21080 | Scalar ring of a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.) |
β’ π = (β€ModβπΊ) β β’ (πΊ β π β β€ring = (Scalarβπ)) | ||
Theorem | zlmvsca 21081 | Scalar multiplication operation of a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (β€ModβπΊ) & β’ Β· = (.gβπΊ) β β’ Β· = ( Β·π βπ) | ||
Theorem | zlmlmod 21082 | The β€-module operation turns an arbitrary abelian group into a left module over β€. Also see zlmassa 21462. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (β€ModβπΊ) β β’ (πΊ β Abel β π β LMod) | ||
Theorem | chrval 21083 | Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π = (odβπ ) & β’ 1 = (1rβπ ) & β’ πΆ = (chrβπ ) β β’ (πβ 1 ) = πΆ | ||
Theorem | chrcl 21084 | Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
β’ πΆ = (chrβπ ) β β’ (π β Ring β πΆ β β0) | ||
Theorem | chrid 21085 | The canonical β€ ring homomorphism applied to a ring's characteristic is zero. (Contributed by Mario Carneiro, 23-Sep-2015.) |
β’ πΆ = (chrβπ ) & β’ πΏ = (β€RHomβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β (πΏβπΆ) = 0 ) | ||
Theorem | chrdvds 21086 | The β€ ring homomorphism is zero only at multiples of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
β’ πΆ = (chrβπ ) & β’ πΏ = (β€RHomβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β β€) β (πΆ β₯ π β (πΏβπ) = 0 )) | ||
Theorem | chrcong 21087 | If two integers are congruent relative to the ring characteristic, their images in the ring are the same. (Contributed by Mario Carneiro, 24-Sep-2015.) |
β’ πΆ = (chrβπ ) & β’ πΏ = (β€RHomβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β β€ β§ π β β€) β (πΆ β₯ (π β π) β (πΏβπ) = (πΏβπ))) | ||
Theorem | chrnzr 21088 | Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ (π β Ring β (π β NzRing β (chrβπ ) β 1)) | ||
Theorem | chrrhm 21089 | The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ (πΉ β (π RingHom π) β (chrβπ) β₯ (chrβπ )) | ||
Theorem | domnchr 21090 | The characteristic of a domain can only be zero or a prime. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ (π β Domn β ((chrβπ ) = 0 β¨ (chrβπ ) β β)) | ||
Theorem | znlidl 21091 | The set πβ€ is an ideal in β€. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
β’ π = (RSpanββ€ring) β β’ (π β β€ β (πβ{π}) β (LIdealββ€ring)) | ||
Theorem | zncrng2 21092 | The value of the β€/nβ€ structure. It is defined as the quotient ring β€ / πβ€, with an "artificial" ordering added to make it a Toset. (In other words, β€/nβ€ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
β’ π = (RSpanββ€ring) & β’ π = (β€ring /s (β€ring ~QG (πβ{π}))) β β’ (π β β€ β π β CRing) | ||
Theorem | znval 21093 | The value of the β€/nβ€ structure. It is defined as the quotient ring β€ / πβ€, with an "artificial" ordering added to make it a Toset. (In other words, β€/nβ€ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.) |
β’ π = (RSpanββ€ring) & β’ π = (β€ring /s (β€ring ~QG (πβ{π}))) & β’ π = (β€/nβ€βπ) & β’ πΉ = ((β€RHomβπ) βΎ π) & β’ π = if(π = 0, β€, (0..^π)) & β’ β€ = ((πΉ β β€ ) β β‘πΉ) β β’ (π β β0 β π = (π sSet β¨(leβndx), β€ β©)) | ||
Theorem | znle 21094 | The value of the β€/nβ€ structure. It is defined as the quotient ring β€ / πβ€, with an "artificial" ordering added to make it a Toset. (In other words, β€/nβ€ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
β’ π = (RSpanββ€ring) & β’ π = (β€ring /s (β€ring ~QG (πβ{π}))) & β’ π = (β€/nβ€βπ) & β’ πΉ = ((β€RHomβπ) βΎ π) & β’ π = if(π = 0, β€, (0..^π)) & β’ β€ = (leβπ) β β’ (π β β0 β β€ = ((πΉ β β€ ) β β‘πΉ)) | ||
Theorem | znval2 21095 | Self-referential expression for the β€/nβ€ structure. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
β’ π = (RSpanββ€ring) & β’ π = (β€ring /s (β€ring ~QG (πβ{π}))) & β’ π = (β€/nβ€βπ) & β’ β€ = (leβπ) β β’ (π β β0 β π = (π sSet β¨(leβndx), β€ β©)) | ||
Theorem | znbaslem 21096 | Lemma for znbas 21105. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, 3-Nov-2024.) |
β’ π = (RSpanββ€ring) & β’ π = (β€ring /s (β€ring ~QG (πβ{π}))) & β’ π = (β€/nβ€βπ) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (leβndx) β β’ (π β β0 β (πΈβπ) = (πΈβπ)) | ||
Theorem | znbaslemOLD 21097 | Obsolete version of znbaslem 21096 as of 3-Nov-2024. Lemma for znbas 21105. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (RSpanββ€ring) & β’ π = (β€ring /s (β€ring ~QG (πβ{π}))) & β’ π = (β€/nβ€βπ) & β’ πΈ = Slot πΎ & β’ πΎ β β & β’ πΎ < ;10 β β’ (π β β0 β (πΈβπ) = (πΈβπ)) | ||
Theorem | znbas2 21098 | The base set of β€/nβ€ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) |
β’ π = (RSpanββ€ring) & β’ π = (β€ring /s (β€ring ~QG (πβ{π}))) & β’ π = (β€/nβ€βπ) β β’ (π β β0 β (Baseβπ) = (Baseβπ)) | ||
Theorem | znbas2OLD 21099 | Obsolete version of znbas2 21098 as of 3-Nov-2024. The base set of β€/nβ€ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (RSpanββ€ring) & β’ π = (β€ring /s (β€ring ~QG (πβ{π}))) & β’ π = (β€/nβ€βπ) β β’ (π β β0 β (Baseβπ) = (Baseβπ)) | ||
Theorem | znadd 21100 | The additive structure of β€/nβ€ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) |
β’ π = (RSpanββ€ring) & β’ π = (β€ring /s (β€ring ~QG (πβ{π}))) & β’ π = (β€/nβ€βπ) β β’ (π β β0 β (+gβπ) = (+gβπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |