Type | Label | Description |
Statement |
|
Theorem | ringidcl 13201 |
The unity element of a ring belongs to the base set of the ring.
(Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro,
27-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ 1 =
(1rβπ
) β β’ (π
β Ring β 1 β π΅) |
|
Theorem | ring0cl 13202 |
The zero element of a ring belongs to its base set. (Contributed by
Mario Carneiro, 12-Jan-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ 0 =
(0gβπ
) β β’ (π
β Ring β 0 β π΅) |
|
Theorem | ringidmlem 13203 |
Lemma for ringlidm 13204 and ringridm 13205. (Contributed by NM, 15-Sep-2011.)
(Revised by Mario Carneiro, 27-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ 1 =
(1rβπ
) β β’ ((π
β Ring β§ π β π΅) β (( 1 Β· π) = π β§ (π Β· 1 ) = π)) |
|
Theorem | ringlidm 13204 |
The unity element of a ring is a left multiplicative identity.
(Contributed by NM, 15-Sep-2011.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ 1 =
(1rβπ
) β β’ ((π
β Ring β§ π β π΅) β ( 1 Β· π) = π) |
|
Theorem | ringridm 13205 |
The unity element of a ring is a right multiplicative identity.
(Contributed by NM, 15-Sep-2011.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ 1 =
(1rβπ
) β β’ ((π
β Ring β§ π β π΅) β (π Β· 1 ) = π) |
|
Theorem | isringid 13206* |
Properties showing that an element πΌ is the unity element of a ring.
(Contributed by NM, 7-Aug-2013.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ 1 =
(1rβπ
) β β’ (π
β Ring β ((πΌ β π΅ β§ βπ₯ β π΅ ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯)) β 1 = πΌ)) |
|
Theorem | ringid 13207* |
The multiplication operation of a unital ring has (one or more) identity
elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by
Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
) β β’ ((π
β Ring β§ π β π΅) β βπ’ β π΅ ((π’ Β· π) = π β§ (π Β· π’) = π)) |
|
Theorem | ringadd2 13208* |
A ring element plus itself is two times the element. (Contributed by
Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.)
(Revised by AV, 24-Aug-2021.)
|
β’ π΅ = (Baseβπ
)
& β’ + =
(+gβπ
)
& β’ Β· =
(.rβπ
) β β’ ((π
β Ring β§ π β π΅) β βπ₯ β π΅ (π + π) = ((π₯ + π₯) Β· π)) |
|
Theorem | rngo2times 13209 |
A ring element plus itself is two times the element. "Two" in an
arbitrary unital ring is the sum of the unity element with itself.
(Contributed by AV, 24-Aug-2021.)
|
β’ π΅ = (Baseβπ
)
& β’ + =
(+gβπ
)
& β’ Β· =
(.rβπ
)
& β’ 1 =
(1rβπ
) β β’ ((π
β Ring β§ π΄ β π΅) β (π΄ + π΄) = (( 1 + 1 ) Β· π΄)) |
|
Theorem | ringidss 13210 |
A subset of the multiplicative group has the multiplicative identity as
its identity if the identity is in the subset. (Contributed by Mario
Carneiro, 27-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
β’ π = ((mulGrpβπ
) βΎs π΄)
& β’ π΅ = (Baseβπ
)
& β’ 1 =
(1rβπ
) β β’ ((π
β Ring β§ π΄ β π΅ β§ 1 β π΄) β 1 =
(0gβπ)) |
|
Theorem | ringacl 13211 |
Closure of the addition operation of a ring. (Contributed by Mario
Carneiro, 14-Jan-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ + =
(+gβπ
) β β’ ((π
β Ring β§ π β π΅ β§ π β π΅) β (π + π) β π΅) |
|
Theorem | ringcom 13212 |
Commutativity of the additive group of a ring. (Contributed by
GΓ©rard Lang, 4-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ + =
(+gβπ
) β β’ ((π
β Ring β§ π β π΅ β§ π β π΅) β (π + π) = (π + π)) |
|
Theorem | ringabl 13213 |
A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
|
β’ (π
β Ring β π
β Abel) |
|
Theorem | ringcmn 13214 |
A ring is a commutative monoid. (Contributed by Mario Carneiro,
7-Jan-2015.)
|
β’ (π
β Ring β π
β CMnd) |
|
Theorem | ringpropd 13215* |
If two structures have the same group components (properties), 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 13216* |
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 13217 |
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 13218* |
Properties that determine a ring. (Contributed by NM, 2-Aug-2013.)
|
β’ (π β π΅ = (Baseβπ
)) & β’ (π β + =
(+gβπ
)) & β’ (π β Β· =
(.rβπ
)) & β’ (π β π
β Grp) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ Β· π¦) β π΅)
& β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) & β’ (π β 1 β π΅)
& β’ ((π β§ π₯ β π΅) β ( 1 Β· π₯) = π₯)
& β’ ((π β§ π₯ β π΅) β (π₯ Β· 1 ) = π₯) β β’ (π β π
β Ring) |
|
Theorem | iscrngd 13219* |
Properties that determine a commutative ring. (Contributed by Mario
Carneiro, 7-Jan-2015.)
|
β’ (π β π΅ = (Baseβπ
)) & β’ (π β + =
(+gβπ
)) & β’ (π β Β· =
(.rβπ
)) & β’ (π β π
β Grp) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ Β· π¦) β π΅)
& β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) & β’ (π β 1 β π΅)
& β’ ((π β§ π₯ β π΅) β ( 1 Β· π₯) = π₯)
& β’ ((π β§ π₯ β π΅) β (π₯ Β· 1 ) = π₯)
& β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ Β· π¦) = (π¦ Β· π₯)) β β’ (π β π
β CRing) |
|
Theorem | ringlz 13220 |
The zero of a unital ring is a left-absorbing element. (Contributed by
FL, 31-Aug-2009.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ 0 =
(0gβπ
) β β’ ((π
β Ring β§ π β π΅) β ( 0 Β· π) = 0 ) |
|
Theorem | ringrz 13221 |
The zero of a unital ring is a right-absorbing element. (Contributed by
FL, 31-Aug-2009.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ 0 =
(0gβπ
) β β’ ((π
β Ring β§ π β π΅) β (π Β· 0 ) = 0 ) |
|
Theorem | ringsrg 13222 |
Any ring is also a semiring. (Contributed by Thierry Arnoux,
1-Apr-2018.)
|
β’ (π
β Ring β π
β SRing) |
|
Theorem | ring1eq0 13223 |
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 | ringinvnz1ne0 13224* |
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 13225* |
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 13226 |
Negation in a ring is the same as left multiplication by -1.
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ 1 =
(1rβπ
)
& β’ π = (invgβπ
)
& β’ (π β π
β Ring) & β’ (π β π β π΅) β β’ (π β ((πβ 1 ) Β· π) = (πβπ)) |
|
Theorem | rngnegr 13227 |
Negation in a ring is the same as right multiplication by -1.
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ 1 =
(1rβπ
)
& β’ π = (invgβπ
)
& β’ (π β π
β Ring) & β’ (π β π β π΅) β β’ (π β (π Β· (πβ 1 )) = (πβπ)) |
|
Theorem | ringmneg1 13228 |
Negation of a product in a ring. (mulneg1 8351 analog.) (Contributed by
Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ π = (invgβπ
)
& β’ (π β π
β Ring) & β’ (π β π β π΅)
& β’ (π β π β π΅) β β’ (π β ((πβπ) Β· π) = (πβ(π Β· π))) |
|
Theorem | ringmneg2 13229 |
Negation of a product in a ring. (mulneg2 8352 analog.) (Contributed by
Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ π = (invgβπ
)
& β’ (π β π
β Ring) & β’ (π β π β π΅)
& β’ (π β π β π΅) β β’ (π β (π Β· (πβπ)) = (πβ(π Β· π))) |
|
Theorem | ringm2neg 13230 |
Double negation of a product in a ring. (mul2neg 8354 analog.)
(Contributed by Mario Carneiro, 4-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ π = (invgβπ
)
& β’ (π β π
β Ring) & β’ (π β π β π΅)
& β’ (π β π β π΅) β β’ (π β ((πβπ) Β· (πβπ)) = (π Β· π)) |
|
Theorem | ringsubdi 13231 |
Ring multiplication distributes over subtraction. (subdi 8341 analog.)
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ β =
(-gβπ
)
& β’ (π β π
β Ring) & β’ (π β π β π΅)
& β’ (π β π β π΅)
& β’ (π β π β π΅) β β’ (π β (π Β· (π β π)) = ((π Β· π) β (π Β· π))) |
|
Theorem | rngsubdir 13232 |
Ring multiplication distributes over subtraction. (subdir 8342 analog.)
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ β =
(-gβπ
)
& β’ (π β π
β Ring) & β’ (π β π β π΅)
& β’ (π β π β π΅)
& β’ (π β π β π΅) β β’ (π β ((π β π) Β· π) = ((π Β· π) β (π Β· π))) |
|
Theorem | mulgass2 13233 |
An associative property between group multiple and ring multiplication.
(Contributed by Mario Carneiro, 14-Jun-2015.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.gβπ
)
& β’ Γ =
(.rβπ
) β β’ ((π
β Ring β§ (π β β€ β§ π β π΅ β§ π β π΅)) β ((π Β· π) Γ π) = (π Β· (π Γ π))) |
|
Theorem | ring1 13234 |
The (smallest) structure representing a zero ring. (Contributed by
AV, 28-Apr-2019.)
|
β’ π = {β¨(Baseβndx), {π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©,
β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©}
β β’ (π β π β π β Ring) |
|
Theorem | ringn0 13235 |
The class of rings is not empty (it is also inhabited, as shown at
ring1 13234). (Contributed by AV, 29-Apr-2019.)
|
β’ Ring β β
|
|
Theorem | ringressid 13236 |
A ring restricted to its base set is a ring. It will usually be the
original ring exactly, of course, but to show that needs additional
conditions such as those in strressid 12529. (Contributed by Jim Kingdon,
28-Feb-2025.)
|
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Ring β (πΊ βΎs π΅) β Ring) |
|
7.3.5 Opposite ring
|
|
Syntax | coppr 13237 |
The opposite ring operation.
|
class oppr |
|
Definition | df-oppr 13238 |
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 | opprvalg 13239 |
Value of the opposite ring. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ π = (opprβπ
)
β β’ (π
β π β π = (π
sSet β¨(.rβndx), tpos
Β·
β©)) |
|
Theorem | opprmulfvalg 13240 |
Value of the multiplication operation of an opposite ring. (Contributed
by Mario Carneiro, 1-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ π = (opprβπ
) & β’ β =
(.rβπ) β β’ (π
β π β β = tpos Β·
) |
|
Theorem | opprmulg 13241 |
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 13242 |
In a commutative ring, the opposite ring is equivalent to the original
ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ π = (opprβπ
) & β’ β =
(.rβπ) β β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β (π Β· π) = (π β π)) |
|
Theorem | opprex 13243 |
Existence of the opposite ring. If you know that π
is a ring, see
opprring 13247. (Contributed by Jim Kingdon, 10-Jan-2025.)
|
β’ π = (opprβπ
)
β β’ (π
β π β π β V) |
|
Theorem | opprsllem 13244 |
Lemma for opprbasg 13245 and oppraddg 13246. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
|
β’ π = (opprβπ
) & β’ (πΈ = Slot (πΈβndx) β§ (πΈβndx) β β) & β’ (πΈβndx) β
(.rβndx) β β’ (π
β π β (πΈβπ
) = (πΈβπ)) |
|
Theorem | opprbasg 13245 |
Base set of an opposite ring. (Contributed by Mario Carneiro,
1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
β’ π = (opprβπ
) & β’ π΅ = (Baseβπ
)
β β’ (π
β π β π΅ = (Baseβπ)) |
|
Theorem | oppraddg 13246 |
Addition operation of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
β’ π = (opprβπ
) & β’ + =
(+gβπ
) β β’ (π
β π β + =
(+gβπ)) |
|
Theorem | opprring 13247 |
An opposite ring is a ring. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
β’ π = (opprβπ
)
β β’ (π
β Ring β π β Ring) |
|
Theorem | opprringbg 13248 |
Bidirectional form of opprring 13247. (Contributed by Mario Carneiro,
6-Dec-2014.)
|
β’ π = (opprβπ
)
β β’ (π
β π β (π
β Ring β π β Ring)) |
|
Theorem | oppr0g 13249 |
Additive identity of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.)
|
β’ π = (opprβπ
) & β’ 0 =
(0gβπ
) β β’ (π
β π β 0 =
(0gβπ)) |
|
Theorem | oppr1g 13250 |
Multiplicative identity of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.)
|
β’ π = (opprβπ
) & β’ 1 =
(1rβπ
) β β’ (π
β π β 1 =
(1rβπ)) |
|
Theorem | opprnegg 13251 |
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 | mulgass3 13252 |
An associative property between group multiple and ring multiplication.
(Contributed by Mario Carneiro, 14-Jun-2015.)
|
β’ π΅ = (Baseβπ
)
& β’ Β· =
(.gβπ
)
& β’ Γ =
(.rβπ
) β β’ ((π
β Ring β§ (π β β€ β§ π β π΅ β§ π β π΅)) β (π Γ (π Β· π)) = (π Β· (π Γ π))) |
|
7.3.6 Divisibility
|
|
Syntax | cdsr 13253 |
Ring divisibility relation.
|
class β₯r |
|
Syntax | cui 13254 |
Units in a ring.
|
class Unit |
|
Syntax | cir 13255 |
Ring irreducibles.
|
class Irred |
|
Definition | df-dvdsr 13256* |
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 13257 |
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 13258* |
Define the set of irreducible elements in a ring. (Contributed by Mario
Carneiro, 4-Dec-2014.)
|
β’ Irred = (π€ β V β¦
β¦((Baseβπ€) β (Unitβπ€)) / πβ¦{π§ β π β£ βπ₯ β π βπ¦ β π (π₯(.rβπ€)π¦) β π§}) |
|
Theorem | reldvdsrsrg 13259 |
The divides relation is a relation. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.)
|
β’ (π
β SRing β Rel
(β₯rβπ
)) |
|
Theorem | dvdsrvald 13260* |
Value of the divides relation. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
|
β’ (π β π΅ = (Baseβπ
)) & β’ (π β β₯ =
(β₯rβπ
)) & β’ (π β π
β SRing) & β’ (π β Β· =
(.rβπ
)) β β’ (π β β₯ = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ βπ§ β π΅ (π§ Β· π₯) = π¦)}) |
|
Theorem | dvdsrd 13261* |
Value of the divides relation. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
β’ (π β π΅ = (Baseβπ
)) & β’ (π β β₯ =
(β₯rβπ
)) & β’ (π β π
β SRing) & β’ (π β Β· =
(.rβπ
)) β β’ (π β (π β₯ π β (π β π΅ β§ βπ§ β π΅ (π§ Β· π) = π))) |
|
Theorem | dvdsr2d 13262* |
Value of the divides relation. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
β’ (π β π΅ = (Baseβπ
)) & β’ (π β β₯ =
(β₯rβπ
)) & β’ (π β π
β SRing) & β’ (π β Β· =
(.rβπ
)) & β’ (π β π β π΅) β β’ (π β (π β₯ π β βπ§ β π΅ (π§ Β· π) = π)) |
|
Theorem | dvdsrmuld 13263 |
A left-multiple of π is divisible by π.
(Contributed by
Mario Carneiro, 1-Dec-2014.)
|
β’ (π β π΅ = (Baseβπ
)) & β’ (π β β₯ =
(β₯rβπ
)) & β’ (π β π
β SRing) & β’ (π β Β· =
(.rβπ
)) & β’ (π β π β π΅)
& β’ (π β π β π΅) β β’ (π β π β₯ (π Β· π)) |
|
Theorem | dvdsrcld 13264 |
Closure of a dividing element. (Contributed by Mario Carneiro,
5-Dec-2014.)
|
β’ (π β π΅ = (Baseβπ
)) & β’ (π β β₯ =
(β₯rβπ
)) & β’ (π β π
β SRing) & β’ (π β π β₯ π) β β’ (π β π β π΅) |
|
Theorem | dvdsrex 13265 |
Existence of the divisibility relation. (Contributed by Jim Kingdon,
28-Jan-2025.)
|
β’ (π
β SRing β
(β₯rβπ
) β V) |
|
Theorem | dvdsrcl2 13266 |
Closure of a dividing element. (Contributed by Mario Carneiro,
5-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ β₯ =
(β₯rβπ
) β β’ ((π
β Ring β§ π β₯ π) β π β π΅) |
|
Theorem | dvdsrid 13267 |
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 13268 |
Divisibility is transitive. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ β₯ =
(β₯rβπ
) β β’ ((π
β Ring β§ π β₯ π β§ π β₯ π) β π β₯ π) |
|
Theorem | dvdsrmul1 13269 |
The divisibility relation is preserved under right-multiplication.
(Contributed by Mario Carneiro, 1-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ β₯ =
(β₯rβπ
)
& β’ Β· =
(.rβπ
) β β’ ((π
β Ring β§ π β π΅ β§ π β₯ π) β (π Β· π) β₯ (π Β· π)) |
|
Theorem | dvdsrneg 13270 |
An element divides its negative. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
β’ π΅ = (Baseβπ
)
& β’ β₯ =
(β₯rβπ
)
& β’ π = (invgβπ
) β β’ ((π
β Ring β§ π β π΅) β π β₯ (πβπ)) |
|
Theorem | dvdsr01 13271 |
In a ring, zero is divisible by all elements. ("Zero divisor" as a
term
has a somewhat different meaning.) (Contributed by Stefan O'Rear,
29-Mar-2015.)
|
β’ π΅ = (Baseβπ
)
& β’ β₯ =
(β₯rβπ
)
& β’ 0 =
(0gβπ
) β β’ ((π
β Ring β§ π β π΅) β π β₯ 0 ) |
|
Theorem | dvdsr02 13272 |
Only zero is divisible by zero. (Contributed by Stefan O'Rear,
29-Mar-2015.)
|
β’ π΅ = (Baseβπ
)
& β’ β₯ =
(β₯rβπ
)
& β’ 0 =
(0gβπ
) β β’ ((π
β Ring β§ π β π΅) β ( 0 β₯ π β π = 0 )) |
|
Theorem | isunitd 13273 |
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βπ)) & β’ (π β π
β SRing)
β β’ (π β (π β π β (π β₯ 1 β§ ππΈ 1 ))) |
|
Theorem | 1unit 13274 |
The multiplicative identity is a unit. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
β’ π = (Unitβπ
)
& β’ 1 =
(1rβπ
) β β’ (π
β Ring β 1 β π) |
|
Theorem | unitcld 13275 |
A unit is an element of the base set. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
β’ (π β π΅ = (Baseβπ
)) & β’ (π β π = (Unitβπ
)) & β’ (π β π
β SRing) & β’ (π β π β π) β β’ (π β π β π΅) |
|
Theorem | unitssd 13276 |
The set of units is contained in the base set. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
β’ (π β π΅ = (Baseβπ
)) & β’ (π β π = (Unitβπ
)) & β’ (π β π
β SRing)
β β’ (π β π β π΅) |
|
Theorem | opprunitd 13277 |
Being a unit is a symmetric property, so it transfers to the opposite
ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|
β’ (π β π = (Unitβπ
)) & β’ (π β π = (opprβπ
)) & β’ (π β π
β Ring)
β β’ (π β π = (Unitβπ)) |
|
Theorem | crngunit 13278 |
Property of being a unit in a commutative ring. (Contributed by Mario
Carneiro, 18-Apr-2016.)
|
β’ π = (Unitβπ
)
& β’ 1 =
(1rβπ
)
& β’ β₯ =
(β₯rβπ
) β β’ (π
β CRing β (π β π β π β₯ 1 )) |
|
Theorem | dvdsunit 13279 |
A divisor of a unit is a unit. (Contributed by Mario Carneiro,
18-Apr-2016.)
|
β’ π = (Unitβπ
)
& β’ β₯ =
(β₯rβπ
) β β’ ((π
β CRing β§ π β₯ π β§ π β π) β π β π) |
|
Theorem | unitmulcl 13280 |
The product of units is a unit. (Contributed by Mario Carneiro,
2-Dec-2014.)
|
β’ π = (Unitβπ
)
& β’ Β· =
(.rβπ
) β β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π) β π) |
|
Theorem | unitmulclb 13281 |
Reversal of unitmulcl 13280 in a commutative ring. (Contributed by
Mario
Carneiro, 18-Apr-2016.)
|
β’ π = (Unitβπ
)
& β’ Β· =
(.rβπ
)
& β’ π΅ = (Baseβπ
) β β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β ((π Β· π) β π β (π β π β§ π β π))) |
|
Theorem | unitgrpbasd 13282 |
The base set of the group of units. (Contributed by Mario Carneiro,
25-Dec-2014.)
|
β’ (π β π = (Unitβπ
)) & β’ (π β πΊ = ((mulGrpβπ
) βΎs π)) & β’ (π β π
β SRing)
β β’ (π β π = (BaseβπΊ)) |
|
Theorem | unitgrp 13283 |
The group of units is a group under multiplication. (Contributed by
Mario Carneiro, 2-Dec-2014.)
|
β’ π = (Unitβπ
)
& β’ πΊ = ((mulGrpβπ
) βΎs π) β β’ (π
β Ring β πΊ β Grp) |
|
Theorem | unitabl 13284 |
The group of units of a commutative ring is abelian. (Contributed by
Mario Carneiro, 19-Apr-2016.)
|
β’ π = (Unitβπ
)
& β’ πΊ = ((mulGrpβπ
) βΎs π) β β’ (π
β CRing β πΊ β Abel) |
|
Theorem | unitgrpid 13285 |
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 13286 |
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 13287 |
Extend class notation with multiplicative inverse.
|
class invr |
|
Definition | df-invr 13288 |
Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
|
β’ invr = (π β V β¦
(invgβ((mulGrpβπ) βΎs (Unitβπ)))) |
|
Theorem | invrfvald 13289 |
Multiplicative inverse function for a ring. (Contributed by NM,
21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
|
β’ (π β π = (Unitβπ
)) & β’ (π β πΊ = ((mulGrpβπ
) βΎs π)) & β’ (π β πΌ = (invrβπ
)) & β’ (π β π
β Ring)
β β’ (π β πΌ = (invgβπΊ)) |
|
Theorem | unitinvcl 13290 |
The inverse of a unit exists and is a unit. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
β’ π = (Unitβπ
)
& β’ πΌ = (invrβπ
) β β’ ((π
β Ring β§ π β π) β (πΌβπ) β π) |
|
Theorem | unitinvinv 13291 |
The inverse of the inverse of a unit is the same element. (Contributed
by Mario Carneiro, 4-Dec-2014.)
|
β’ π = (Unitβπ
)
& β’ πΌ = (invrβπ
) β β’ ((π
β Ring β§ π β π) β (πΌβ(πΌβπ)) = π) |
|
Theorem | ringinvcl 13292 |
The inverse of a unit is an element of the ring. (Contributed by
Mario Carneiro, 2-Dec-2014.)
|
β’ π = (Unitβπ
)
& β’ πΌ = (invrβπ
)
& β’ π΅ = (Baseβπ
) β β’ ((π
β Ring β§ π β π) β (πΌβπ) β π΅) |
|
Theorem | unitlinv 13293 |
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 13294 |
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 13295 |
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 13296 |
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 13297 |
The negative of a unit is a unit. (Contributed by Mario Carneiro,
4-Dec-2014.)
|
β’ π = (Unitβπ
)
& β’ π = (invgβπ
) β β’ ((π
β Ring β§ π β π) β (πβπ) β π) |
|
Syntax | cdvr 13298 |
Extend class notation with ring division.
|
class /r |
|
Definition | df-dvr 13299* |
Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|
β’ /r = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Unitβπ) β¦ (π₯(.rβπ)((invrβπ)βπ¦)))) |
|
Theorem | dvrfvald 13300* |
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βπ
)) & β’ (π β π
β SRing)
β β’ (π β / = (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦)))) |