![]() |
Metamath
Proof Explorer Theorem List (p. 204 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 | ringpropd 20301* | If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a ring iff the other one is. (Contributed by Mario Carneiro, 6-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Ring ↔ 𝐿 ∈ Ring)) | ||
Theorem | crngpropd 20302* | If two structures have the same group components (properties), one is a commutative ring iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ CRing ↔ 𝐿 ∈ CRing)) | ||
Theorem | ringprop 20303 | If two structures have the same ring components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) |
⊢ (Base‘𝐾) = (Base‘𝐿) & ⊢ (+g‘𝐾) = (+g‘𝐿) & ⊢ (.r‘𝐾) = (.r‘𝐿) ⇒ ⊢ (𝐾 ∈ Ring ↔ 𝐿 ∈ Ring) | ||
Theorem | isringd 20304* | Properties that determine a ring. (Contributed by NM, 2-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) & ⊢ (𝜑 → 1 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥) ⇒ ⊢ (𝜑 → 𝑅 ∈ Ring) | ||
Theorem | iscrngd 20305* | Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) & ⊢ (𝜑 → 1 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) ⇒ ⊢ (𝜑 → 𝑅 ∈ CRing) | ||
Theorem | ringlz 20306 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) (Proof shortened by AV, 30-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 ) | ||
Theorem | ringrz 20307 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) (Proof shortened by AV, 30-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 ) | ||
Theorem | ringlzd 20308 | The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 0 · 𝑋) = 0 ) | ||
Theorem | ringrzd 20309 | The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 0 ) = 0 ) | ||
Theorem | ringsrg 20310 | Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing) | ||
Theorem | ring1eq0 20311 | If one and zero are equal, then any two elements of a ring are equal. Alternately, every ring has one distinct from zero except the zero ring containing the single element {0}. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( 1 = 0 → 𝑋 = 𝑌)) | ||
Theorem | ring1ne0 20312 | If a ring has at least two elements, its one and zero are different. (Contributed by AV, 13-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 1 < (♯‘𝐵)) → 1 ≠ 0 ) | ||
Theorem | ringinvnz1ne0 20313* | In a unital ring, a left invertible element is different from zero iff 1 ≠ 0. (Contributed by FL, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 (𝑎 · 𝑋) = 1 ) ⇒ ⊢ (𝜑 → (𝑋 ≠ 0 ↔ 1 ≠ 0 )) | ||
Theorem | ringinvnzdiv 20314* | In a unital ring, a left invertible element is not a zero divisor. (Contributed by FL, 18-Apr-2010.) (Revised by Jeff Madsen, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 (𝑎 · 𝑋) = 1 ) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑌 = 0 )) | ||
Theorem | ringnegl 20315 | Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 37927 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘ 1 ) · 𝑋) = (𝑁‘𝑋)) | ||
Theorem | ringnegr 20316 | Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 37928 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑁‘ 1 )) = (𝑁‘𝑋)) | ||
Theorem | ringmneg1 20317 | Negation of a product in a ring. (mulneg1 11696 analog.) Compared with rngmneg1 20184, the proof is shorter making use of the existence of a ring unity. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) · 𝑌) = (𝑁‘(𝑋 · 𝑌))) | ||
Theorem | ringmneg2 20318 | Negation of a product in a ring. (mulneg2 11697 analog.) Compared with rngmneg2 20185, the proof is shorter making use of the existence of a ring unity. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑁‘𝑌)) = (𝑁‘(𝑋 · 𝑌))) | ||
Theorem | ringm2neg 20319 | Double negation of a product in a ring. (mul2neg 11699 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) (Proof shortened by AV, 30-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = (𝑋 · 𝑌)) | ||
Theorem | ringsubdi 20320 | Ring multiplication distributes over subtraction. (subdi 11693 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑌 − 𝑍)) = ((𝑋 · 𝑌) − (𝑋 · 𝑍))) | ||
Theorem | ringsubdir 20321 | Ring multiplication distributes over subtraction. (subdir 11694 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) · 𝑍) = ((𝑋 · 𝑍) − (𝑌 · 𝑍))) | ||
Theorem | mulgass2 20322 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ × = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌))) | ||
Theorem | ring1 20323 | The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉, 〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ⇒ ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Ring) | ||
Theorem | ringn0 20324 | Rings exist. (Contributed by AV, 29-Apr-2019.) |
⊢ Ring ≠ ∅ | ||
Theorem | ringlghm 20325* | Left-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) ∈ (𝑅 GrpHom 𝑅)) | ||
Theorem | ringrghm 20326* | Right-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)) ∈ (𝑅 GrpHom 𝑅)) | ||
Theorem | gsummulc1OLD 20327* | Obsolete version of gsummulc1 20329 as of 7-Mar-2025. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌)) | ||
Theorem | gsummulc2OLD 20328* | Obsolete version of gsummulc2 20330 as of 7-Mar-2025. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑌 · 𝑋))) = (𝑌 · (𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)))) | ||
Theorem | gsummulc1 20329* | A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) Remove unused hypothesis. (Revised by SN, 7-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌)) | ||
Theorem | gsummulc2 20330* | A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) Remove unused hypothesis. (Revised by SN, 7-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑌 · 𝑋))) = (𝑌 · (𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)))) | ||
Theorem | gsummgp0 20331* | If one factor in a finite group sum of the multiplicative group of a commutative ring is 0, the whole "sum" (i.e. product) is 0. (Contributed by AV, 3-Jan-2019.) |
⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅)) & ⊢ ((𝜑 ∧ 𝑛 = 𝑖) → 𝐴 = 𝐵) & ⊢ (𝜑 → ∃𝑖 ∈ 𝑁 𝐵 = 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ 𝐴)) = 0 ) | ||
Theorem | gsumdixp 20332* | Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.) (Revised by AV, 10-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑋) finSupp 0 ) & ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑌) finSupp 0 ) ⇒ ⊢ (𝜑 → ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ 𝑋)) · (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌))) = (𝑅 Σg (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)))) | ||
Theorem | prdsmulrcl 20333 | A structure product of rings has closed binary operation. (Contributed by Mario Carneiro, 11-Mar-2015.) (Proof shortened by AV, 30-Mar-2025.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵) | ||
Theorem | prdsringd 20334 | A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Ring) ⇒ ⊢ (𝜑 → 𝑌 ∈ Ring) | ||
Theorem | prdscrngd 20335 | A product of commutative rings is a commutative ring. Since the resulting ring will have zero divisors in all nontrivial cases, this cannot be strengthened much further. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶CRing) ⇒ ⊢ (𝜑 → 𝑌 ∈ CRing) | ||
Theorem | prds1 20336 | Value of the ring unity in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Ring) ⇒ ⊢ (𝜑 → (1r ∘ 𝑅) = (1r‘𝑌)) | ||
Theorem | pwsring 20337 | A structure power of a ring is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Ring) | ||
Theorem | pws1 20338 | Value of the ring unity in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × { 1 }) = (1r‘𝑌)) | ||
Theorem | pwscrng 20339 | A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ CRing) | ||
Theorem | pwsmgp 20340 | The multiplicative group of the power structure resembles the power of the multiplicative group. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (𝑀 ↑s 𝐼) & ⊢ 𝑁 = (mulGrp‘𝑌) & ⊢ 𝐵 = (Base‘𝑁) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ + = (+g‘𝑁) & ⊢ ✚ = (+g‘𝑍) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 = 𝐶 ∧ + = ✚ )) | ||
Theorem | pwspjmhmmgpd 20341* | The projection given by pwspjmhm 18855 is also a monoid homomorphism between the respective multiplicative groups. (Contributed by SN, 30-Jul-2024.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑇 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑀 MndHom 𝑇)) | ||
Theorem | pwsexpg 20342 | Value of a group exponentiation in a structure power. Compare pwsmulg 19149. (Contributed by SN, 30-Jul-2024.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑇 = (mulGrp‘𝑅) & ⊢ ∙ = (.g‘𝑀) & ⊢ · = (.g‘𝑇) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝑁 ∙ 𝑋)‘𝐴) = (𝑁 · (𝑋‘𝐴))) | ||
Theorem | imasring 20343* | The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝑈 ∈ Ring ∧ (𝐹‘ 1 ) = (1r‘𝑈))) | ||
Theorem | imasringf1 20344 | The image of a ring under an injection is a ring (imasmndf1 18801 analog). (Contributed by AV, 27-Feb-2025.) |
⊢ 𝑈 = (𝐹 “s 𝑅) & ⊢ 𝑉 = (Base‘𝑅) ⇒ ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Ring) → 𝑈 ∈ Ring) | ||
Theorem | xpsringd 20345 | A product of two rings is a ring (xpsmnd 18802 analog). (Contributed by AV, 28-Feb-2025.) |
⊢ 𝑌 = (𝑆 ×s 𝑅) & ⊢ (𝜑 → 𝑆 ∈ Ring) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑌 ∈ Ring) | ||
Theorem | xpsring1d 20346 | The multiplicative identity element of a binary product of rings. (Contributed by AV, 16-Mar-2025.) |
⊢ 𝑌 = (𝑆 ×s 𝑅) & ⊢ (𝜑 → 𝑆 ∈ Ring) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (1r‘𝑌) = 〈(1r‘𝑆), (1r‘𝑅)〉) | ||
Theorem | qusring2 20347* | 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 20348* | The binomial theorem for commutative rings (special case of csrgbinom 20249): (𝐴 + 𝐵)↑𝑁 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 20349 | The opposite ring operation. |
class oppr | ||
Definition | df-oppr 20350 | 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 20351 | Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ 𝑂 = (𝑅 sSet 〈(.r‘ndx), tpos · 〉) | ||
Theorem | opprmulfval 20352 | Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (.r‘𝑂) ⇒ ⊢ ∙ = tpos · | ||
Theorem | opprmul 20353 | 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 20354 | In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 20433). (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (.r‘𝑂) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∙ 𝑌)) | ||
Theorem | opprlem 20355 | Lemma for opprbas 20357 and oppradd 20359. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (.r‘ndx) ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑂) | ||
Theorem | opprlemOLD 20356 | Obsolete version of opprlem 20355 as of 6-Nov-2024. Lemma for opprbas 20357 and oppradd 20359. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 3 ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑂) | ||
Theorem | opprbas 20357 | Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | opprbasOLD 20358 | Obsolete version of opprbas 20357 as of 6-Nov-2024. Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | oppradd 20359 | Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ + = (+g‘𝑂) | ||
Theorem | oppraddOLD 20360 | Obsolete version of opprbas 20357 as of 6-Nov-2024. Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ + = (+g‘𝑂) | ||
Theorem | opprrng 20361 | An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → 𝑂 ∈ Rng) | ||
Theorem | opprrngb 20362 | A class is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 20361. (Contributed by AV, 15-Feb-2025.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng ↔ 𝑂 ∈ Rng) | ||
Theorem | opprring 20363 | An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.) (Proof shortened by AV, 30-Mar-2025.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑂 ∈ Ring) | ||
Theorem | opprringb 20364 | Bidirectional form of opprring 20363. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring ↔ 𝑂 ∈ Ring) | ||
Theorem | oppr0 20365 | Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 0 = (0g‘𝑂) | ||
Theorem | oppr1 20366 | Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ 1 = (1r‘𝑂) | ||
Theorem | opprneg 20367 | 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 20368 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (SubGrp‘𝑅) = (SubGrp‘𝑂) | ||
Theorem | mulgass3 20369 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ × = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 × (𝑁 · 𝑌)) = (𝑁 · (𝑋 × 𝑌))) | ||
Syntax | cdsr 20370 | Ring divisibility relation. |
class ∥r | ||
Syntax | cui 20371 | Units in a ring. |
class Unit | ||
Syntax | cir 20372 | Ring irreducibles. |
class Irred | ||
Definition | df-dvdsr 20373* | 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 20374 | 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 20375* | Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ Irred = (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧}) | ||
Theorem | reldvdsr 20376 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ Rel ∥ | ||
Theorem | dvdsrval 20377* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ∥ = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} | ||
Theorem | dvdsr 20378* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)) | ||
Theorem | dvdsr2 20379* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐵 → (𝑋 ∥ 𝑌 ↔ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)) | ||
Theorem | dvdsrmul 20380 | A left-multiple of 𝑋 is divisible by 𝑋. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∥ (𝑌 · 𝑋)) | ||
Theorem | dvdsrcl 20381 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑋 ∥ 𝑌 → 𝑋 ∈ 𝐵) | ||
Theorem | dvdsrcl2 20382 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∥ 𝑌) → 𝑌 ∈ 𝐵) | ||
Theorem | dvdsrid 20383 | 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 20384 | Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋) → 𝑌 ∥ 𝑋) | ||
Theorem | dvdsrmul1 20385 | The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∥ 𝑌) → (𝑋 · 𝑍) ∥ (𝑌 · 𝑍)) | ||
Theorem | dvdsrneg 20386 | An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ (𝑁‘𝑋)) | ||
Theorem | dvdsr01 20387 | In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 20710.) (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ 0 ) | ||
Theorem | dvdsr02 20388 | Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 ∥ 𝑋 ↔ 𝑋 = 0 )) | ||
Theorem | isunit 20389 | 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 20390 | The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 1 ∈ 𝑈) | ||
Theorem | unitcl 20391 | A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ 𝐵) | ||
Theorem | unitss 20392 | The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ 𝑈 ⊆ 𝐵 | ||
Theorem | opprunit 20393 | 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 20394 | Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∥ 1 )) | ||
Theorem | dvdsunit 20395 | A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ∧ 𝑋 ∈ 𝑈) → 𝑌 ∈ 𝑈) | ||
Theorem | unitmulcl 20396 | The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝑈) | ||
Theorem | unitmulclb 20397 | Reversal of unitmulcl 20396 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) ∈ 𝑈 ↔ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈))) | ||
Theorem | unitgrpbas 20398 | The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ 𝑈 = (Base‘𝐺) | ||
Theorem | unitgrp 20399 | The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) | ||
Theorem | unitabl 20400 | The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝑅 ∈ CRing → 𝐺 ∈ Abel) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |