![]() |
Metamath
Proof Explorer Theorem List (p. 371 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rrndstprj1 37001 | The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
β’ π = (β βm πΌ) & β’ π = ((abs β β ) βΎ (β Γ β)) β β’ (((πΌ β Fin β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β ((πΉβπ΄)π(πΊβπ΄)) β€ (πΉ(βnβπΌ)πΊ)) | ||
Theorem | rrndstprj2 37002* | Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 37001 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
β’ π = (β βm πΌ) & β’ π = ((abs β β ) βΎ (β Γ β)) β β’ (((πΌ β (Fin β {β }) β§ πΉ β π β§ πΊ β π) β§ (π β β+ β§ βπ β πΌ ((πΉβπ)π(πΊβπ)) < π )) β (πΉ(βnβπΌ)πΊ) < (π Β· (ββ(β―βπΌ)))) | ||
Theorem | rrncmslem 37003* | Lemma for rrncms 37004. (Contributed by Jeff Madsen, 6-Jun-2014.) (Revised by Mario Carneiro, 13-Sep-2015.) |
β’ π = (β βm πΌ) & β’ π = ((abs β β ) βΎ (β Γ β)) & β’ π½ = (MetOpenβ(βnβπΌ)) & β’ (π β πΌ β Fin) & β’ (π β πΉ β (Cauβ(βnβπΌ))) & β’ (π β πΉ:ββΆπ) & β’ π = (π β πΌ β¦ ( β β(π‘ β β β¦ ((πΉβπ‘)βπ)))) β β’ (π β πΉ β dom (βπ‘βπ½)) | ||
Theorem | rrncms 37004 | Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
β’ π = (β βm πΌ) β β’ (πΌ β Fin β (βnβπΌ) β (CMetβπ)) | ||
Theorem | repwsmet 37005 | The supremum metric on ββπΌ is a metric. (Contributed by Jeff Madsen, 15-Sep-2015.) |
β’ π = ((βfld βΎs β) βs πΌ) & β’ π· = (distβπ) & β’ π = (β βm πΌ) β β’ (πΌ β Fin β π· β (Metβπ)) | ||
Theorem | rrnequiv 37006 | The supremum metric on ββπΌ is equivalent to the βn metric. (Contributed by Jeff Madsen, 15-Sep-2015.) |
β’ π = ((βfld βΎs β) βs πΌ) & β’ π· = (distβπ) & β’ π = (β βm πΌ) & β’ (π β πΌ β Fin) β β’ ((π β§ (πΉ β π β§ πΊ β π)) β ((πΉπ·πΊ) β€ (πΉ(βnβπΌ)πΊ) β§ (πΉ(βnβπΌ)πΊ) β€ ((ββ(β―βπΌ)) Β· (πΉπ·πΊ)))) | ||
Theorem | rrntotbnd 37007 | A set in Euclidean space is totally bounded iff its is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
β’ π = (β βm πΌ) & β’ π = ((βnβπΌ) βΎ (π Γ π)) β β’ (πΌ β Fin β (π β (TotBndβπ) β π β (Bndβπ))) | ||
Theorem | rrnheibor 37008 | Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ π = (β βm πΌ) & β’ π = ((βnβπΌ) βΎ (π Γ π)) & β’ π = (MetOpenβπ) & β’ π = (MetOpenβ(βnβπΌ)) β β’ ((πΌ β Fin β§ π β π) β (π β Comp β (π β (Clsdβπ) β§ π β (Bndβπ)))) | ||
Theorem | ismrer1 37009* | An isometry between β and ββ1. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ π = ((abs β β ) βΎ (β Γ β)) & β’ πΉ = (π₯ β β β¦ ({π΄} Γ {π₯})) β β’ (π΄ β π β πΉ β (π Ismty (βnβ{π΄}))) | ||
Theorem | reheibor 37010 | Heine-Borel theorem for real numbers. A subset of β is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ π = ((abs β β ) βΎ (π Γ π)) & β’ π = (MetOpenβπ) & β’ π = (topGenβran (,)) β β’ (π β β β (π β Comp β (π β (Clsdβπ) β§ π β (Bndβπ)))) | ||
Theorem | iccbnd 37011 | A closed interval in β is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Sep-2015.) |
β’ π½ = (π΄[,]π΅) & β’ π = ((abs β β ) βΎ (π½ Γ π½)) β β’ ((π΄ β β β§ π΅ β β) β π β (Bndβπ½)) | ||
Theorem | icccmpALT 37012 | A closed interval in β is compact. Alternate proof of icccmp 24561 using the Heine-Borel theorem heibor 36992. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Aug-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π½ = (π΄[,]π΅) & β’ π = ((abs β β ) βΎ (π½ Γ π½)) & β’ π = (MetOpenβπ) β β’ ((π΄ β β β§ π΅ β β) β π β Comp) | ||
Syntax | cass 37013 | Extend class notation with a device to add associativity to internal operations. |
class Ass | ||
Definition | df-ass 37014* | A device to add associativity to various sorts of internal operations. The definition is meaningful when π is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.) |
β’ Ass = {π β£ βπ₯ β dom dom πβπ¦ β dom dom πβπ§ β dom dom π((π₯ππ¦)ππ§) = (π₯π(π¦ππ§))} | ||
Syntax | cexid 37015 | Extend class notation with the class of all the internal operations with an identity element. |
class ExId | ||
Definition | df-exid 37016* | A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ ExId = {π β£ βπ₯ β dom dom πβπ¦ β dom dom π((π₯ππ¦) = π¦ β§ (π¦ππ₯) = π¦)} | ||
Theorem | isass 37017* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β Ass β βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)))) | ||
Theorem | isexid 37018* | The predicate πΊ has a left and right identity element. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β ExId β βπ₯ β π βπ¦ β π ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦))) | ||
Syntax | cmagm 37019 | Extend class notation with the class of all magmas. |
class Magma | ||
Definition | df-mgmOLD 37020* | Obsolete version of df-mgm 18565 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ Magma = {π β£ βπ‘ π:(π‘ Γ π‘)βΆπ‘} | ||
Theorem | ismgmOLD 37021 | Obsolete version of ismgm 18566 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β Magma β πΊ:(π Γ π)βΆπ)) | ||
Theorem | clmgmOLD 37022 | Obsolete version of mgmcl 18568 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ ((πΊ β Magma β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
Theorem | opidonOLD 37023 | Obsolete version of mndpfo 18682 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β (Magma β© ExId ) β πΊ:(π Γ π)βontoβπ) | ||
Theorem | rngopidOLD 37024 | Obsolete version of mndpfo 18682 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (πΊ β (Magma β© ExId ) β ran πΊ = dom dom πΊ) | ||
Theorem | opidon2OLD 37025 | Obsolete version of mndpfo 18682 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β (Magma β© ExId ) β πΊ:(π Γ π)βontoβπ) | ||
Theorem | isexid2 37026* | If πΊ β (Magma β© ExId ), then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β (Magma β© ExId ) β βπ’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ (π₯πΊπ’) = π₯)) | ||
Theorem | exidu1 37027* | Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β (Magma β© ExId ) β β!π’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ (π₯πΊπ’) = π₯)) | ||
Theorem | idrval 37028* | The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (πΊ β π΄ β π = (β©π’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ (π₯πΊπ’) = π₯))) | ||
Theorem | iorlid 37029 | A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (πΊ β (Magma β© ExId ) β π β π) | ||
Theorem | cmpidelt 37030 | A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((πΊ β (Magma β© ExId ) β§ π΄ β π) β ((ππΊπ΄) = π΄ β§ (π΄πΊπ) = π΄)) | ||
Syntax | csem 37031 | Extend class notation with the class of all semigroups. |
class SemiGrp | ||
Definition | df-sgrOLD 37032 | Obsolete version of df-sgrp 18644 as of 3-Feb-2020. A semigroup is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ SemiGrp = (Magma β© Ass) | ||
Theorem | smgrpismgmOLD 37033 | Obsolete version of sgrpmgm 18649 as of 3-Feb-2020. A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (πΊ β SemiGrp β πΊ β Magma) | ||
Theorem | issmgrpOLD 37034* | Obsolete version of issgrp 18645 as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β SemiGrp β (πΊ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))))) | ||
Theorem | smgrpmgm 37035 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β SemiGrp β πΊ:(π Γ π)βΆπ) | ||
Theorem | smgrpassOLD 37036* | Obsolete version of sgrpass 18650 as of 3-Feb-2020. A semigroup is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β SemiGrp β βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) | ||
Syntax | cmndo 37037 | Extend class notation with the class of all monoids. |
class MndOp | ||
Definition | df-mndo 37038 | A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ MndOp = (SemiGrp β© ExId ) | ||
Theorem | mndoissmgrpOLD 37039 | Obsolete version of mndsgrp 18665 as of 3-Feb-2020. A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (πΊ β MndOp β πΊ β SemiGrp) | ||
Theorem | mndoisexid 37040 | A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ (πΊ β MndOp β πΊ β ExId ) | ||
Theorem | mndoismgmOLD 37041 | Obsolete version of mndmgm 18666 as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (πΊ β MndOp β πΊ β Magma) | ||
Theorem | mndomgmid 37042 | A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
β’ (πΊ β MndOp β πΊ β (Magma β© ExId )) | ||
Theorem | ismndo 37043* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β MndOp β (πΊ β SemiGrp β§ βπ₯ β π βπ¦ β π ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)))) | ||
Theorem | ismndo1 37044* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β MndOp β (πΊ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ₯ β π βπ¦ β π ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)))) | ||
Theorem | ismndo2 37045* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β π΄ β (πΊ β MndOp β (πΊ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ₯ β π βπ¦ β π ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)))) | ||
Theorem | grpomndo 37046 | A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ (πΊ β GrpOp β πΊ β MndOp) | ||
Theorem | exidcl 37047 | Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ β β’ ((πΊ β (Magma β© ExId ) β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
Theorem | exidreslem 37048* | Lemma for exidres 37049 and exidresid 37050. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π» = (πΊ βΎ (π Γ π)) β β’ ((πΊ β (Magma β© ExId ) β§ π β π β§ π β π) β (π β dom dom π» β§ βπ₯ β dom dom π»((ππ»π₯) = π₯ β§ (π₯π»π) = π₯))) | ||
Theorem | exidres 37049 | The restriction of a binary operation with identity to a subset containing the identity has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π» = (πΊ βΎ (π Γ π)) β β’ ((πΊ β (Magma β© ExId ) β§ π β π β§ π β π) β π» β ExId ) | ||
Theorem | exidresid 37050 | The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π» = (πΊ βΎ (π Γ π)) β β’ (((πΊ β (Magma β© ExId ) β§ π β π β§ π β π) β§ π» β Magma) β (GIdβπ») = π) | ||
Theorem | ablo4pnp 37051 | A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ πΉ β π))) β ((π΄πΊπ΅)π·(πΆπΊπΉ)) = ((π΄π·πΆ)πΊ(π΅π·πΉ))) | ||
Theorem | grpoeqdivid 37052 | Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄ = π΅ β (π΄π·π΅) = π)) | ||
Theorem | grposnOLD 37053 | The group operation for the singleton group. Obsolete, use grp1 18966. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ β V β β’ {β¨β¨π΄, π΄β©, π΄β©} β GrpOp | ||
Syntax | cghomOLD 37054 | Obsolete version of cghm 19127 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.) |
class GrpOpHom | ||
Definition | df-ghomOLD 37055* | Obsolete version of df-ghm 19128 as of 15-Mar-2020. Define the set of group homomorphisms from π to β. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
β’ GrpOpHom = (π β GrpOp, β β GrpOp β¦ {π β£ (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)))}) | ||
Theorem | elghomlem1OLD 37056* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 37058. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))} β β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΊ GrpOpHom π») = π) | ||
Theorem | elghomlem2OLD 37057* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 37058. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))} β β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β (πΊ GrpOpHom π») β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) | ||
Theorem | elghomOLD 37058* | Obsolete version of isghm 19130 as of 15-Mar-2020. Membership in the set of group homomorphisms from πΊ to π». (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = ran πΊ & β’ π = ran π» β β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β (πΊ GrpOpHom π») β (πΉ:πβΆπ β§ βπ₯ β π βπ¦ β π ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) | ||
Theorem | ghomlinOLD 37059 | Obsolete version of ghmlin 19135 as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = ran πΊ β β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β ((πΉβπ΄)π»(πΉβπ΅)) = (πΉβ(π΄πΊπ΅))) | ||
Theorem | ghomidOLD 37060 | Obsolete version of ghmid 19136 as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (GIdβπΊ) & β’ π = (GIdβπ») β β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉβπ) = π) | ||
Theorem | ghomf 37061 | Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) |
β’ π = ran πΊ & β’ π = ran π» β β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β πΉ:πβΆπ) | ||
Theorem | ghomco 37062 | The composition of two group homomorphisms is a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β§ (π β (πΊ GrpOpHom π») β§ π β (π» GrpOpHom πΎ))) β (π β π) β (πΊ GrpOpHom πΎ)) | ||
Theorem | ghomdiv 37063 | Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) & β’ πΆ = ( /π βπ») β β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π·π΅)) = ((πΉβπ΄)πΆ(πΉβπ΅))) | ||
Theorem | grpokerinj 37064 | A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = ran π» & β’ π = (GIdβπ») β β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉ:πβ1-1βπ β (β‘πΉ β {π}) = {π})) | ||
Syntax | crngo 37065 | Extend class notation with the class of all unital rings. |
class RingOps | ||
Definition | df-rngo 37066* | Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.) |
β’ RingOps = {β¨π, ββ© β£ ((π β AbelOp β§ β:(ran π Γ ran π)βΆran π) β§ (βπ₯ β ran πβπ¦ β ran πβπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β§ βπ₯ β ran πβπ¦ β ran π((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦)))} | ||
Theorem | relrngo 37067 | The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ Rel RingOps | ||
Theorem | isrngo 37068* | The predicate "is a (unital) ring." Definition of "ring with unit" in [Schechter] p. 187. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (π» β π΄ β (β¨πΊ, π»β© β RingOps β ((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))))) | ||
Theorem | isrngod 37069* | Conditions that determine a ring. (Changed label from isringd 20179 to isrngod 37069-NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ (π β πΊ β AbelOp) & β’ (π β π = ran πΊ) & β’ (π β π»:(π Γ π)βΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§))) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§))) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) & β’ (π β π β π) & β’ ((π β§ π¦ β π) β (ππ»π¦) = π¦) & β’ ((π β§ π¦ β π) β (π¦π»π) = π¦) β β’ (π β β¨πΊ, π»β© β RingOps) | ||
Theorem | rngoi 37070* | The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β ((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))) | ||
Theorem | rngosm 37071 | Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β π»:(π Γ π)βΆπ) | ||
Theorem | rngocl 37072 | Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄π»π΅) β π) | ||
Theorem | rngoid 37073* | The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π) β βπ’ β π ((π’π»π΄) = π΄ β§ (π΄π»π’) = π΄)) | ||
Theorem | rngoideu 37074* | The unity element of a ring is unique. (Contributed by NM, 4-Apr-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β β!π’ β π βπ₯ β π ((π’π»π₯) = π₯ β§ (π₯π»π’) = π₯)) | ||
Theorem | rngodi 37075 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»(π΅πΊπΆ)) = ((π΄π»π΅)πΊ(π΄π»πΆ))) | ||
Theorem | rngodir 37076 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)π»πΆ) = ((π΄π»πΆ)πΊ(π΅π»πΆ))) | ||
Theorem | rngoass 37077 | Associative law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π»π΅)π»πΆ) = (π΄π»(π΅π»πΆ))) | ||
Theorem | rngo2 37078* | A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π) β βπ₯ β π (π΄πΊπ΄) = ((π₯πΊπ₯)π»π΄)) | ||
Theorem | rngoablo 37079 | A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) β β’ (π β RingOps β πΊ β AbelOp) | ||
Theorem | rngoablo2 37080 | In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
β’ (β¨πΊ, π»β© β RingOps β πΊ β AbelOp) | ||
Theorem | rngogrpo 37081 | A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) β β’ (π β RingOps β πΊ β GrpOp) | ||
Theorem | rngone0 37082 | The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β π β β ) | ||
Theorem | rngogcl 37083 | Closure law for the addition (group) operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
Theorem | rngocom 37084 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | rngoaass 37085 | The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | rngoa32 37086 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = ((π΄πΊπΆ)πΊπ΅)) | ||
Theorem | rngoa4 37087 | Rearrangement of 4 terms in a sum of ring elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)πΊ(πΆπΊπ·)) = ((π΄πΊπΆ)πΊ(π΅πΊπ·))) | ||
Theorem | rngorcan 37088 | Right cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπΆ) = (π΅πΊπΆ) β π΄ = π΅)) | ||
Theorem | rngolcan 37089 | Left cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆπΊπ΄) = (πΆπΊπ΅) β π΄ = π΅)) | ||
Theorem | rngo0cl 37090 | A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β π β π) | ||
Theorem | rngo0rid 37091 | The additive identity of a ring is a right identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (π΄πΊπ) = π΄) | ||
Theorem | rngo0lid 37092 | The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (ππΊπ΄) = π΄) | ||
Theorem | rngolz 37093 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
β’ π = (GIdβπΊ) & β’ π = ran πΊ & β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) β β’ ((π β RingOps β§ π΄ β π) β (ππ»π΄) = π) | ||
Theorem | rngorz 37094 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
β’ π = (GIdβπΊ) & β’ π = ran πΊ & β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) β β’ ((π β RingOps β§ π΄ β π) β (π΄π»π) = π) | ||
Theorem | rngosn3 37095 | Obsolete as of 25-Jan-2020. Use ring1zr 20540 or srg1zr 20109 instead. The only unital ring with a base set consisting in one element is the zero ring. (Contributed by FL, 13-Feb-2010.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π΅) β (π = {π΄} β π = β¨{β¨β¨π΄, π΄β©, π΄β©}, {β¨β¨π΄, π΄β©, π΄β©}β©)) | ||
Theorem | rngosn4 37096 | Obsolete as of 25-Jan-2020. Use rngen1zr 20541 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π) β (π β 1o β π = β¨{β¨β¨π΄, π΄β©, π΄β©}, {β¨β¨π΄, π΄β©, π΄β©}β©)) | ||
Theorem | rngosn6 37097 | Obsolete as of 25-Jan-2020. Use ringen1zr 20542 or srgen1zr 20110 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β (π β 1o β π = β¨{β¨β¨π, πβ©, πβ©}, {β¨β¨π, πβ©, πβ©}β©)) | ||
Theorem | rngonegcl 37098 | A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (πβπ΄) β π) | ||
Theorem | rngoaddneg1 37099 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (π΄πΊ(πβπ΄)) = π) | ||
Theorem | rngoaddneg2 37100 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β ((πβπ΄)πΊπ΄) = π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |