HomeTheorem List (p. 204 of 502)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 204 of 502) | < 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: | Metamath Proof Explorer
(1-31005) |
Hilbert Space Explorer
(31006-32528) |
Users' Mathboxes
(32529-50158) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mulgass3 20301 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ × = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 × (𝑁 · 𝑌)) = (𝑁 · (𝑋 × 𝑌))) | ||
| Syntax | cdsr 20302 | Ring divisibility relation. |
| class ∥r | ||
| Syntax | cui 20303 | Units in a ring. |
| class Unit | ||
| Syntax | cir 20304 | Ring irreducibles. |
| class Irred | ||
| Definition | df-dvdsr 20305* | Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through (∥r‘(oppr‘𝑅)). (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ ∥r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑤) ∧ ∃𝑧 ∈ (Base‘𝑤)(𝑧(.r‘𝑤)𝑥) = 𝑦)}) | ||
| Definition | df-unit 20306 | Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ Unit = (𝑤 ∈ V ↦ (◡((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤))) “ {(1r‘𝑤)})) | ||
| Definition | df-irred 20307* | Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ Irred = (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧}) | ||
| Theorem | reldvdsr 20308 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ Rel ∥ | ||
| Theorem | dvdsrval 20309* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ∥ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} | ||
| Theorem | dvdsr 20310* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)) | ||
| Theorem | dvdsr2 20311* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐵 → (𝑋 ∥ 𝑌 ↔ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)) | ||
| Theorem | dvdsrmul 20312 | A left-multiple of 𝑋 is divisible by 𝑋. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∥ (𝑌 · 𝑋)) | ||
| Theorem | dvdsrcl 20313 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑋 ∥ 𝑌 → 𝑋 ∈ 𝐵) | ||
| Theorem | dvdsrcl2 20314 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∥ 𝑌) → 𝑌 ∈ 𝐵) | ||
| Theorem | dvdsrid 20315 | An element in a (unital) ring divides itself. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ 𝑋) | ||
| Theorem | dvdsrtr 20316 | Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋) → 𝑌 ∥ 𝑋) | ||
| Theorem | dvdsrmul1 20317 | The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∥ 𝑌) → (𝑋 · 𝑍) ∥ (𝑌 · 𝑍)) | ||
| Theorem | dvdsrneg 20318 | An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ (𝑁‘𝑋)) | ||
| Theorem | dvdsr01 20319 | In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 20639.) (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ 0 ) | ||
| Theorem | dvdsr02 20320 | Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 ∥ 𝑋 ↔ 𝑋 = 0 )) | ||
| Theorem | isunit 20321 | Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 8-Dec-2015.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝑆 = (oppr‘𝑅) & ⊢ 𝐸 = (∥r‘𝑆) ⇒ ⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 )) | ||
| Theorem | 1unit 20322 | The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 1 ∈ 𝑈) | ||
| Theorem | unitcl 20323 | A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ 𝐵) | ||
| Theorem | unitss 20324 | The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ 𝑈 ⊆ 𝐵 | ||
| Theorem | opprunit 20325 | 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 20326 | Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∥ 1 )) | ||
| Theorem | dvdsunit 20327 | A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ∧ 𝑋 ∈ 𝑈) → 𝑌 ∈ 𝑈) | ||
| Theorem | unitmulcl 20328 | The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝑈) | ||
| Theorem | unitmulclb 20329 | Reversal of unitmulcl 20328 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) ∈ 𝑈 ↔ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈))) | ||
| Theorem | unitgrpbas 20330 | The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ 𝑈 = (Base‘𝐺) | ||
| Theorem | unitgrp 20331 | The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) | ||
| Theorem | unitabl 20332 | The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝑅 ∈ CRing → 𝐺 ∈ Abel) | ||
| Theorem | unitgrpid 20333 | 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 20334 | 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 20335 | Extend class notation with multiplicative inverse. |
| class invr | ||
| Definition | df-invr 20336 | Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.) |
| ⊢ invr = (𝑟 ∈ V ↦ (invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟)))) | ||
| Theorem | invrfval 20337 | 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 20338 | The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ 𝑈) | ||
| Theorem | unitinvinv 20339 | The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘(𝐼‘𝑋)) = 𝑋) | ||
| Theorem | ringinvcl 20340 | The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ 𝐵) | ||
| Theorem | unitlinv 20341 | 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 20342 | 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 20343 | 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 20344 | 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 20345 | The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈) | ||
| Theorem | ringunitnzdiv 20346 | 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 20347 | 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 20348 | Extend class notation with ring division. |
| class /r | ||
| Definition | df-dvr 20349* | Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
| ⊢ /r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦)))) | ||
| Theorem | dvrfval 20350* | 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 20351 | 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 20352 | Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝐵) | ||
| Theorem | unitdvcl 20353 | The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝑈) | ||
| Theorem | dvrid 20354 | A ring element divided by itself is the ring unity. (divid 11839 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 / 𝑋) = 1 ) | ||
| Theorem | dvr1 20355 | A ring element divided by the ring unity is itself. (div1 11843 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 / 1 ) = 𝑋) | ||
| Theorem | dvrass 20356 | An associative law for division. (divass 11826 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑌) / 𝑍) = (𝑋 · (𝑌 / 𝑍))) | ||
| Theorem | dvrcan1 20357 | A cancellation law for division. (divcan1 11817 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) · 𝑌) = 𝑋) | ||
| Theorem | dvrcan3 20358 | A cancellation law for division. (divcan3 11834 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 · 𝑌) / 𝑌) = 𝑋) | ||
| Theorem | dvreq1 20359 | Equality in terms of ratio equal to ring unity. (diveq1 11838 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) = 1 ↔ 𝑋 = 𝑌)) | ||
| Theorem | dvrdir 20360 | Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 + 𝑌) / 𝑍) = ((𝑋 / 𝑍) + (𝑌 / 𝑍))) | ||
| Theorem | rdivmuldivd 20361 | 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 20362 | 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 20363* | 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 20364* | 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 20365* | 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 20366* | 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 20367* | 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 20368* | 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 20369* | Expand out the class difference from isirred 20367. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (Irred‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 𝑋 → (𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈)))) | ||
| Theorem | opprirred 20370 | 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 20371 | The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 0 ) | ||
| Theorem | irredcl 20372 | An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ 𝐵) | ||
| Theorem | irrednu 20373 | An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐼 → ¬ 𝑋 ∈ 𝑈) | ||
| Theorem | irredn1 20374 | The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 1 ) | ||
| Theorem | irredrmul 20375 | The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝐼) | ||
| Theorem | irredlmul 20376 | The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼) → (𝑋 · 𝑌) ∈ 𝐼) | ||
| Theorem | irredmul 20377 | 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 20378 | The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼) | ||
| Theorem | irrednegb 20379 | An element is irreducible iff its negative is. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ 𝐼 ↔ (𝑁‘𝑋) ∈ 𝐼)) | ||
| Syntax | crpm 20380 | Syntax for the ring primes function. |
| class RPrime | ||
| Definition | df-rprm 20381* | 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 16652. Prime elements are closely related to irreducible elements (see df-irred 20307). (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ RPrime = (𝑤 ∈ V ↦ ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))}) | ||
| Syntax | crnghm 20382 | non-unital ring homomorphisms. |
| class RngHom | ||
| Syntax | crngim 20383 | non-unital ring isomorphisms. |
| class RngIso | ||
| Definition | df-rnghm 20384* | 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 20385* | Define the set of non-unital ring isomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.) |
| ⊢ RngIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RngHom 𝑟)}) | ||
| Theorem | rnghmrcl 20386 | Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.) |
| ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → (𝑅 ∈ Rng ∧ 𝑆 ∈ Rng)) | ||
| Theorem | rnghmfn 20387 | 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 20388* | 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 20389* | 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 20390 | 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 20391 | A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹 ∈ (𝑀 MgmHom 𝑁)) | ||
| Theorem | rnghmval2 20392 | 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 20393 | 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 20394 | Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.) |
| ⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V)) | ||
| Theorem | rnghmghm 20395 | A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.) |
| ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | ||
| Theorem | rnghmf 20396 | A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹:𝐵⟶𝐶) | ||
| Theorem | rnghmmul 20397 | A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵))) | ||
| Theorem | isrnghm2d 20398* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHom 𝑆)) | ||
| Theorem | isrnghmd 20399* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ⨣ = (+g‘𝑆) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHom 𝑆)) | ||
| Theorem | rnghmf1o 20400 | 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 𝑅))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |