Home | Metamath
Proof Explorer Theorem List (p. 201 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvdsrcl 20001 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) β β’ (π β₯ π β π β π΅) | ||
Theorem | dvdsrcl2 20002 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β Ring β§ π β₯ π) β π β π΅) | ||
Theorem | dvdsrid 20003 | An element in a (unital) ring divides itself. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β Ring β§ π β π΅) β π β₯ π) | ||
Theorem | dvdsrtr 20004 | Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β Ring β§ π β₯ π β§ π β₯ π) β π β₯ π) | ||
Theorem | dvdsrmul1 20005 | The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β₯ π) β (π Β· π) β₯ (π Β· π)) | ||
Theorem | dvdsrneg 20006 | An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ π β π΅) β π β₯ (πβπ)) | ||
Theorem | dvdsr01 20007 | In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 20676.) (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β π β₯ 0 ) | ||
Theorem | dvdsr02 20008 | Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β ( 0 β₯ π β π = 0 )) | ||
Theorem | isunit 20009 | Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 8-Dec-2015.) |
β’ π = (Unitβπ ) & β’ 1 = (1rβπ ) & β’ β₯ = (β₯rβπ ) & β’ π = (opprβπ ) & β’ πΈ = (β₯rβπ) β β’ (π β π β (π β₯ 1 β§ ππΈ 1 )) | ||
Theorem | 1unit 20010 | The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π = (Unitβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β 1 β π) | ||
Theorem | unitcl 20011 | A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) β β’ (π β π β π β π΅) | ||
Theorem | unitss 20012 | The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) β β’ π β π΅ | ||
Theorem | opprunit 20013 | Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (Unitβπ ) & β’ π = (opprβπ ) β β’ π = (Unitβπ) | ||
Theorem | crngunit 20014 | Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ π = (Unitβπ ) & β’ 1 = (1rβπ ) & β’ β₯ = (β₯rβπ ) β β’ (π β CRing β (π β π β π β₯ 1 )) | ||
Theorem | dvdsunit 20015 | A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ π = (Unitβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β CRing β§ π β₯ π β§ π β π) β π β π) | ||
Theorem | unitmulcl 20016 | The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π β§ π β π) β (π Β· π) β π) | ||
Theorem | unitmulclb 20017 | Reversal of unitmulcl 20016 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β CRing β§ π β π΅ β§ π β π΅) β ((π Β· π) β π β (π β π β§ π β π))) | ||
Theorem | unitgrpbas 20018 | The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs π) β β’ π = (BaseβπΊ) | ||
Theorem | unitgrp 20019 | The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs π) β β’ (π β Ring β πΊ β Grp) | ||
Theorem | unitabl 20020 | The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (Unitβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs π) β β’ (π β CRing β πΊ β Abel) | ||
Theorem | unitgrpid 20021 | The identity of the multiplicative group is 1r. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs π) & β’ 1 = (1rβπ ) β β’ (π β Ring β 1 = (0gβπΊ)) | ||
Theorem | unitsubm 20022 | The group of units is a submonoid of the multiplicative monoid of the ring. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π = (Unitβπ ) & β’ π = (mulGrpβπ ) β β’ (π β Ring β π β (SubMndβπ)) | ||
Syntax | cinvr 20023 | Extend class notation with multiplicative inverse. |
class invr | ||
Definition | df-invr 20024 | Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.) |
β’ invr = (π β V β¦ (invgβ((mulGrpβπ) βΎs (Unitβπ)))) | ||
Theorem | invrfval 20025 | Multiplicative inverse function for a division ring. (Contributed by NM, 21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs π) & β’ πΌ = (invrβπ ) β β’ πΌ = (invgβπΊ) | ||
Theorem | unitinvcl 20026 | The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β Ring β§ π β π) β (πΌβπ) β π) | ||
Theorem | unitinvinv 20027 | The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β Ring β§ π β π) β (πΌβ(πΌβπ)) = π) | ||
Theorem | ringinvcl 20028 | The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β π) β (πΌβπ) β π΅) | ||
Theorem | unitlinv 20029 | A unit times its inverse is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π) β ((πΌβπ) Β· π) = 1 ) | ||
Theorem | unitrinv 20030 | A unit times its inverse is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π) β (π Β· (πΌβπ)) = 1 ) | ||
Theorem | 1rinv 20031 | The inverse of the ring unity is the ring unity. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ πΌ = (invrβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β (πΌβ 1 ) = 1 ) | ||
Theorem | 0unit 20032 | The additive identity is a unit if and only if 1 = 0, i.e. we are in the zero ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β ( 0 β π β 1 = 0 )) | ||
Theorem | unitnegcl 20033 | The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (Unitβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ π β π) β (πβπ) β π) | ||
Syntax | cdvr 20034 | Extend class notation with ring division. |
class /r | ||
Definition | df-dvr 20035* | Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ /r = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Unitβπ) β¦ (π₯(.rβπ)((invrβπ)βπ¦)))) | ||
Theorem | dvrfval 20036* | Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Proof shortened by AV, 2-Mar-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ / = (/rβπ ) β β’ / = (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦))) | ||
Theorem | dvrval 20037 | Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ / = (/rβπ ) β β’ ((π β π΅ β§ π β π) β (π / π) = (π Β· (πΌβπ))) | ||
Theorem | dvrcl 20038 | Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β (π / π) β π΅) | ||
Theorem | unitdvcl 20039 | The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ π = (Unitβπ ) & β’ / = (/rβπ ) β β’ ((π β Ring β§ π β π β§ π β π) β (π / π) β π) | ||
Theorem | dvrid 20040 | A cancellation law for division. (divid 11776 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π) β (π / π) = 1 ) | ||
Theorem | dvr1 20041 | A cancellation law for division. (div1 11778 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅) β (π / 1 ) = π) | ||
Theorem | dvrass 20042 | An associative law for division. (divass 11765 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π Β· π) / π) = (π Β· (π / π))) | ||
Theorem | dvrcan1 20043 | A cancellation law for division. (divcan1 11756 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π / π) Β· π) = π) | ||
Theorem | dvrcan3 20044 | A cancellation law for division. (divcan3 11773 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π Β· π) / π) = π) | ||
Theorem | dvreq1 20045 | A cancellation law for division. (diveq1 11780 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π / π) = 1 β π = π)) | ||
Theorem | ringinvdv 20046 | Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β Ring β§ π β π) β (πΌβπ) = ( 1 / π)) | ||
Theorem | rngidpropd 20047* | The ring identity depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (1rβπΎ) = (1rβπΏ)) | ||
Theorem | dvdsrpropd 20048* | The divisibility relation depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (β₯rβπΎ) = (β₯rβπΏ)) | ||
Theorem | unitpropd 20049* | The set of units depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (UnitβπΎ) = (UnitβπΏ)) | ||
Theorem | invrpropd 20050* | The ring inverse function depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (invrβπΎ) = (invrβπΏ)) | ||
Theorem | isirred 20051* | An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (Irredβπ ) & β’ π = (π΅ β π) & β’ Β· = (.rβπ ) β β’ (π β πΌ β (π β π β§ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π)) | ||
Theorem | isnirred 20052* | The property of being a non-irreducible (reducible) element in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (Irredβπ ) & β’ π = (π΅ β π) & β’ Β· = (.rβπ ) β β’ (π β π΅ β (Β¬ π β πΌ β (π β π β¨ βπ₯ β π βπ¦ β π (π₯ Β· π¦) = π))) | ||
Theorem | isirred2 20053* | Expand out the class difference from isirred 20051. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (Irredβπ ) & β’ Β· = (.rβπ ) β β’ (π β πΌ β (π β π΅ β§ Β¬ π β π β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) | ||
Theorem | opprirred 20054 | Irreducibility is symmetric, so the irreducible elements of the opposite ring are the same as the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (opprβπ ) & β’ πΌ = (Irredβπ ) β β’ πΌ = (Irredβπ) | ||
Theorem | irredn0 20055 | The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β πΌ) β π β 0 ) | ||
Theorem | irredcl 20056 | An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β πΌ β π β π΅) | ||
Theorem | irrednu 20057 | An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (Unitβπ ) β β’ (π β πΌ β Β¬ π β π) | ||
Theorem | irredn1 20058 | The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β πΌ) β π β 1 ) | ||
Theorem | irredrmul 20059 | The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β πΌ β§ π β π) β (π Β· π) β πΌ) | ||
Theorem | irredlmul 20060 | The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π β§ π β πΌ) β (π Β· π) β πΌ) | ||
Theorem | irredmul 20061 | If product of two elements is irreducible, then one of the elements must be a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) β β’ ((π β π΅ β§ π β π΅ β§ (π Β· π) β πΌ) β (π β π β¨ π β π)) | ||
Theorem | irredneg 20062 | The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ π β πΌ) β (πβπ) β πΌ) | ||
Theorem | irrednegb 20063 | An element is irreducible iff its negative is. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (invgβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β π΅) β (π β πΌ β (πβπ) β πΌ)) | ||
Syntax | crpm 20064 | Syntax for the ring primes function. |
class RPrime | ||
Definition | df-rprm 20065* | Define the function associating with a ring its set of prime elements. A prime element is a nonzero non-unit that satisfies an equivalent of Euclid's lemma euclemma 16524. Prime elements are closely related to irreducible elements (see df-irred 19995). (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ RPrime = (π€ β V β¦ β¦(Baseβπ€) / πβ¦{π β (π β ((Unitβπ€) βͺ {(0gβπ€)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦))}) | ||
Syntax | crh 20066 | Extend class notation with the ring homomorphisms. |
class RingHom | ||
Syntax | crs 20067 | Extend class notation with the ring isomorphisms. |
class RingIso | ||
Syntax | cric 20068 | Extend class notation with the ring isomorphism relation. |
class βπ | ||
Definition | df-rnghom 20069* | Define the set of ring homomorphisms from π to π . (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ RingHom = (π β Ring, π β Ring β¦ β¦(Baseβπ) / π£β¦β¦(Baseβπ ) / π€β¦{π β (π€ βm π£) β£ ((πβ(1rβπ)) = (1rβπ ) β§ βπ₯ β π£ βπ¦ β π£ ((πβ(π₯(+gβπ)π¦)) = ((πβπ₯)(+gβπ )(πβπ¦)) β§ (πβ(π₯(.rβπ)π¦)) = ((πβπ₯)(.rβπ )(πβπ¦))))}) | ||
Definition | df-rngiso 20070* | Define the set of ring isomorphisms from π to π . (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ RingIso = (π β V, π β V β¦ {π β (π RingHom π ) β£ β‘π β (π RingHom π)}) | ||
Theorem | dfrhm2 20071* | The property of a ring homomorphism can be decomposed into separate homomorphic conditions for addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ RingHom = (π β Ring, π β Ring β¦ ((π GrpHom π ) β© ((mulGrpβπ) MndHom (mulGrpβπ )))) | ||
Definition | df-ric 20072 | Define the ring isomorphism relation, analogous to df-gic 18982: Two (unital) rings are said to be isomorphic iff they are connected by at least one isomorphism. Isomorphic rings share all global ring properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by AV, 24-Dec-2019.) |
β’ βπ = (β‘ RingIso β (V β 1o)) | ||
Theorem | rhmrcl1 20073 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π RingHom π) β π β Ring) | ||
Theorem | rhmrcl2 20074 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π RingHom π) β π β Ring) | ||
Theorem | isrhm 20075 | A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ π = (mulGrpβπ ) & β’ π = (mulGrpβπ) β β’ (πΉ β (π RingHom π) β ((π β Ring β§ π β Ring) β§ (πΉ β (π GrpHom π) β§ πΉ β (π MndHom π)))) | ||
Theorem | rhmmhm 20076 | A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ π = (mulGrpβπ ) & β’ π = (mulGrpβπ) β β’ (πΉ β (π RingHom π) β πΉ β (π MndHom π)) | ||
Theorem | isrim0OLD 20077 | Obsolete version of isrim0 20079 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β π β§ π β π) β (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π )))) | ||
Theorem | rimrcl 20078 | Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019.) |
β’ (πΉ β (π RingIso π) β (π β V β§ π β V)) | ||
Theorem | isrim0 20079 | A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 18987. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.) |
β’ (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π ))) | ||
Theorem | rhmghm 20080 | A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π RingHom π) β πΉ β (π GrpHom π)) | ||
Theorem | rhmf 20081 | A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RingHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | rhmmul 20082 | A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) β β’ ((πΉ β (π RingHom π) β§ π΄ β π β§ π΅ β π) β (πΉβ(π΄ Β· π΅)) = ((πΉβπ΄) Γ (πΉβπ΅))) | ||
Theorem | isrhm2d 20083* | Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) & β’ π = (1rβπ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) & β’ (π β π β Ring) & β’ (π β π β Ring) & β’ (π β (πΉβ 1 ) = π) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Γ (πΉβπ¦))) & β’ (π β πΉ β (π GrpHom π)) β β’ (π β πΉ β (π RingHom π)) | ||
Theorem | isrhmd 20084* | Demonstration of ring homomorphism. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) & β’ π = (1rβπ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) & β’ (π β π β Ring) & β’ (π β π β Ring) & β’ (π β (πΉβ 1 ) = π) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Γ (πΉβπ¦))) & β’ πΆ = (Baseβπ) & β’ + = (+gβπ ) & ⒠⨣ = (+gβπ) & β’ (π β πΉ:π΅βΆπΆ) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦))) β β’ (π β πΉ β (π RingHom π)) | ||
Theorem | rhm1 20085 | Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ 1 = (1rβπ ) & β’ π = (1rβπ) β β’ (πΉ β (π RingHom π) β (πΉβ 1 ) = π) | ||
Theorem | idrhm 20086 | The identity homomorphism on a ring. (Contributed by AV, 14-Feb-2020.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β ( I βΎ π΅) β (π RingHom π )) | ||
Theorem | rhmf1o 20087 | A ring homomorphism is bijective iff its converse is also a ring homomorphism. (Contributed by AV, 22-Oct-2019.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RingHom π) β (πΉ:π΅β1-1-ontoβπΆ β β‘πΉ β (π RingHom π ))) | ||
Theorem | isrim 20088 | An isomorphism of rings is a bijective homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 12-Jan-2025.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ πΉ:π΅β1-1-ontoβπΆ)) | ||
Theorem | isrimOLD 20089 | Obsolete version of isrim 20088 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ ((π β π β§ π β π) β (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ πΉ:π΅β1-1-ontoβπΆ))) | ||
Theorem | rimf1o 20090 | An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RingIso π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Theorem | rimrhmOLD 20091 | Obsolete version of rimrhm 20092 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RingIso π) β πΉ β (π RingHom π)) | ||
Theorem | rimrhm 20092 | A ring isomorphism is a homomorphism. Compare gimghm 18986. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.) |
β’ (πΉ β (π RingIso π) β πΉ β (π RingHom π)) | ||
Theorem | rimgim 20093 | An isomorphism of rings is an isomorphism of their additive groups. (Contributed by AV, 24-Dec-2019.) |
β’ (πΉ β (π RingIso π) β πΉ β (π GrpIso π)) | ||
Theorem | rhmco 20094 | The composition of ring homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β (πΉ β πΊ) β (π RingHom π)) | ||
Theorem | pwsco1rhm 20095* | Right composition with a function on the index sets yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (π βs π΄) & β’ π = (π βs π΅) & β’ πΆ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (π β πΆ β¦ (π β πΉ)) β (π RingHom π)) | ||
Theorem | pwsco2rhm 20096* | Left composition with a ring homomorphism yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (π βs π΄) & β’ π = (π βs π΄) & β’ π΅ = (Baseβπ) & β’ (π β π΄ β π) & β’ (π β πΉ β (π RingHom π)) β β’ (π β (π β π΅ β¦ (πΉ β π)) β (π RingHom π)) | ||
Theorem | f1ghm0to0 20097 | If a group homomorphism πΉ is injective, it maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.) |
β’ π΄ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ 0 = (0gβπ ) β β’ ((πΉ β (π GrpHom π) β§ πΉ:π΄β1-1βπ΅ β§ π β π΄) β ((πΉβπ) = π β π = 0 )) | ||
Theorem | f1rhm0to0ALT 20098 | Alternate proof for f1ghm0to0 20097. Using ghmf1 18969 does not make the proof shorter and requires disjoint variable restrictions! (Contributed by AV, 24-Oct-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ 0 = (0gβπ ) β β’ ((πΉ β (π RingHom π) β§ πΉ:π΄β1-1βπ΅ β§ π β π΄) β ((πΉβπ) = π β π = 0 )) | ||
Theorem | gim0to0 20099 | A group isomorphism maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 23-May-2023.) |
β’ π΄ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ 0 = (0gβπ ) β β’ ((πΉ β (π GrpIso π) β§ π β π΄) β ((πΉβπ) = π β π = 0 )) | ||
Theorem | kerf1ghm 20100 | A group homomorphism πΉ is injective if and only if its kernel is the singleton {π}. (Contributed by Thierry Arnoux, 27-Oct-2017.) (Proof shortened by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.) |
β’ π΄ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ ) & β’ 0 = (0gβπ) β β’ (πΉ β (π GrpHom π) β (πΉ:π΄β1-1βπ΅ β (β‘πΉ β { 0 }) = {π})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |