![]() |
Metamath
Proof Explorer Theorem List (p. 203 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ringrghm 20201* | 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 20202* | Obsolete version of gsummulc1 20204 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 20203* | Obsolete version of gsummulc2 20205 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 20204* | 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 20205* | 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 20206* | 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 20207* | 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 20208 | 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 20209 | A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆRing) β β’ (π β π β Ring) | ||
Theorem | prdscrngd 20210 | 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 20211 | Value of the ring unity in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆRing) β β’ (π β (1r β π ) = (1rβπ)) | ||
Theorem | pwsring 20212 | A structure power of a ring is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (π βs πΌ) β β’ ((π β Ring β§ πΌ β π) β π β Ring) | ||
Theorem | pws1 20213 | Value of the ring unity in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (π βs πΌ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ πΌ β π) β (πΌ Γ { 1 }) = (1rβπ)) | ||
Theorem | pwscrng 20214 | A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (π βs πΌ) β β’ ((π β CRing β§ πΌ β π) β π β CRing) | ||
Theorem | pwsmgp 20215 | 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 20216* | The projection given by pwspjmhm 18747 is also a monoid homomorphism between the respective multiplicative groups. (Contributed by SN, 30-Jul-2024.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (mulGrpβπ) & β’ π = (mulGrpβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π΄ β πΌ) β β’ (π β (π₯ β π΅ β¦ (π₯βπ΄)) β (π MndHom π)) | ||
Theorem | pwsexpg 20217 | Value of a group exponentiation in a structure power. Compare pwsmulg 19035. (Contributed by SN, 30-Jul-2024.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (mulGrpβπ) & β’ π = (mulGrpβπ ) & β’ β = (.gβπ) & β’ Β· = (.gβπ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β π΄ β πΌ) β β’ (π β ((π β π)βπ΄) = (π Β· (πβπ΄))) | ||
Theorem | imasring 20218* | 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 20219 | The image of a ring under an injection is a ring (imasmndf1 18698 analog). (Contributed by AV, 27-Feb-2025.) |
β’ π = (πΉ βs π ) & β’ π = (Baseβπ ) β β’ ((πΉ:πβ1-1βπ΅ β§ π β Ring) β π β Ring) | ||
Theorem | xpsringd 20220 | A product of two rings is a ring (xpsmnd 18699 analog). (Contributed by AV, 28-Feb-2025.) |
β’ π = (π Γs π ) & β’ (π β π β Ring) & β’ (π β π β Ring) β β’ (π β π β Ring) | ||
Theorem | xpsring1d 20221 | The multiplicative identity element of a binary product of rings. (Contributed by AV, 16-Mar-2025.) |
β’ π = (π Γs π ) & β’ (π β π β Ring) & β’ (π β π β Ring) β β’ (π β (1rβπ) = β¨(1rβπ), (1rβπ )β©) | ||
Theorem | qusring2 20222* | 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 20223* | The binomial theorem for commutative rings (special case of csrgbinom 20126): (π΄ + π΅)βπ 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 20224 | The opposite ring operation. |
class oppr | ||
Definition | df-oppr 20225 | 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 20226 | Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (opprβπ ) β β’ π = (π sSet β¨(.rβndx), tpos Β· β©) | ||
Theorem | opprmulfval 20227 | Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (opprβπ ) & β’ β = (.rβπ) β β’ β = tpos Β· | ||
Theorem | opprmul 20228 | 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 20229 | In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 20308). (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (opprβπ ) & β’ β = (.rβπ) β β’ ((π β CRing β§ π β π΅ β§ π β π΅) β (π Β· π) = (π β π)) | ||
Theorem | opprlem 20230 | Lemma for opprbas 20232 and oppradd 20234. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.) |
β’ π = (opprβπ ) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (.rβndx) β β’ (πΈβπ ) = (πΈβπ) | ||
Theorem | opprlemOLD 20231 | Obsolete version of opprlem 20230 as of 6-Nov-2024. Lemma for opprbas 20232 and oppradd 20234. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (opprβπ ) & β’ πΈ = Slot π & β’ π β β & β’ π < 3 β β’ (πΈβπ ) = (πΈβπ) | ||
Theorem | opprbas 20232 | 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 20233 | Obsolete proof of opprbas 20232 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 20234 | 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 20235 | Obsolete proof of opprbas 20232 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 20236 | An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.) |
β’ π = (opprβπ ) β β’ (π β Rng β π β Rng) | ||
Theorem | opprrngb 20237 | A class is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 20236. (Contributed by AV, 15-Feb-2025.) |
β’ π = (opprβπ ) β β’ (π β Rng β π β Rng) | ||
Theorem | opprring 20238 | 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 20239 | Bidirectional form of opprring 20238. (Contributed by Mario Carneiro, 6-Dec-2014.) |
β’ π = (opprβπ ) β β’ (π β Ring β π β Ring) | ||
Theorem | oppr0 20240 | Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π = (opprβπ ) & β’ 0 = (0gβπ ) β β’ 0 = (0gβπ) | ||
Theorem | oppr1 20241 | Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π = (opprβπ ) & β’ 1 = (1rβπ ) β β’ 1 = (1rβπ) | ||
Theorem | opprneg 20242 | 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 20243 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
β’ π = (opprβπ ) β β’ (SubGrpβπ ) = (SubGrpβπ) | ||
Theorem | mulgass3 20244 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.gβπ ) & β’ Γ = (.rβπ ) β β’ ((π β Ring β§ (π β β€ β§ π β π΅ β§ π β π΅)) β (π Γ (π Β· π)) = (π Β· (π Γ π))) | ||
Syntax | cdsr 20245 | Ring divisibility relation. |
class β₯r | ||
Syntax | cui 20246 | Units in a ring. |
class Unit | ||
Syntax | cir 20247 | Ring irreducibles. |
class Irred | ||
Definition | df-dvdsr 20248* | 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 20249 | 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 20250* | Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ Irred = (π€ β V β¦ β¦((Baseβπ€) β (Unitβπ€)) / πβ¦{π§ β π β£ βπ₯ β π βπ¦ β π (π₯(.rβπ€)π¦) β π§}) | ||
Theorem | reldvdsr 20251 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ β₯ = (β₯rβπ ) β β’ Rel β₯ | ||
Theorem | dvdsrval 20252* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ β₯ = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ βπ§ β π΅ (π§ Β· π₯) = π¦)} | ||
Theorem | dvdsr 20253* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ (π β₯ π β (π β π΅ β§ βπ§ β π΅ (π§ Β· π) = π)) | ||
Theorem | dvdsr2 20254* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ (π β π΅ β (π β₯ π β βπ§ β π΅ (π§ Β· π) = π)) | ||
Theorem | dvdsrmul 20255 | A left-multiple of π is divisible by π. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β π΅ β§ π β π΅) β π β₯ (π Β· π)) | ||
Theorem | dvdsrcl 20256 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) β β’ (π β₯ π β π β π΅) | ||
Theorem | dvdsrcl2 20257 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β Ring β§ π β₯ π) β π β π΅) | ||
Theorem | dvdsrid 20258 | 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 20259 | Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β Ring β§ π β₯ π β§ π β₯ π) β π β₯ π) | ||
Theorem | dvdsrmul1 20260 | The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β₯ π) β (π Β· π) β₯ (π Β· π)) | ||
Theorem | dvdsrneg 20261 | An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ π β π΅) β π β₯ (πβπ)) | ||
Theorem | dvdsr01 20262 | In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 21099.) (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β π β₯ 0 ) | ||
Theorem | dvdsr02 20263 | Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β ( 0 β₯ π β π = 0 )) | ||
Theorem | isunit 20264 | 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 20265 | The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π = (Unitβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β 1 β π) | ||
Theorem | unitcl 20266 | A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) β β’ (π β π β π β π΅) | ||
Theorem | unitss 20267 | The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) β β’ π β π΅ | ||
Theorem | opprunit 20268 | 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 20269 | Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ π = (Unitβπ ) & β’ 1 = (1rβπ ) & β’ β₯ = (β₯rβπ ) β β’ (π β CRing β (π β π β π β₯ 1 )) | ||
Theorem | dvdsunit 20270 | A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ π = (Unitβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β CRing β§ π β₯ π β§ π β π) β π β π) | ||
Theorem | unitmulcl 20271 | The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π β§ π β π) β (π Β· π) β π) | ||
Theorem | unitmulclb 20272 | Reversal of unitmulcl 20271 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β CRing β§ π β π΅ β§ π β π΅) β ((π Β· π) β π β (π β π β§ π β π))) | ||
Theorem | unitgrpbas 20273 | The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs π) β β’ π = (BaseβπΊ) | ||
Theorem | unitgrp 20274 | The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs π) β β’ (π β Ring β πΊ β Grp) | ||
Theorem | unitabl 20275 | The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (Unitβπ ) & β’ πΊ = ((mulGrpβπ ) βΎs π) β β’ (π β CRing β πΊ β Abel) | ||
Theorem | unitgrpid 20276 | 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 20277 | 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 20278 | Extend class notation with multiplicative inverse. |
class invr | ||
Definition | df-invr 20279 | Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.) |
β’ invr = (π β V β¦ (invgβ((mulGrpβπ) βΎs (Unitβπ)))) | ||
Theorem | invrfval 20280 | 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 20281 | The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β Ring β§ π β π) β (πΌβπ) β π) | ||
Theorem | unitinvinv 20282 | The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β Ring β§ π β π) β (πΌβ(πΌβπ)) = π) | ||
Theorem | ringinvcl 20283 | The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β π) β (πΌβπ) β π΅) | ||
Theorem | unitlinv 20284 | 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 20285 | 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 20286 | 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 20287 | 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 20288 | The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π = (Unitβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ π β π) β (πβπ) β π) | ||
Theorem | ringunitnzdiv 20289 | 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 20290 | 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 20291 | Extend class notation with ring division. |
class /r | ||
Definition | df-dvr 20292* | Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ /r = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Unitβπ) β¦ (π₯(.rβπ)((invrβπ)βπ¦)))) | ||
Theorem | dvrfval 20293* | 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 20294 | 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 20295 | Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β (π / π) β π΅) | ||
Theorem | unitdvcl 20296 | The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.) |
β’ π = (Unitβπ ) & β’ / = (/rβπ ) β β’ ((π β Ring β§ π β π β§ π β π) β (π / π) β π) | ||
Theorem | dvrid 20297 | A ring element divided by itself is the ring unity. (divid 11905 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π) β (π / π) = 1 ) | ||
Theorem | dvr1 20298 | A ring element divided by the ring unity is itself. (div1 11907 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ / = (/rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅) β (π / 1 ) = π) | ||
Theorem | dvrass 20299 | An associative law for division. (divass 11894 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π Β· π) / π) = (π Β· (π / π))) | ||
Theorem | dvrcan1 20300 | A cancellation law for division. (divcan1 11885 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((π / π) Β· π) = π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |