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