![]() |
Metamath
Proof Explorer Theorem List (p. 203 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cinvr 20201 | Extend class notation with multiplicative inverse. |
class invr | ||
Definition | df-invr 20202 | Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.) |
β’ invr = (π β V β¦ (invgβ((mulGrpβπ) βΎs (Unitβπ)))) | ||
Theorem | invrfval 20203 | 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 20204 | The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β Ring β§ π β π) β (πΌβπ) β π) | ||
Theorem | unitinvinv 20205 | The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β Ring β§ π β π) β (πΌβ(πΌβπ)) = π) | ||
Theorem | ringinvcl 20206 | The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β π) β (πΌβπ) β π΅) | ||
Theorem | unitlinv 20207 | 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 20208 | 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 20209 | 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 20210 | 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 20211 | The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (Unitβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ π β π) β (πβπ) β π) | ||
Theorem | ringunitnzdiv 20212 | In a unitary ring, a unit is not a zero divisor. (Contributed by AV, 7-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β (Unitβπ )) β β’ (π β ((π Β· π) = 0 β π = 0 )) | ||
Theorem | ring1nzdiv 20213 | In a unitary ring, the ring unity is not a zero divisor. (Contributed by AV, 7-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ 1 = (1rβπ ) β β’ (π β (( 1 Β· π) = 0 β π = 0 )) | ||
Syntax | cdvr 20214 | Extend class notation with ring division. |
class /r | ||
Definition | df-dvr 20215* | Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ /r = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Unitβπ) β¦ (π₯(.rβπ)((invrβπ)βπ¦)))) | ||
Theorem | dvrfval 20216* | 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 20217 | 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 20218 | Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β (π / π) β π΅) | ||
Theorem | unitdvcl 20219 | The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ π = (Unitβπ ) & β’ / = (/rβπ ) β β’ ((π β Ring β§ π β π β§ π β π) β (π / π) β π) | ||
Theorem | dvrid 20220 | A ring element divided by itself is the ring unity. (divid 11901 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π) β (π / π) = 1 ) | ||
Theorem | dvr1 20221 | A ring element divided by the ring unity is itself. (div1 11903 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅) β (π / 1 ) = π) | ||
Theorem | dvrass 20222 | An associative law for division. (divass 11890 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π Β· π) / π) = (π Β· (π / π))) | ||
Theorem | dvrcan1 20223 | A cancellation law for division. (divcan1 11881 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π / π) Β· π) = π) | ||
Theorem | dvrcan3 20224 | A cancellation law for division. (divcan3 11898 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π Β· π) / π) = π) | ||
Theorem | dvreq1 20225 | Equality in terms of ratio equal to ring unity. (diveq1 11905 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π / π) = 1 β π = π)) | ||
Theorem | dvrdir 20226 | Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ + = (+gβπ ) & β’ / = (/rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π + π) / π) = ((π / π) + (π / π))) | ||
Theorem | rdivmuldivd 20227 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 30-Oct-2017.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ + = (+gβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π) β β’ (π β ((π / π) Β· (π / π)) = ((π Β· π) / (π Β· π))) | ||
Theorem | ringinvdv 20228 | 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 20229* | The ring unity 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 20230* | 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 20231* | 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 20232* | 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 20233* | 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 20234* | 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 20235* | Expand out the class difference from isirred 20233. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (Irredβπ ) & β’ Β· = (.rβπ ) β β’ (π β πΌ β (π β π΅ β§ Β¬ π β π β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) | ||
Theorem | opprirred 20236 | 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 20237 | The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β πΌ) β π β 0 ) | ||
Theorem | irredcl 20238 | An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β πΌ β π β π΅) | ||
Theorem | irrednu 20239 | An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (Unitβπ ) β β’ (π β πΌ β Β¬ π β π) | ||
Theorem | irredn1 20240 | The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β πΌ) β π β 1 ) | ||
Theorem | irredrmul 20241 | The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β πΌ β§ π β π) β (π Β· π) β πΌ) | ||
Theorem | irredlmul 20242 | The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π β§ π β πΌ) β (π Β· π) β πΌ) | ||
Theorem | irredmul 20243 | 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 20244 | The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ π β πΌ) β (πβπ) β πΌ) | ||
Theorem | irrednegb 20245 | An element is irreducible iff its negative is. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (invgβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β π΅) β (π β πΌ β (πβπ) β πΌ)) | ||
Syntax | crpm 20246 | Syntax for the ring primes function. |
class RPrime | ||
Definition | df-rprm 20247* | 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 16650. Prime elements are closely related to irreducible elements (see df-irred 20173). (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ RPrime = (π€ β V β¦ β¦(Baseβπ€) / πβ¦{π β (π β ((Unitβπ€) βͺ {(0gβπ€)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦))}) | ||
Syntax | crh 20248 | Extend class notation with the ring homomorphisms. |
class RingHom | ||
Syntax | crs 20249 | Extend class notation with the ring isomorphisms. |
class RingIso | ||
Syntax | cric 20250 | Extend class notation with the ring isomorphism relation. |
class βπ | ||
Definition | df-rnghom 20251* | 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 20252* | Define the set of ring isomorphisms from π to π . (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ RingIso = (π β V, π β V β¦ {π β (π RingHom π ) β£ β‘π β (π RingHom π)}) | ||
Theorem | dfrhm2 20253* | 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 20254 | Define the ring isomorphism relation, analogous to df-gic 19134: 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 20255 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π RingHom π) β π β Ring) | ||
Theorem | rhmrcl2 20256 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π RingHom π) β π β Ring) | ||
Theorem | isrhm 20257 | 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 20258 | A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ π = (mulGrpβπ ) & β’ π = (mulGrpβπ) β β’ (πΉ β (π RingHom π) β πΉ β (π MndHom π)) | ||
Theorem | isrim0OLD 20259 | Obsolete version of isrim0 20261 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β π β§ π β π) β (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π )))) | ||
Theorem | rimrcl 20260 | Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019.) |
β’ (πΉ β (π RingIso π) β (π β V β§ π β V)) | ||
Theorem | isrim0 20261 | A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 19139. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.) |
β’ (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π ))) | ||
Theorem | rhmghm 20262 | A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π RingHom π) β πΉ β (π GrpHom π)) | ||
Theorem | rhmf 20263 | A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RingHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | rhmmul 20264 | A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) β β’ ((πΉ β (π RingHom π) β§ π΄ β π β§ π΅ β π) β (πΉβ(π΄ Β· π΅)) = ((πΉβπ΄) Γ (πΉβπ΅))) | ||
Theorem | isrhm2d 20265* | Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) & β’ π = (1rβπ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) & β’ (π β π β Ring) & β’ (π β π β Ring) & β’ (π β (πΉβ 1 ) = π) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Γ (πΉβπ¦))) & β’ (π β πΉ β (π GrpHom π)) β β’ (π β πΉ β (π RingHom π)) | ||
Theorem | isrhmd 20266* | 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 20267 | Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ 1 = (1rβπ ) & β’ π = (1rβπ) β β’ (πΉ β (π RingHom π) β (πΉβ 1 ) = π) | ||
Theorem | idrhm 20268 | The identity homomorphism on a ring. (Contributed by AV, 14-Feb-2020.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β ( I βΎ π΅) β (π RingHom π )) | ||
Theorem | rhmf1o 20269 | 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 20270 | 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 20271 | Obsolete version of isrim 20270 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 20272 | An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RingIso π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Theorem | rimrhmOLD 20273 | Obsolete version of rimrhm 20274 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 20274 | A ring isomorphism is a homomorphism. Compare gimghm 19138. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.) |
β’ (πΉ β (π RingIso π) β πΉ β (π RingHom π)) | ||
Theorem | rimgim 20275 | An isomorphism of rings is an isomorphism of their additive groups. (Contributed by AV, 24-Dec-2019.) |
β’ (πΉ β (π RingIso π) β πΉ β (π GrpIso π)) | ||
Theorem | rhmco 20276 | The composition of ring homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β (πΉ β πΊ) β (π RingHom π)) | ||
Theorem | pwsco1rhm 20277* | 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 20278* | 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 20279 | 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 20280 | Alternate proof for f1ghm0to0 20279. Using ghmf1 19121 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 20281 | 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 20282 | 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 }) = {π})) | ||
Theorem | brric 20283 | The relation "is isomorphic to" for (unital) rings. (Contributed by AV, 24-Dec-2019.) |
β’ (π βπ π β (π RingIso π) β β ) | ||
Theorem | brrici 20284 | Prove isomorphic by an explicit isomorphism. (Contributed by SN, 10-Jan-2025.) |
β’ (πΉ β (π RingIso π) β π βπ π) | ||
Theorem | brric2 20285* | The relation "is isomorphic to" for (unital) rings. This theorem corresponds to Definition df-risc 36851 of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019.) |
β’ (π βπ π β ((π β Ring β§ π β Ring) β§ βπ π β (π RingIso π))) | ||
Theorem | ricgic 20286 | If two rings are (ring) isomorphic, their additive groups are (group) isomorphic. (Contributed by AV, 24-Dec-2019.) |
β’ (π βπ π β π βπ π) | ||
Theorem | rhmdvdsr 20287 | A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
β’ π = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ / = (β₯rβπ) β β’ (((πΉ β (π RingHom π) β§ π΄ β π β§ π΅ β π) β§ π΄ β₯ π΅) β (πΉβπ΄) / (πΉβπ΅)) | ||
Theorem | rhmopp 20288 | A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
β’ (πΉ β (π RingHom π) β πΉ β ((opprβπ ) RingHom (opprβπ))) | ||
Theorem | elrhmunit 20289 | Ring homomorphisms preserve unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
β’ ((πΉ β (π RingHom π) β§ π΄ β (Unitβπ )) β (πΉβπ΄) β (Unitβπ)) | ||
Theorem | rhmunitinv 20290 | Ring homomorphisms preserve the inverse of unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
β’ ((πΉ β (π RingHom π) β§ π΄ β (Unitβπ )) β (πΉβ((invrβπ )βπ΄)) = ((invrβπ)β(πΉβπ΄))) | ||
Syntax | cnzr 20291 | The class of nonzero rings. |
class NzRing | ||
Definition | df-nzr 20292 | A nonzero or nontrivial ring is a ring with at least two values, or equivalently where 1 and 0 are different. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ NzRing = {π β Ring β£ (1rβπ) β (0gβπ)} | ||
Theorem | isnzr 20293 | Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ (π β NzRing β (π β Ring β§ 1 β 0 )) | ||
Theorem | nzrnz 20294 | One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ (π β NzRing β 1 β 0 ) | ||
Theorem | nzrring 20295 | A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.) |
β’ (π β NzRing β π β Ring) | ||
Theorem | nzrringOLD 20296 | Obsolete version of nzrring 20295 as of 23-Feb-2025. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β NzRing β π β Ring) | ||
Theorem | isnzr2 20297 | Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β NzRing β (π β Ring β§ 2o βΌ π΅)) | ||
Theorem | isnzr2hash 20298 | Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 20297. (Contributed by AV, 14-Apr-2019.) |
β’ π΅ = (Baseβπ ) β β’ (π β NzRing β (π β Ring β§ 1 < (β―βπ΅))) | ||
Theorem | opprnzr 20299 | The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ π = (opprβπ ) β β’ (π β NzRing β π β NzRing) | ||
Theorem | ringelnzr 20300 | A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 13-Jun-2015.) |
β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β (π΅ β { 0 })) β π β NzRing) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |