Type | Label | Description |
Statement |
|
Theorem | lspsnel 13701* |
Member of span of the singleton of a vector. (Contributed by NM,
22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ π = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β (πβ{π}) β βπ β πΎ π = (π Β· π))) |
|
Theorem | lspsnvsi 13702 |
Span of a scalar product of a singleton. (Contributed by NM,
23-Apr-2014.) (Proof shortened by Mario Carneiro, 4-Sep-2014.)
|
β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ π = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π
β πΎ β§ π β π) β (πβ{(π
Β· π)}) β (πβ{π})) |
|
Theorem | lspsnss2 13703* |
Comparable spans of singletons must have proportional vectors.
(Contributed by NM, 7-Jun-2015.)
|
β’ π = (Baseβπ)
& β’ π = (Scalarβπ)
& β’ πΎ = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β ((πβ{π}) β (πβ{π}) β βπ β πΎ π = (π Β· π))) |
|
Theorem | lspsnneg 13704 |
Negation does not change the span of a singleton. (Contributed by NM,
24-Apr-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (invgβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{(πβπ)}) = (πβ{π})) |
|
Theorem | lspsnsub 13705 |
Swapping subtraction order does not change the span of a singleton.
(Contributed by NM, 4-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ β =
(-gβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (πβ{(π β π)}) = (πβ{(π β π)})) |
|
Theorem | lspsn0 13706 |
Span of the singleton of the zero vector. (Contributed by NM,
15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|
β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ) β β’ (π β LMod β (πβ{ 0 }) = { 0 }) |
|
Theorem | lsp0 13707 |
Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.)
|
β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ) β β’ (π β LMod β (πββ
) = { 0 }) |
|
Theorem | lspuni0 13708 |
Union of the span of the empty set. (Contributed by NM,
14-Mar-2015.)
|
β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ) β β’ (π β LMod β βͺ (πββ
) = 0 ) |
|
Theorem | lspun0 13709 |
The span of a union with the zero subspace. (Contributed by NM,
22-May-2015.)
|
β’ π = (Baseβπ)
& β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β (πβ(π βͺ { 0 })) = (πβπ)) |
|
Theorem | lspsneq0 13710 |
Span of the singleton is the zero subspace iff the vector is zero.
(Contributed by NM, 27-Apr-2014.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β ((πβ{π}) = { 0 } β π = 0 )) |
|
Theorem | lspsneq0b 13711 |
Equal singleton spans imply both arguments are zero or both are nonzero.
(Contributed by NM, 21-Mar-2015.)
|
β’ π = (Baseβπ)
& β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π)
& β’ (π β (πβ{π}) = (πβ{π})) β β’ (π β (π = 0 β π = 0 )) |
|
Theorem | lmodindp1 13712 |
Two independent (non-colinear) vectors have nonzero sum. (Contributed
by NM, 22-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π)
& β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π + π) β 0 ) |
|
Theorem | lsslsp 13713 |
Spans in submodules correspond to spans in the containing module.
(Contributed by Stefan O'Rear, 12-Dec-2014.) Terms in the equation were
swapped as proposed by NM on 15-Mar-2015. (Revised by AV,
18-Apr-2025.)
|
β’ π = (π βΎs π)
& β’ π = (LSpanβπ)
& β’ π = (LSpanβπ)
& β’ πΏ = (LSubSpβπ) β β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) = (πβπΊ)) |
|
Theorem | lss0v 13714 |
The zero vector in a submodule equals the zero vector in the including
module. (Contributed by NM, 15-Mar-2015.)
|
β’ π = (π βΎs π)
& β’ 0 =
(0gβπ)
& β’ π = (0gβπ)
& β’ πΏ = (LSubSpβπ) β β’ ((π β LMod β§ π β πΏ) β π = 0 ) |
|
Theorem | lsspropdg 13715* |
If two structures have the same components (properties), they have the
same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015.)
(Revised by Mario Carneiro, 14-Jun-2015.)
|
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β π)
& β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦))
& β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) β π)
& β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπΏ)π¦)) & β’ (π β π = (Baseβ(ScalarβπΎ))) & β’ (π β π = (Baseβ(ScalarβπΏ))) & β’ (π β πΎ β π)
& β’ (π β πΏ β π) β β’ (π β (LSubSpβπΎ) = (LSubSpβπΏ)) |
|
Theorem | lsppropd 13716* |
If two structures have the same components (properties), they have the
same span function. (Contributed by Mario Carneiro, 9-Feb-2015.)
(Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV,
24-Apr-2024.)
|
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β π)
& β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦))
& β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) β π)
& β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπΏ)π¦)) & β’ (π β π = (Baseβ(ScalarβπΎ))) & β’ (π β π = (Baseβ(ScalarβπΏ))) & β’ (π β πΎ β π)
& β’ (π β πΏ β π) β β’ (π β (LSpanβπΎ) = (LSpanβπΏ)) |
|
7.6 Subring algebras and
ideals
|
|
7.6.1 Subring algebras
|
|
Syntax | csra 13717 |
Extend class notation with the subring algebra generator.
|
class subringAlg |
|
Syntax | crglmod 13718 |
Extend class notation with the left module induced by a ring over
itself.
|
class ringLMod |
|
Definition | df-sra 13719* |
Any ring can be regarded as a left algebra over any of its subrings.
The function subringAlg associates with any ring
and any of its
subrings the left algebra consisting in the ring itself regarded as a
left algebra over the subring. It has an inner product which is simply
the ring product. (Contributed by Mario Carneiro, 27-Nov-2014.)
(Revised by Thierry Arnoux, 16-Jun-2019.)
|
β’ subringAlg = (π€ β V β¦ (π β π« (Baseβπ€) β¦ (((π€ sSet β¨(Scalarβndx), (π€ βΎs π )β©) sSet β¨(
Β·π βndx), (.rβπ€)β©) sSet
β¨(Β·πβndx),
(.rβπ€)β©))) |
|
Definition | df-rgmod 13720 |
Any ring can be regarded as a left algebra over itself. The function
ringLMod associates with any ring the left
algebra consisting in the
ring itself regarded as a left algebra over itself. It has an inner
product which is simply the ring product. (Contributed by Stefan
O'Rear, 6-Dec-2014.)
|
β’ ringLMod = (π€ β V β¦ ((subringAlg βπ€)β(Baseβπ€))) |
|
Theorem | sraval 13721 |
Lemma for srabaseg 13723 through sravscag 13727. (Contributed by Mario
Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|
β’ ((π β π β§ π β (Baseβπ)) β ((subringAlg βπ)βπ) = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
|
Theorem | sralemg 13722 |
Lemma for srabaseg 13723 and similar theorems. (Contributed by Mario
Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
(Revised by AV, 29-Oct-2024.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π)
& β’ (πΈ = Slot (πΈβndx) β§ (πΈβndx) β β) & β’
(Scalarβndx) β (πΈβndx) & β’ (
Β·π βndx) β (πΈβndx) & β’
(Β·πβndx) β (πΈβndx) β β’ (π β (πΈβπ) = (πΈβπ΄)) |
|
Theorem | srabaseg 13723 |
Base set of a subring algebra. (Contributed by Stefan O'Rear,
27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by
Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (Baseβπ) = (Baseβπ΄)) |
|
Theorem | sraaddgg 13724 |
Additive operation of a subring algebra. (Contributed by Stefan O'Rear,
27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by
Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (+gβπ) = (+gβπ΄)) |
|
Theorem | sramulrg 13725 |
Multiplicative operation of a subring algebra. (Contributed by Stefan
O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.)
(Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV,
29-Oct-2024.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (.rβπ) = (.rβπ΄)) |
|
Theorem | srascag 13726 |
The set of scalars of a subring algebra. (Contributed by Stefan O'Rear,
27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by
Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (π βΎs π) = (Scalarβπ΄)) |
|
Theorem | sravscag 13727 |
The scalar product operation of a subring algebra. (Contributed by
Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.)
(Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV,
12-Nov-2024.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (.rβπ) = (
Β·π βπ΄)) |
|
Theorem | sraipg 13728 |
The inner product operation of a subring algebra. (Contributed by
Thierry Arnoux, 16-Jun-2019.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (.rβπ) =
(Β·πβπ΄)) |
|
Theorem | sratsetg 13729 |
Topology component of a subring algebra. (Contributed by Mario
Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
(Revised by AV, 29-Oct-2024.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (TopSetβπ) = (TopSetβπ΄)) |
|
Theorem | sraex 13730 |
Existence of a subring algebra. (Contributed by Jim Kingdon,
16-Apr-2025.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β π΄ β V) |
|
Theorem | sratopng 13731 |
Topology component of a subring algebra. (Contributed by Mario
Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (TopOpenβπ) = (TopOpenβπ΄)) |
|
Theorem | sradsg 13732 |
Distance function of a subring algebra. (Contributed by Mario Carneiro,
4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV,
29-Oct-2024.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (distβπ) = (distβπ΄)) |
|
Theorem | sraring 13733 |
Condition for a subring algebra to be a ring. (Contributed by Thierry
Arnoux, 24-Jul-2023.)
|
β’ π΄ = ((subringAlg βπ
)βπ)
& β’ π΅ = (Baseβπ
) β β’ ((π
β Ring β§ π β π΅) β π΄ β Ring) |
|
Theorem | sralmod 13734 |
The subring algebra is a left module. (Contributed by Stefan O'Rear,
27-Nov-2014.)
|
β’ π΄ = ((subringAlg βπ)βπ) β β’ (π β (SubRingβπ) β π΄ β LMod) |
|
Theorem | sralmod0g 13735 |
The subring module inherits a zero from its ring. (Contributed by
Stefan O'Rear, 27-Dec-2014.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β 0 =
(0gβπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β 0 =
(0gβπ΄)) |
|
Theorem | issubrgd 13736* |
Prove a subring by closure (definition version). (Contributed by Stefan
O'Rear, 7-Dec-2014.)
|
β’ (π β π = (πΌ βΎs π·)) & β’ (π β 0 =
(0gβπΌ)) & β’ (π β + =
(+gβπΌ)) & β’ (π β π· β (BaseβπΌ)) & β’ (π β 0 β π·)
& β’ ((π β§ π₯ β π· β§ π¦ β π·) β (π₯ + π¦) β π·)
& β’ ((π β§ π₯ β π·) β ((invgβπΌ)βπ₯) β π·)
& β’ (π β 1 =
(1rβπΌ)) & β’ (π β Β· =
(.rβπΌ)) & β’ (π β 1 β π·)
& β’ ((π β§ π₯ β π· β§ π¦ β π·) β (π₯ Β· π¦) β π·)
& β’ (π β πΌ β Ring)
β β’ (π β π· β (SubRingβπΌ)) |
|
Theorem | rlmfn 13737 |
ringLMod is a function. (Contributed by Stefan O'Rear,
6-Dec-2014.)
|
β’ ringLMod Fn V |
|
Theorem | rlmvalg 13738 |
Value of the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π β π β (ringLModβπ) = ((subringAlg βπ)β(Baseβπ))) |
|
Theorem | rlmbasg 13739 |
Base set of the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π
β π β (Baseβπ
) = (Baseβ(ringLModβπ
))) |
|
Theorem | rlmplusgg 13740 |
Vector addition in the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π
β π β (+gβπ
) =
(+gβ(ringLModβπ
))) |
|
Theorem | rlm0g 13741 |
Zero vector in the ring module. (Contributed by Stefan O'Rear,
6-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|
β’ (π
β π β (0gβπ
) =
(0gβ(ringLModβπ
))) |
|
Theorem | rlmsubg 13742 |
Subtraction in the ring module. (Contributed by Thierry Arnoux,
30-Jun-2019.)
|
β’ (π
β π β (-gβπ
) =
(-gβ(ringLModβπ
))) |
|
Theorem | rlmmulrg 13743 |
Ring multiplication in the ring module. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
β’ (π
β π β (.rβπ
) =
(.rβ(ringLModβπ
))) |
|
Theorem | rlmscabas 13744 |
Scalars in the ring module have the same base set. (Contributed by Jim
Kingdon, 29-Apr-2025.)
|
β’ (π
β π β (Baseβπ
) =
(Baseβ(Scalarβ(ringLModβπ
)))) |
|
Theorem | rlmvscag 13745 |
Scalar multiplication in the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π
β π β (.rβπ
) = (
Β·π β(ringLModβπ
))) |
|
Theorem | rlmtopng 13746 |
Topology component of the ring module. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
β’ (π
β π β (TopOpenβπ
) = (TopOpenβ(ringLModβπ
))) |
|
Theorem | rlmdsg 13747 |
Metric component of the ring module. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
β’ (π
β π β (distβπ
) = (distβ(ringLModβπ
))) |
|
Theorem | rlmlmod 13748 |
The ring module is a module. (Contributed by Stefan O'Rear,
6-Dec-2014.)
|
β’ (π
β Ring β (ringLModβπ
) β LMod) |
|
Theorem | rlmvnegg 13749 |
Vector negation in the ring module. (Contributed by Stefan O'Rear,
6-Dec-2014.) (Revised by Mario Carneiro, 5-Jun-2015.)
|
β’ (π
β π β (invgβπ
) =
(invgβ(ringLModβπ
))) |
|
Theorem | ixpsnbasval 13750* |
The value of an infinite Cartesian product of the base of a left module
over a ring with a singleton. (Contributed by AV, 3-Dec-2018.)
|
β’ ((π
β π β§ π β π) β Xπ₯ β {π} (Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = {π β£ (π Fn {π} β§ (πβπ) β (Baseβπ
))}) |
|
7.6.2 Ideals and spans
|
|
Syntax | clidl 13751 |
Ring left-ideal function.
|
class LIdeal |
|
Syntax | crsp 13752 |
Ring span function.
|
class RSpan |
|
Definition | df-lidl 13753 |
Define the class of left ideals of a given ring. An ideal is a submodule
of the ring viewed as a module over itself. (Contributed by Stefan
O'Rear, 31-Mar-2015.)
|
β’ LIdeal = (LSubSp β
ringLMod) |
|
Definition | df-rsp 13754 |
Define the linear span function in a ring (Ideal generator). (Contributed
by Stefan O'Rear, 4-Apr-2015.)
|
β’ RSpan = (LSpan β
ringLMod) |
|
Theorem | lidlvalg 13755 |
Value of the set of ring ideals. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π β π β (LIdealβπ) = (LSubSpβ(ringLModβπ))) |
|
Theorem | rspvalg 13756 |
Value of the ring span function. (Contributed by Stefan O'Rear,
4-Apr-2015.)
|
β’ (π β π β (RSpanβπ) = (LSpanβ(ringLModβπ))) |
|
Theorem | lidlex 13757 |
Existence of the set of left ideals. (Contributed by Jim Kingdon,
27-Apr-2025.)
|
β’ (π β π β (LIdealβπ) β V) |
|
Theorem | rspex 13758 |
Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
|
β’ (π β π β (RSpanβπ) β V) |
|
Theorem | lidlmex 13759 |
Existence of the set a left ideal is built from (when the ideal is
inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
|
β’ πΌ = (LIdealβπ) β β’ (π β πΌ β π β V) |
|
Theorem | lidlss 13760 |
An ideal is a subset of the base set. (Contributed by Stefan O'Rear,
28-Mar-2015.)
|
β’ π΅ = (Baseβπ)
& β’ πΌ = (LIdealβπ) β β’ (π β πΌ β π β π΅) |
|
Theorem | lidlssbas 13761 |
The base set of the restriction of the ring to a (left) ideal is a
subset of the base set of the ring. (Contributed by AV,
17-Feb-2020.)
|
β’ πΏ = (LIdealβπ
)
& β’ πΌ = (π
βΎs π) β β’ (π β πΏ β (BaseβπΌ) β (Baseβπ
)) |
|
Theorem | lidlbas 13762 |
A (left) ideal of a ring is the base set of the restriction of the ring
to this ideal. (Contributed by AV, 17-Feb-2020.)
|
β’ πΏ = (LIdealβπ
)
& β’ πΌ = (π
βΎs π) β β’ (π β πΏ β (BaseβπΌ) = π) |
|
Theorem | islidlm 13763* |
Predicate of being a (left) ideal. (Contributed by Stefan O'Rear,
1-Apr-2015.)
|
β’ π = (LIdealβπ
)
& β’ π΅ = (Baseβπ
)
& β’ + =
(+gβπ
)
& β’ Β· =
(.rβπ
) β β’ (πΌ β π β (πΌ β π΅ β§ βπ π β πΌ β§ βπ₯ β π΅ βπ β πΌ βπ β πΌ ((π₯ Β· π) + π) β πΌ)) |
|
Theorem | rnglidlmcl 13764 |
A (left) ideal containing the zero element is closed under
left-multiplication by elements of the full non-unital ring. If the
ring is not a unital ring, and the ideal does not contain the zero
element of the ring, then the closure cannot be proven. (Contributed
by AV, 18-Feb-2025.)
|
β’ 0 =
(0gβπ
)
& β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
)
& β’ π = (LIdealβπ
) β β’ (((π
β Rng β§ πΌ β π β§ 0 β πΌ) β§ (π β π΅ β§ π β πΌ)) β (π Β· π) β πΌ) |
|
Theorem | dflidl2rng 13765* |
Alternate (the usual textbook) definition of a (left) ideal of a
non-unital ring to be a subgroup of the additive group of the ring which
is closed under left-multiplication by elements of the full ring.
(Contributed by AV, 21-Mar-2025.)
|
β’ π = (LIdealβπ
)
& β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
) β β’ ((π
β Rng β§ πΌ β (SubGrpβπ
)) β (πΌ β π β βπ₯ β π΅ βπ¦ β πΌ (π₯ Β· π¦) β πΌ)) |
|
Theorem | isridlrng 13766* |
A right ideal is a left ideal of the opposite non-unital ring. This
theorem shows that this definition corresponds to the usual textbook
definition of a right ideal of a ring to be a subgroup of the additive
group of the ring which is closed under right-multiplication by elements
of the full ring. (Contributed by AV, 21-Mar-2025.)
|
β’ π =
(LIdealβ(opprβπ
)) & β’ π΅ = (Baseβπ
) & β’ Β· =
(.rβπ
) β β’ ((π
β Rng β§ πΌ β (SubGrpβπ
)) β (πΌ β π β βπ₯ β π΅ βπ¦ β πΌ (π¦ Β· π₯) β πΌ)) |
|
Theorem | lidl0cl 13767 |
An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ 0 =
(0gβπ
) β β’ ((π
β Ring β§ πΌ β π) β 0 β πΌ) |
|
Theorem | lidlacl 13768 |
An ideal is closed under addition. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ + =
(+gβπ
) β β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β πΌ)) β (π + π) β πΌ) |
|
Theorem | lidlnegcl 13769 |
An ideal contains negatives. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ π = (invgβπ
) β β’ ((π
β Ring β§ πΌ β π β§ π β πΌ) β (πβπ) β πΌ) |
|
Theorem | lidlsubg 13770 |
An ideal is a subgroup of the additive group. (Contributed by Mario
Carneiro, 14-Jun-2015.)
|
β’ π = (LIdealβπ
) β β’ ((π
β Ring β§ πΌ β π) β πΌ β (SubGrpβπ
)) |
|
Theorem | lidlsubcl 13771 |
An ideal is closed under subtraction. (Contributed by Stefan O'Rear,
28-Mar-2015.) (Proof shortened by OpenAI, 25-Mar-2020.)
|
β’ π = (LIdealβπ
)
& β’ β =
(-gβπ
) β β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β πΌ)) β (π β π) β πΌ) |
|
Theorem | dflidl2 13772* |
Alternate (the usual textbook) definition of a (left) ideal of a ring to
be a subgroup of the additive group of the ring which is closed under
left-multiplication by elements of the full ring. (Contributed by AV,
13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
|
β’ π = (LIdealβπ
)
& β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
) β β’ (π
β Ring β (πΌ β π β (πΌ β (SubGrpβπ
) β§ βπ₯ β π΅ βπ¦ β πΌ (π₯ Β· π¦) β πΌ))) |
|
Theorem | lidl0 13773 |
Every ring contains a zero ideal. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ 0 =
(0gβπ
) β β’ (π
β Ring β { 0 } β π) |
|
Theorem | lidl1 13774 |
Every ring contains a unit ideal. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ π΅ = (Baseβπ
) β β’ (π
β Ring β π΅ β π) |
|
Theorem | rspcl 13775 |
The span of a set of ring elements is an ideal. (Contributed by
Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro,
2-Oct-2015.)
|
β’ πΎ = (RSpanβπ
)
& β’ π΅ = (Baseβπ
)
& β’ π = (LIdealβπ
) β β’ ((π
β Ring β§ πΊ β π΅) β (πΎβπΊ) β π) |
|
Theorem | rspssid 13776 |
The span of a set of ring elements contains those elements.
(Contributed by Stefan O'Rear, 3-Jan-2015.)
|
β’ πΎ = (RSpanβπ
)
& β’ π΅ = (Baseβπ
) β β’ ((π
β Ring β§ πΊ β π΅) β πΊ β (πΎβπΊ)) |
|
Theorem | rsp0 13777 |
The span of the zero element is the zero ideal. (Contributed by
Stefan O'Rear, 3-Jan-2015.)
|
β’ πΎ = (RSpanβπ
)
& β’ 0 =
(0gβπ
) β β’ (π
β Ring β (πΎβ{ 0 }) = { 0 }) |
|
Theorem | rspssp 13778 |
The ideal span of a set of elements in a ring is contained in any
subring which contains those elements. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
β’ πΎ = (RSpanβπ
)
& β’ π = (LIdealβπ
) β β’ ((π
β Ring β§ πΌ β π β§ πΊ β πΌ) β (πΎβπΊ) β πΌ) |
|
Theorem | lidlrsppropdg 13779* |
The left ideals and ring span of a ring depend only on the ring
components. Here π is expected to be either π΅ (when
closure is
available) or V (when strong equality is
available). (Contributed
by Mario Carneiro, 14-Jun-2015.)
|
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β π)
& β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦))
& β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) β π)
& β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦))
& β’ (π β πΎ β π)
& β’ (π β πΏ β π) β β’ (π β ((LIdealβπΎ) = (LIdealβπΏ) β§ (RSpanβπΎ) = (RSpanβπΏ))) |
|
Theorem | rnglidlmmgm 13780 |
The multiplicative group of a (left) ideal of a non-unital ring is a
magma. (Contributed by AV, 17-Feb-2020.) Generalization for
non-unital rings. The assumption 0 β π is required because a
left ideal of a non-unital ring does not have to be a subgroup.
(Revised by AV, 11-Mar-2025.)
|
β’ πΏ = (LIdealβπ
)
& β’ πΌ = (π
βΎs π)
& β’ 0 =
(0gβπ
) β β’ ((π
β Rng β§ π β πΏ β§ 0 β π) β (mulGrpβπΌ) β Mgm) |
|
Theorem | rnglidlmsgrp 13781 |
The multiplicative group of a (left) ideal of a non-unital ring is a
semigroup. (Contributed by AV, 17-Feb-2020.) Generalization for
non-unital rings. The assumption 0 β π is required because a
left ideal of a non-unital ring does not have to be a subgroup.
(Revised by AV, 11-Mar-2025.)
|
β’ πΏ = (LIdealβπ
)
& β’ πΌ = (π
βΎs π)
& β’ 0 =
(0gβπ
) β β’ ((π
β Rng β§ π β πΏ β§ 0 β π) β (mulGrpβπΌ) β Smgrp) |
|
Theorem | rnglidlrng 13782 |
A (left) ideal of a non-unital ring is a non-unital ring. (Contributed
by AV, 17-Feb-2020.) Generalization for non-unital rings. The
assumption π β (SubGrpβπ
) is required because a left ideal of
a non-unital ring does not have to be a subgroup. (Revised by AV,
11-Mar-2025.)
|
β’ πΏ = (LIdealβπ
)
& β’ πΌ = (π
βΎs π) β β’ ((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β πΌ β Rng) |
|
7.6.3 Two-sided ideals and quotient
rings
|
|
Syntax | c2idl 13783 |
Ring two-sided ideal function.
|
class 2Ideal |
|
Definition | df-2idl 13784 |
Define the class of two-sided ideals of a ring. A two-sided ideal is a
left ideal which is also a right ideal (or a left ideal over the opposite
ring). (Contributed by Mario Carneiro, 14-Jun-2015.)
|
β’ 2Ideal = (π β V β¦ ((LIdealβπ) β©
(LIdealβ(opprβπ)))) |
|
Theorem | 2idlvalg 13785 |
Definition of a two-sided ideal. (Contributed by Mario Carneiro,
14-Jun-2015.)
|
β’ πΌ = (LIdealβπ
)
& β’ π = (opprβπ
) & β’ π½ = (LIdealβπ) & β’ π = (2Idealβπ
)
β β’ (π
β π β π = (πΌ β© π½)) |
|
Theorem | 2idlmex 13786 |
Existence of the set a two-sided ideal is built from (when the ideal is
inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
|
β’ π = (2Idealβπ) β β’ (π β π β π β V) |
|
Theorem | isridl 13787* |
A right ideal is a left ideal of the opposite ring. This theorem shows
that this definition corresponds to the usual textbook definition of a
right ideal of a ring to be a subgroup of the additive group of the ring
which is closed under right-multiplication by elements of the full ring.
(Contributed by AV, 13-Feb-2025.)
|
β’ π =
(LIdealβ(opprβπ
)) & β’ π΅ = (Baseβπ
) & β’ Β· =
(.rβπ
) β β’ (π
β Ring β (πΌ β π β (πΌ β (SubGrpβπ
) β§ βπ₯ β π΅ βπ¦ β πΌ (π¦ Β· π₯) β πΌ))) |
|
Theorem | 2idlelb 13788 |
Membership in a two-sided ideal. (Contributed by Mario Carneiro,
14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
|
β’ πΌ = (LIdealβπ
)
& β’ π = (opprβπ
) & β’ π½ = (LIdealβπ) & β’ π = (2Idealβπ
)
β β’ (π β π β (π β πΌ β§ π β π½)) |
|
Theorem | 2idllidld 13789 |
A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux,
9-Mar-2025.)
|
β’ (π β πΌ β (2Idealβπ
)) β β’ (π β πΌ β (LIdealβπ
)) |
|
Theorem | 2idlridld 13790 |
A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux,
9-Mar-2025.)
|
β’ (π β πΌ β (2Idealβπ
)) & β’ π =
(opprβπ
) β β’ (π β πΌ β (LIdealβπ)) |
|
Theorem | df2idl2rng 13791* |
Alternate (the usual textbook) definition of a two-sided ideal of a
non-unital ring to be a subgroup of the additive group of the ring which
is closed under left- and right-multiplication by elements of the full
ring. (Contributed by AV, 21-Mar-2025.)
|
β’ π = (2Idealβπ
)
& β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
) β β’ ((π
β Rng β§ πΌ β (SubGrpβπ
)) β (πΌ β π β βπ₯ β π΅ βπ¦ β πΌ ((π₯ Β· π¦) β πΌ β§ (π¦ Β· π₯) β πΌ))) |
|
Theorem | df2idl2 13792* |
Alternate (the usual textbook) definition of a two-sided ideal of a ring
to be a subgroup of the additive group of the ring which is closed under
left- and right-multiplication by elements of the full ring.
(Contributed by AV, 13-Feb-2025.) (Proof shortened by AV,
18-Apr-2025.)
|
β’ π = (2Idealβπ
)
& β’ π΅ = (Baseβπ
)
& β’ Β· =
(.rβπ
) β β’ (π
β Ring β (πΌ β π β (πΌ β (SubGrpβπ
) β§ βπ₯ β π΅ βπ¦ β πΌ ((π₯ Β· π¦) β πΌ β§ (π¦ Β· π₯) β πΌ)))) |
|
Theorem | ridl0 13793 |
Every ring contains a zero right ideal. (Contributed by AV,
13-Feb-2025.)
|
β’ π =
(LIdealβ(opprβπ
)) & β’ 0 =
(0gβπ
) β β’ (π
β Ring β { 0 } β π) |
|
Theorem | ridl1 13794 |
Every ring contains a unit right ideal. (Contributed by AV,
13-Feb-2025.)
|
β’ π =
(LIdealβ(opprβπ
)) & β’ π΅ = (Baseβπ
)
β β’ (π
β Ring β π΅ β π) |
|
Theorem | 2idl0 13795 |
Every ring contains a zero two-sided ideal. (Contributed by AV,
13-Feb-2025.)
|
β’ πΌ = (2Idealβπ
)
& β’ 0 =
(0gβπ
) β β’ (π
β Ring β { 0 } β πΌ) |
|
Theorem | 2idl1 13796 |
Every ring contains a unit two-sided ideal. (Contributed by AV,
13-Feb-2025.)
|
β’ πΌ = (2Idealβπ
)
& β’ π΅ = (Baseβπ
) β β’ (π
β Ring β π΅ β πΌ) |
|
Theorem | 2idlss 13797 |
A two-sided ideal is a subset of the base set. (Contributed by Mario
Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened
by AV, 13-Mar-2025.)
|
β’ π΅ = (Baseβπ)
& β’ πΌ = (2Idealβπ) β β’ (π β πΌ β π β π΅) |
|
Theorem | 2idlbas 13798 |
The base set of a two-sided ideal as structure. (Contributed by AV,
20-Feb-2025.)
|
β’ (π β πΌ β (2Idealβπ
)) & β’ π½ = (π
βΎs πΌ)
& β’ π΅ = (Baseβπ½) β β’ (π β π΅ = πΌ) |
|
Theorem | 2idlelbas 13799 |
The base set of a two-sided ideal as structure is a left and right
ideal. (Contributed by AV, 20-Feb-2025.)
|
β’ (π β πΌ β (2Idealβπ
)) & β’ π½ = (π
βΎs πΌ)
& β’ π΅ = (Baseβπ½) β β’ (π β (π΅ β (LIdealβπ
) β§ π΅ β
(LIdealβ(opprβπ
)))) |
|
Theorem | rng2idlsubrng 13800 |
A two-sided ideal of a non-unital ring which is a non-unital ring is a
subring of the ring. (Contributed by AV, 20-Feb-2025.) (Revised by AV,
11-Mar-2025.)
|
β’ (π β π
β Rng) & β’ (π β πΌ β (2Idealβπ
)) & β’ (π β (π
βΎs πΌ) β Rng)
β β’ (π β πΌ β (SubRngβπ
)) |