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