![]() |
Metamath
Proof Explorer Theorem List (p. 204 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvrcan1 20301 | A cancellation law for division. (divcan1 11886 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π / π) Β· π) = π) | ||
Theorem | dvrcan3 20302 | A cancellation law for division. (divcan3 11903 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π Β· π) / π) = π) | ||
Theorem | dvreq1 20303 | Equality in terms of ratio equal to ring unity. (diveq1 11910 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π / π) = 1 β π = π)) | ||
Theorem | dvrdir 20304 | Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ + = (+gβπ ) & β’ / = (/rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π + π) / π) = ((π / π) + (π / π))) | ||
Theorem | rdivmuldivd 20305 | 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 20306 | 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 20307* | 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 20308* | 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 20309* | 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 20310* | 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 20311* | 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 20312* | 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 20313* | Expand out the class difference from isirred 20311. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (Irredβπ ) & β’ Β· = (.rβπ ) β β’ (π β πΌ β (π β π΅ β§ Β¬ π β π β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) | ||
Theorem | opprirred 20314 | 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 20315 | The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β πΌ) β π β 0 ) | ||
Theorem | irredcl 20316 | An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β πΌ β π β π΅) | ||
Theorem | irrednu 20317 | An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (Unitβπ ) β β’ (π β πΌ β Β¬ π β π) | ||
Theorem | irredn1 20318 | The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β πΌ) β π β 1 ) | ||
Theorem | irredrmul 20319 | The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β πΌ β§ π β π) β (π Β· π) β πΌ) | ||
Theorem | irredlmul 20320 | The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π β§ π β πΌ) β (π Β· π) β πΌ) | ||
Theorem | irredmul 20321 | 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 20322 | The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ π β πΌ) β (πβπ) β πΌ) | ||
Theorem | irrednegb 20323 | An element is irreducible iff its negative is. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ πΌ = (Irredβπ ) & β’ π = (invgβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β π΅) β (π β πΌ β (πβπ) β πΌ)) | ||
Syntax | crpm 20324 | Syntax for the ring primes function. |
class RPrime | ||
Definition | df-rprm 20325* | 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 16655. Prime elements are closely related to irreducible elements (see df-irred 20251). (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ RPrime = (π€ β V β¦ β¦(Baseβπ€) / πβ¦{π β (π β ((Unitβπ€) βͺ {(0gβπ€)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦))}) | ||
Syntax | crnghm 20326 | non-unital ring homomorphisms. |
class RngHom | ||
Syntax | crngim 20327 | non-unital ring isomorphisms. |
class RngIso | ||
Definition | df-rnghm 20328* | Define the set of non-unital ring homomorphisms from π to π . (Contributed by AV, 20-Feb-2020.) |
β’ RngHom = (π β Rng, π β Rng β¦ β¦(Baseβπ) / π£β¦β¦(Baseβπ ) / π€β¦{π β (π€ βm π£) β£ βπ₯ β π£ βπ¦ β π£ ((πβ(π₯(+gβπ)π¦)) = ((πβπ₯)(+gβπ )(πβπ¦)) β§ (πβ(π₯(.rβπ)π¦)) = ((πβπ₯)(.rβπ )(πβπ¦)))}) | ||
Definition | df-rngim 20329* | Define the set of non-unital ring isomorphisms from π to π . (Contributed by AV, 20-Feb-2020.) |
β’ RngIso = (π β V, π β V β¦ {π β (π RngHom π ) β£ β‘π β (π RngHom π)}) | ||
Theorem | rnghmrcl 20330 | Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.) |
β’ (πΉ β (π RngHom π) β (π β Rng β§ π β Rng)) | ||
Theorem | rnghmfn 20331 | The mapping of two non-unital rings to the non-unital ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.) |
β’ RngHom Fn (Rng Γ Rng) | ||
Theorem | rnghmval 20332* | The set of the non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 22-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) & β’ πΆ = (Baseβπ) & β’ + = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β Rng β§ π β Rng) β (π RngHom π) = {π β (πΆ βm π΅) β£ βπ₯ β π΅ βπ¦ β π΅ ((πβ(π₯ + π¦)) = ((πβπ₯) β (πβπ¦)) β§ (πβ(π₯ Β· π¦)) = ((πβπ₯) β (πβπ¦)))}) | ||
Theorem | isrnghm 20333* | A function is a non-unital ring homomorphism iff it is a group homomorphism and preserves multiplication. (Contributed by AV, 22-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (πΉ β (π RngHom π) β ((π β Rng β§ π β Rng) β§ (πΉ β (π GrpHom π) β§ βπ₯ β π΅ βπ¦ β π΅ (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) β (πΉβπ¦))))) | ||
Theorem | isrnghmmul 20334 | A function is a non-unital ring homomorphism iff it preserves both addition and multiplication. (Contributed by AV, 27-Feb-2020.) |
β’ π = (mulGrpβπ ) & β’ π = (mulGrpβπ) β β’ (πΉ β (π RngHom π) β ((π β Rng β§ π β Rng) β§ (πΉ β (π GrpHom π) β§ πΉ β (π MgmHom π)))) | ||
Theorem | rnghmmgmhm 20335 | A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.) |
β’ π = (mulGrpβπ ) & β’ π = (mulGrpβπ) β β’ (πΉ β (π RngHom π) β πΉ β (π MgmHom π)) | ||
Theorem | rnghmval2 20336 | The non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 1-Mar-2020.) |
β’ ((π β Rng β§ π β Rng) β (π RngHom π) = ((π GrpHom π) β© ((mulGrpβπ ) MgmHom (mulGrpβπ)))) | ||
Theorem | isrngim 20337 | An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020.) |
β’ ((π β π β§ π β π) β (πΉ β (π RngIso π) β (πΉ β (π RngHom π) β§ β‘πΉ β (π RngHom π )))) | ||
Theorem | rngimrcl 20338 | Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.) |
β’ (πΉ β (π RngIso π) β (π β V β§ π β V)) | ||
Theorem | rnghmghm 20339 | A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.) |
β’ (πΉ β (π RngHom π) β πΉ β (π GrpHom π)) | ||
Theorem | rnghmf 20340 | A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RngHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | rnghmmul 20341 | A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.) |
β’ π = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) β β’ ((πΉ β (π RngHom π) β§ π΄ β π β§ π΅ β π) β (πΉβ(π΄ Β· π΅)) = ((πΉβπ΄) Γ (πΉβπ΅))) | ||
Theorem | isrnghm2d 20342* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) & β’ (π β π β Rng) & β’ (π β π β Rng) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Γ (πΉβπ¦))) & β’ (π β πΉ β (π GrpHom π)) β β’ (π β πΉ β (π RngHom π)) | ||
Theorem | isrnghmd 20343* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) & β’ (π β π β Rng) & β’ (π β π β Rng) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Γ (πΉβπ¦))) & β’ πΆ = (Baseβπ) & β’ + = (+gβπ ) & ⒠⨣ = (+gβπ) & β’ (π β πΉ:π΅βΆπΆ) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦))) β β’ (π β πΉ β (π RngHom π)) | ||
Theorem | rnghmf1o 20344 | A non-unital ring homomorphism is bijective iff its converse is also a non-unital ring homomorphism. (Contributed by AV, 27-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RngHom π) β (πΉ:π΅β1-1-ontoβπΆ β β‘πΉ β (π RngHom π ))) | ||
Theorem | isrngim2 20345 | An isomorphism of non-unital rings is a bijective homomorphism. (Contributed by AV, 23-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ ((π β π β§ π β π) β (πΉ β (π RngIso π) β (πΉ β (π RngHom π) β§ πΉ:π΅β1-1-ontoβπΆ))) | ||
Theorem | rngimf1o 20346 | An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RngIso π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Theorem | rngimrnghm 20347 | An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RngIso π) β πΉ β (π RngHom π)) | ||
Theorem | rngimcnv 20348 | The converse of an isomorphism of non-unital rings is an isomorphism of non-unital rings. (Contributed by AV, 27-Feb-2025.) |
β’ (πΉ β (π RngIso π) β β‘πΉ β (π RngIso π)) | ||
Theorem | rnghmco 20349 | The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.) |
β’ ((πΉ β (π RngHom π) β§ πΊ β (π RngHom π)) β (πΉ β πΊ) β (π RngHom π)) | ||
Theorem | idrnghm 20350 | The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.) |
β’ π΅ = (Baseβπ ) β β’ (π β Rng β ( I βΎ π΅) β (π RngHom π )) | ||
Theorem | c0mgm 20351* | The constant mapping to zero is a magma homomorphism into a monoid. Remark: Instead of the assumption that T is a monoid, it would be sufficient that T is a magma with a right or left identity. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π₯ β π΅ β¦ 0 ) β β’ ((π β Mgm β§ π β Mnd) β π» β (π MgmHom π)) | ||
Theorem | c0mhm 20352* | The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π₯ β π΅ β¦ 0 ) β β’ ((π β Mnd β§ π β Mnd) β π» β (π MndHom π)) | ||
Theorem | c0ghm 20353* | The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π₯ β π΅ β¦ 0 ) β β’ ((π β Grp β§ π β Grp) β π» β (π GrpHom π)) | ||
Theorem | c0snmgmhm 20354* | The constant mapping to zero is a magma homomorphism from a magma with one element to any monoid. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π₯ β π΅ β¦ 0 ) β β’ ((π β Mnd β§ π β Mgm β§ (β―βπ΅) = 1) β π» β (π MgmHom π)) | ||
Theorem | c0snmhm 20355* | The constant mapping to zero is a monoid homomorphism from the trivial monoid (consisting of the zero only) to any monoid. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π₯ β π΅ β¦ 0 ) & β’ π = (0gβπ) β β’ ((π β Mnd β§ π β Mnd β§ π΅ = {π}) β π» β (π MndHom π)) | ||
Theorem | c0snghm 20356* | The constant mapping to zero is a group homomorphism from the trivial group (consisting of the zero only) to any group. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π₯ β π΅ β¦ 0 ) & β’ π = (0gβπ) β β’ ((π β Grp β§ π β Grp β§ π΅ = {π}) β π» β (π GrpHom π)) | ||
Theorem | rngisomfv1 20357 | If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the function value of the ring unity of the unital ring is an element of the base set of the non-unital ring. (Contributed by AV, 27-Feb-2025.) |
β’ 1 = (1rβπ ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β (π RngIso π)) β (πΉβ 1 ) β π΅) | ||
Theorem | rngisom1 20358* | If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the function value of the ring unity of the unital ring is a ring unity of the non-unital ring. (Contributed by AV, 27-Feb-2025.) |
β’ 1 = (1rβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) β β’ ((π β Ring β§ π β Rng β§ πΉ β (π RngIso π)) β βπ₯ β π΅ (((πΉβ 1 ) Β· π₯) = π₯ β§ (π₯ Β· (πΉβ 1 )) = π₯)) | ||
Theorem | rngisomring 20359 | If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then both rings are unital. (Contributed by AV, 27-Feb-2025.) |
β’ ((π β Ring β§ π β Rng β§ πΉ β (π RngIso π)) β π β Ring) | ||
Theorem | rngisomring1 20360 | If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the ring unity of the second ring is the function value of the ring unity of the first ring for the isomorphism. (Contributed by AV, 16-Mar-2025.) |
β’ ((π β Ring β§ π β Rng β§ πΉ β (π RngIso π)) β (1rβπ) = (πΉβ(1rβπ ))) | ||
Syntax | crh 20361 | Extend class notation with the ring homomorphisms. |
class RingHom | ||
Syntax | crs 20362 | Extend class notation with the ring isomorphisms. |
class RingIso | ||
Syntax | cric 20363 | Extend class notation with the ring isomorphism relation. |
class βπ | ||
Definition | df-rhm 20364* | 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-rim 20365* | Define the set of ring isomorphisms from π to π . (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ RingIso = (π β V, π β V β¦ {π β (π RingHom π ) β£ β‘π β (π RingHom π)}) | ||
Theorem | dfrhm2 20366* | 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 20367 | Define the ring isomorphism relation, analogous to df-gic 19175: 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 20368 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π RingHom π) β π β Ring) | ||
Theorem | rhmrcl2 20369 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π RingHom π) β π β Ring) | ||
Theorem | isrhm 20370 | 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 20371 | A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ π = (mulGrpβπ ) & β’ π = (mulGrpβπ) β β’ (πΉ β (π RingHom π) β πΉ β (π MndHom π)) | ||
Theorem | rhmisrnghm 20372 | Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.) |
β’ (πΉ β (π RingHom π) β πΉ β (π RngHom π)) | ||
Theorem | isrim0OLD 20373 | Obsolete version of isrim0 20375 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β π β§ π β π) β (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π )))) | ||
Theorem | rimrcl 20374 | Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019.) |
β’ (πΉ β (π RingIso π) β (π β V β§ π β V)) | ||
Theorem | isrim0 20375 | A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 19180. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.) |
β’ (πΉ β (π RingIso π) β (πΉ β (π RingHom π) β§ β‘πΉ β (π RingHom π ))) | ||
Theorem | rhmghm 20376 | A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π RingHom π) β πΉ β (π GrpHom π)) | ||
Theorem | rhmf 20377 | A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RingHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | rhmmul 20378 | A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) β β’ ((πΉ β (π RingHom π) β§ π΄ β π β§ π΅ β π) β (πΉβ(π΄ Β· π΅)) = ((πΉβπ΄) Γ (πΉβπ΅))) | ||
Theorem | isrhm2d 20379* | Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) & β’ π = (1rβπ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) & β’ (π β π β Ring) & β’ (π β π β Ring) & β’ (π β (πΉβ 1 ) = π) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Γ (πΉβπ¦))) & β’ (π β πΉ β (π GrpHom π)) β β’ (π β πΉ β (π RingHom π)) | ||
Theorem | isrhmd 20380* | 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 20381 | Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ 1 = (1rβπ ) & β’ π = (1rβπ) β β’ (πΉ β (π RingHom π) β (πΉβ 1 ) = π) | ||
Theorem | idrhm 20382 | The identity homomorphism on a ring. (Contributed by AV, 14-Feb-2020.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β ( I βΎ π΅) β (π RingHom π )) | ||
Theorem | rhmf1o 20383 | 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 20384 | 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 20385 | Obsolete version of isrim 20384 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 20386 | An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π RingIso π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Theorem | rimrhmOLD 20387 | Obsolete version of rimrhm 20388 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 20388 | A ring isomorphism is a homomorphism. Compare gimghm 19179. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.) |
β’ (πΉ β (π RingIso π) β πΉ β (π RingHom π)) | ||
Theorem | rimgim 20389 | An isomorphism of rings is an isomorphism of their additive groups. (Contributed by AV, 24-Dec-2019.) |
β’ (πΉ β (π RingIso π) β πΉ β (π GrpIso π)) | ||
Theorem | rimisrngim 20390 | Each unital ring isomorphism is a non-unital ring isomorphism. (Contributed by AV, 30-Mar-2025.) |
β’ (πΉ β (π RingIso π) β πΉ β (π RngIso π)) | ||
Theorem | rhmfn 20391 | The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.) |
β’ RingHom Fn (Ring Γ Ring) | ||
Theorem | rhmval 20392 | The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.) |
β’ ((π β Ring β§ π β Ring) β (π RingHom π) = ((π GrpHom π) β© ((mulGrpβπ ) MndHom (mulGrpβπ)))) | ||
Theorem | rhmco 20393 | The composition of ring homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ ((πΉ β (π RingHom π) β§ πΊ β (π RingHom π)) β (πΉ β πΊ) β (π RingHom π)) | ||
Theorem | pwsco1rhm 20394* | 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 20395* | 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 | brric 20396 | The relation "is isomorphic to" for (unital) rings. (Contributed by AV, 24-Dec-2019.) |
β’ (π βπ π β (π RingIso π) β β ) | ||
Theorem | brrici 20397 | Prove isomorphic by an explicit isomorphism. (Contributed by SN, 10-Jan-2025.) |
β’ (πΉ β (π RingIso π) β π βπ π) | ||
Theorem | brric2 20398* | The relation "is isomorphic to" for (unital) rings. This theorem corresponds to Definition df-risc 37155 of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019.) |
β’ (π βπ π β ((π β Ring β§ π β Ring) β§ βπ π β (π RingIso π))) | ||
Theorem | ricgic 20399 | If two rings are (ring) isomorphic, their additive groups are (group) isomorphic. (Contributed by AV, 24-Dec-2019.) |
β’ (π βπ π β π βπ π) | ||
Theorem | rhmdvdsr 20400 | A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
β’ π = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ / = (β₯rβπ) β β’ (((πΉ β (π RingHom π) β§ π΄ β π β§ π΅ β π) β§ π΄ β₯ π΅) β (πΉβπ΄) / (πΉβπ΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |