Home | Metamath
Proof Explorer Theorem List (p. 194 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | qusring2 19301* | The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞))) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝑈 ∈ Ring ∧ [ 1 ] ∼ = (1r‘𝑈))) | ||
Theorem | crngbinom 19302* | The binomial theorem for commutative rings (special case of csrgbinom 19227): (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)). (Contributed by AV, 24-Aug-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) | ||
Syntax | coppr 19303 | The opposite ring operation. |
class oppr | ||
Definition | df-oppr 19304 | Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ oppr = (𝑓 ∈ V ↦ (𝑓 sSet 〈(.r‘ndx), tpos (.r‘𝑓)〉)) | ||
Theorem | opprval 19305 | Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ 𝑂 = (𝑅 sSet 〈(.r‘ndx), tpos · 〉) | ||
Theorem | opprmulfval 19306 | Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (.r‘𝑂) ⇒ ⊢ ∙ = tpos · | ||
Theorem | opprmul 19307 | Value of the multiplication operation of an opposite ring. Hypotheses eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (.r‘𝑂) ⇒ ⊢ (𝑋 ∙ 𝑌) = (𝑌 · 𝑋) | ||
Theorem | crngoppr 19308 | In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 19378). (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (.r‘𝑂) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∙ 𝑌)) | ||
Theorem | opprlem 19309 | Lemma for opprbas 19310 and oppradd 19311. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 3 ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑂) | ||
Theorem | opprbas 19310 | Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | oppradd 19311 | Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ + = (+g‘𝑂) | ||
Theorem | opprring 19312 | An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑂 ∈ Ring) | ||
Theorem | opprringb 19313 | Bidirectional form of opprring 19312. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring ↔ 𝑂 ∈ Ring) | ||
Theorem | oppr0 19314 | Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 0 = (0g‘𝑂) | ||
Theorem | oppr1 19315 | Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ 1 = (1r‘𝑂) | ||
Theorem | opprneg 19316 | The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ 𝑁 = (invg‘𝑂) | ||
Theorem | opprsubg 19317 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (SubGrp‘𝑅) = (SubGrp‘𝑂) | ||
Theorem | mulgass3 19318 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ × = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 × (𝑁 · 𝑌)) = (𝑁 · (𝑋 × 𝑌))) | ||
Syntax | cdsr 19319 | Ring divisibility relation. |
class ∥r | ||
Syntax | cui 19320 | Ring unit. |
class Unit | ||
Syntax | cir 19321 | Ring irreducibles. |
class Irred | ||
Definition | df-dvdsr 19322* | 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 19323 | 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 19324* | Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ Irred = (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧}) | ||
Theorem | reldvdsr 19325 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ Rel ∥ | ||
Theorem | dvdsrval 19326* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ∥ = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} | ||
Theorem | dvdsr 19327* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)) | ||
Theorem | dvdsr2 19328* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐵 → (𝑋 ∥ 𝑌 ↔ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)) | ||
Theorem | dvdsrmul 19329 | A left-multiple of 𝑋 is divisible by 𝑋. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∥ (𝑌 · 𝑋)) | ||
Theorem | dvdsrcl 19330 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑋 ∥ 𝑌 → 𝑋 ∈ 𝐵) | ||
Theorem | dvdsrcl2 19331 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∥ 𝑌) → 𝑌 ∈ 𝐵) | ||
Theorem | dvdsrid 19332 | 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 19333 | Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋) → 𝑌 ∥ 𝑋) | ||
Theorem | dvdsrmul1 19334 | The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∥ 𝑌) → (𝑋 · 𝑍) ∥ (𝑌 · 𝑍)) | ||
Theorem | dvdsrneg 19335 | An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ (𝑁‘𝑋)) | ||
Theorem | dvdsr01 19336 | In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 19986.) (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ 0 ) | ||
Theorem | dvdsr02 19337 | Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 ∥ 𝑋 ↔ 𝑋 = 0 )) | ||
Theorem | isunit 19338 | 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 19339 | The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 1 ∈ 𝑈) | ||
Theorem | unitcl 19340 | A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ 𝐵) | ||
Theorem | unitss 19341 | The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ 𝑈 ⊆ 𝐵 | ||
Theorem | opprunit 19342 | 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 19343 | Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∥ 1 )) | ||
Theorem | dvdsunit 19344 | A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ∧ 𝑋 ∈ 𝑈) → 𝑌 ∈ 𝑈) | ||
Theorem | unitmulcl 19345 | The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝑈) | ||
Theorem | unitmulclb 19346 | Reversal of unitmulcl 19345 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) ∈ 𝑈 ↔ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈))) | ||
Theorem | unitgrpbas 19347 | The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ 𝑈 = (Base‘𝐺) | ||
Theorem | unitgrp 19348 | The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) | ||
Theorem | unitabl 19349 | The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝑅 ∈ CRing → 𝐺 ∈ Abel) | ||
Theorem | unitgrpid 19350 | The identity of the multiplicative group is 1r. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 1 = (0g‘𝐺)) | ||
Theorem | unitsubm 19351 | 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 19352 | Extend class notation with multiplicative inverse. |
class invr | ||
Definition | df-invr 19353 | Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.) |
⊢ invr = (𝑟 ∈ V ↦ (invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟)))) | ||
Theorem | invrfval 19354 | 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 19355 | The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ 𝑈) | ||
Theorem | unitinvinv 19356 | The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘(𝐼‘𝑋)) = 𝑋) | ||
Theorem | ringinvcl 19357 | The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ 𝐵) | ||
Theorem | unitlinv 19358 | A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝐼‘𝑋) · 𝑋) = 1 ) | ||
Theorem | unitrinv 19359 | A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 · (𝐼‘𝑋)) = 1 ) | ||
Theorem | 1rinv 19360 | The inverse of the identity is the identity. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝐼 = (invr‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐼‘ 1 ) = 1 ) | ||
Theorem | 0unit 19361 | 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 19362 | The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈) | ||
Syntax | cdvr 19363 | Extend class notation with ring division. |
class /r | ||
Definition | df-dvr 19364* | Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
⊢ /r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦)))) | ||
Theorem | dvrfval 19365* | 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 19366 | 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 19367 | Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝐵) | ||
Theorem | unitdvcl 19368 | The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝑈) | ||
Theorem | dvrid 19369 | A cancellation law for division. (divid 11316 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 / 𝑋) = 1 ) | ||
Theorem | dvr1 19370 | A cancellation law for division. (div1 11318 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 / 1 ) = 𝑋) | ||
Theorem | dvrass 19371 | An associative law for division. (divass 11305 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑌) / 𝑍) = (𝑋 · (𝑌 / 𝑍))) | ||
Theorem | dvrcan1 19372 | A cancellation law for division. (divcan1 11296 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) · 𝑌) = 𝑋) | ||
Theorem | dvrcan3 19373 | A cancellation law for division. (divcan3 11313 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 · 𝑌) / 𝑌) = 𝑋) | ||
Theorem | dvreq1 19374 | A cancellation law for division. (diveq1 11320 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) = 1 ↔ 𝑋 = 𝑌)) | ||
Theorem | ringinvdv 19375 | 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 19376* | The ring identity 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 19377* | 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 19378* | 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 19379* | 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 19380* | 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 19381* | 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 19382* | Expand out the class difference from isirred 19380. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (Irred‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 𝑋 → (𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈)))) | ||
Theorem | opprirred 19383 | 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 19384 | The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐼 = (Irred‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 0 ) | ||
Theorem | irredcl 19385 | An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ 𝐵) | ||
Theorem | irrednu 19386 | An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐼 → ¬ 𝑋 ∈ 𝑈) | ||
Theorem | irredn1 19387 | The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐼 = (Irred‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 1 ) | ||
Theorem | irredrmul 19388 | The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝐼) | ||
Theorem | irredlmul 19389 | The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼) → (𝑋 · 𝑌) ∈ 𝐼) | ||
Theorem | irredmul 19390 | 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 19391 | The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼) | ||
Theorem | irrednegb 19392 | An element is irreducible iff its negative is. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐼 = (Irred‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ 𝐼 ↔ (𝑁‘𝑋) ∈ 𝐼)) | ||
Syntax | crpm 19393 | Syntax for the ring primes function. |
class RPrime | ||
Definition | df-rprm 19394* | 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 16047. Prime elements are closely related to irreducible elements (see df-irred 19324). (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ RPrime = (𝑤 ∈ V ↦ ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))}) | ||
Syntax | crh 19395 | Extend class notation with the ring homomorphisms. |
class RingHom | ||
Syntax | crs 19396 | Extend class notation with the ring isomorphisms. |
class RingIso | ||
Syntax | cric 19397 | Extend class notation with the ring isomorphism relation. |
class ≃𝑟 | ||
Definition | df-rnghom 19398* | 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-rngiso 19399* | Define the set of ring isomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)}) | ||
Theorem | dfrhm2 19400* | 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 > |