| Metamath
Proof Explorer Theorem List (p. 205 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-dvr 20401* | Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
| ⊢ /r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦)))) | ||
| Theorem | dvrfval 20402* | 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 20403 | 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 20404 | Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝐵) | ||
| Theorem | unitdvcl 20405 | The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝑈) | ||
| Theorem | dvrid 20406 | A ring element divided by itself is the ring unity. (divid 11953 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 / 𝑋) = 1 ) | ||
| Theorem | dvr1 20407 | A ring element divided by the ring unity is itself. (div1 11957 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 / 1 ) = 𝑋) | ||
| Theorem | dvrass 20408 | An associative law for division. (divass 11940 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑌) / 𝑍) = (𝑋 · (𝑌 / 𝑍))) | ||
| Theorem | dvrcan1 20409 | A cancellation law for division. (divcan1 11931 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) · 𝑌) = 𝑋) | ||
| Theorem | dvrcan3 20410 | A cancellation law for division. (divcan3 11948 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 · 𝑌) / 𝑌) = 𝑋) | ||
| Theorem | dvreq1 20411 | Equality in terms of ratio equal to ring unity. (diveq1 11952 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) = 1 ↔ 𝑋 = 𝑌)) | ||
| Theorem | dvrdir 20412 | Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 + 𝑌) / 𝑍) = ((𝑋 / 𝑍) + (𝑌 / 𝑍))) | ||
| Theorem | rdivmuldivd 20413 | 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 20414 | 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 20415* | 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 20416* | 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 20417* | 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 20418* | 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 20419* | 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 20420* | 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 20421* | Expand out the class difference from isirred 20419. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (Irred‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 𝑋 → (𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈)))) | ||
| Theorem | opprirred 20422 | 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 20423 | The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 0 ) | ||
| Theorem | irredcl 20424 | An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ 𝐵) | ||
| Theorem | irrednu 20425 | An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐼 → ¬ 𝑋 ∈ 𝑈) | ||
| Theorem | irredn1 20426 | The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 1 ) | ||
| Theorem | irredrmul 20427 | The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝐼) | ||
| Theorem | irredlmul 20428 | The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼) → (𝑋 · 𝑌) ∈ 𝐼) | ||
| Theorem | irredmul 20429 | 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 20430 | The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼) | ||
| Theorem | irrednegb 20431 | An element is irreducible iff its negative is. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ 𝐼 ↔ (𝑁‘𝑋) ∈ 𝐼)) | ||
| Syntax | crpm 20432 | Syntax for the ring primes function. |
| class RPrime | ||
| Definition | df-rprm 20433* | 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 16750. Prime elements are closely related to irreducible elements (see df-irred 20359). (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ RPrime = (𝑤 ∈ V ↦ ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))}) | ||
| Syntax | crnghm 20434 | non-unital ring homomorphisms. |
| class RngHom | ||
| Syntax | crngim 20435 | non-unital ring isomorphisms. |
| class RngIso | ||
| Definition | df-rnghm 20436* | 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 20437* | Define the set of non-unital ring isomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.) |
| ⊢ RngIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RngHom 𝑟)}) | ||
| Theorem | rnghmrcl 20438 | Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.) |
| ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → (𝑅 ∈ Rng ∧ 𝑆 ∈ Rng)) | ||
| Theorem | rnghmfn 20439 | 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 20440* | 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 20441* | 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 20442 | 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 20443 | A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹 ∈ (𝑀 MgmHom 𝑁)) | ||
| Theorem | rnghmval2 20444 | 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 20445 | 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 20446 | Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.) |
| ⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V)) | ||
| Theorem | rnghmghm 20447 | A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.) |
| ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | ||
| Theorem | rnghmf 20448 | A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹:𝐵⟶𝐶) | ||
| Theorem | rnghmmul 20449 | A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵))) | ||
| Theorem | isrnghm2d 20450* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHom 𝑆)) | ||
| Theorem | isrnghmd 20451* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ⨣ = (+g‘𝑆) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHom 𝑆)) | ||
| Theorem | rnghmf1o 20452 | 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 20453 | 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 20454 | An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
| Theorem | rngimrnghm 20455 | An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → 𝐹 ∈ (𝑅 RngHom 𝑆)) | ||
| Theorem | rngimcnv 20456 | 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 20457 | The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.) |
| ⊢ ((𝐹 ∈ (𝑇 RngHom 𝑈) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RngHom 𝑈)) | ||
| Theorem | idrnghm 20458 | The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → ( I ↾ 𝐵) ∈ (𝑅 RngHom 𝑅)) | ||
| Theorem | c0mgm 20459* | 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 20460* | The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MndHom 𝑇)) | ||
| Theorem | c0ghm 20461* | The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → 𝐻 ∈ (𝑆 GrpHom 𝑇)) | ||
| Theorem | c0snmgmhm 20462* | 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 20463* | 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 20464* | 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 20465 | 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 20466* | 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 20467 | 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 20468 | 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 20469 | Extend class notation with the ring homomorphisms. |
| class RingHom | ||
| Syntax | crs 20470 | Extend class notation with the ring isomorphisms. |
| class RingIso | ||
| Syntax | cric 20471 | Extend class notation with the ring isomorphism relation. |
| class ≃𝑟 | ||
| Definition | df-rhm 20472* | 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 20473* | Define the set of ring isomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
| ⊢ RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)}) | ||
| Theorem | dfrhm2 20474* | 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 20475 | Define the ring isomorphism relation, analogous to df-gic 19278: 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 20476 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
| ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) | ||
| Theorem | rhmrcl2 20477 | Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
| ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring) | ||
| Theorem | isrhm 20478 | 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 20479 | A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑀 MndHom 𝑁)) | ||
| Theorem | rhmisrnghm 20480 | Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.) |
| ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 RngHom 𝑆)) | ||
| Theorem | isrim0OLD 20481 | Obsolete version of isrim0 20483 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RingHom 𝑅)))) | ||
| Theorem | rimrcl 20482 | Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019.) |
| ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V)) | ||
| Theorem | isrim0 20483 | A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 19283. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.) |
| ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RingHom 𝑅))) | ||
| Theorem | rhmghm 20484 | A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
| ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | ||
| Theorem | rhmf 20485 | A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐵⟶𝐶) | ||
| Theorem | rhmmul 20486 | A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵))) | ||
| Theorem | isrhm2d 20487* | Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (1r‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑆 ∈ Ring) & ⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) | ||
| Theorem | isrhmd 20488* | 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 20489 | Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
| ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (1r‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘ 1 ) = 𝑁) | ||
| Theorem | idrhm 20490 | The identity homomorphism on a ring. (Contributed by AV, 14-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → ( I ↾ 𝐵) ∈ (𝑅 RingHom 𝑅)) | ||
| Theorem | rhmf1o 20491 | 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 20492 | 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 20493 | Obsolete version of isrim 20492 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 20494 | An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
| Theorem | rimrhmOLD 20495 | Obsolete version of rimrhm 20496 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 20496 | A ring isomorphism is a homomorphism. Compare gimghm 19282. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.) |
| ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | ||
| Theorem | rimgim 20497 | An isomorphism of rings is an isomorphism of their additive groups. (Contributed by AV, 24-Dec-2019.) |
| ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 GrpIso 𝑆)) | ||
| Theorem | rimisrngim 20498 | Each unital ring isomorphism is a non-unital ring isomorphism. (Contributed by AV, 30-Mar-2025.) |
| ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RngIso 𝑆)) | ||
| Theorem | rhmfn 20499 | 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 20500 | The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.) |
| ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |