Type | Label | Description |
Statement |
|
Theorem | lspsnel 13601* |
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 13602 |
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 13603* |
Comparable spans of singletons must have proportional vectors.
(Contributed by NM, 7-Jun-2015.)
|
β’ π = (Baseβπ)
& β’ π = (Scalarβπ)
& β’ πΎ = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β ((πβ{π}) β (πβ{π}) β βπ β πΎ π = (π Β· π))) |
|
Theorem | lspsnneg 13604 |
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 13605 |
Swapping subtraction order does not change the span of a singleton.
(Contributed by NM, 4-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ β =
(-gβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (πβ{(π β π)}) = (πβ{(π β π)})) |
|
Theorem | lspsn0 13606 |
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 13607 |
Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.)
|
β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ) β β’ (π β LMod β (πββ
) = { 0 }) |
|
Theorem | lspuni0 13608 |
Union of the span of the empty set. (Contributed by NM,
14-Mar-2015.)
|
β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ) β β’ (π β LMod β βͺ (πββ
) = 0 ) |
|
Theorem | lspun0 13609 |
The span of a union with the zero subspace. (Contributed by NM,
22-May-2015.)
|
β’ π = (Baseβπ)
& β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β (πβ(π βͺ { 0 })) = (πβπ)) |
|
Theorem | lspsneq0 13610 |
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 13611 |
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 13612 |
Two independent (non-colinear) vectors have nonzero sum. (Contributed
by NM, 22-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ 0 =
(0gβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π)
& β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π + π) β 0 ) |
|
Theorem | lsslsp 13613 |
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 13614 |
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 13615* |
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 13616* |
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 13617 |
Extend class notation with the subring algebra generator.
|
class subringAlg |
|
Syntax | crglmod 13618 |
Extend class notation with the left module induced by a ring over
itself.
|
class ringLMod |
|
Definition | df-sra 13619* |
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 13620 |
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 13621 |
Lemma for srabaseg 13623 through sravscag 13627. (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 13622 |
Lemma for srabaseg 13623 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 13623 |
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 13624 |
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 13625 |
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 13626 |
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 13627 |
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 13628 |
The inner product operation of a subring algebra. (Contributed by
Thierry Arnoux, 16-Jun-2019.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β (.rβπ) =
(Β·πβπ΄)) |
|
Theorem | sratsetg 13629 |
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 13630 |
Existence of a subring algebra. (Contributed by Jim Kingdon,
16-Apr-2025.)
|
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ (π β π β π) β β’ (π β π΄ β V) |
|
Theorem | sratopng 13631 |
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 13632 |
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 13633 |
Condition for a subring algebra to be a ring. (Contributed by Thierry
Arnoux, 24-Jul-2023.)
|
β’ π΄ = ((subringAlg βπ
)βπ)
& β’ π΅ = (Baseβπ
) β β’ ((π
β Ring β§ π β π΅) β π΄ β Ring) |
|
Theorem | sralmod 13634 |
The subring algebra is a left module. (Contributed by Stefan O'Rear,
27-Nov-2014.)
|
β’ π΄ = ((subringAlg βπ)βπ) β β’ (π β (SubRingβπ) β π΄ β LMod) |
|
Theorem | sralmod0g 13635 |
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 13636* |
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 13637 |
ringLMod is a function. (Contributed by Stefan O'Rear,
6-Dec-2014.)
|
β’ ringLMod Fn V |
|
Theorem | rlmvalg 13638 |
Value of the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π β π β (ringLModβπ) = ((subringAlg βπ)β(Baseβπ))) |
|
Theorem | rlmbasg 13639 |
Base set of the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π
β π β (Baseβπ
) = (Baseβ(ringLModβπ
))) |
|
Theorem | rlmplusgg 13640 |
Vector addition in the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π
β π β (+gβπ
) =
(+gβ(ringLModβπ
))) |
|
Theorem | rlm0g 13641 |
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 13642 |
Subtraction in the ring module. (Contributed by Thierry Arnoux,
30-Jun-2019.)
|
β’ (π
β π β (-gβπ
) =
(-gβ(ringLModβπ
))) |
|
Theorem | rlmmulrg 13643 |
Ring multiplication in the ring module. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
β’ (π
β π β (.rβπ
) =
(.rβ(ringLModβπ
))) |
|
Theorem | rlmscabas 13644 |
Scalars in the ring module have the same base set. (Contributed by Jim
Kingdon, 29-Apr-2025.)
|
β’ (π
β π β (Baseβπ
) =
(Baseβ(Scalarβ(ringLModβπ
)))) |
|
Theorem | rlmvscag 13645 |
Scalar multiplication in the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π
β π β (.rβπ
) = (
Β·π β(ringLModβπ
))) |
|
Theorem | rlmtopng 13646 |
Topology component of the ring module. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
β’ (π
β π β (TopOpenβπ
) = (TopOpenβ(ringLModβπ
))) |
|
Theorem | rlmdsg 13647 |
Metric component of the ring module. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
β’ (π
β π β (distβπ
) = (distβ(ringLModβπ
))) |
|
Theorem | rlmlmod 13648 |
The ring module is a module. (Contributed by Stefan O'Rear,
6-Dec-2014.)
|
β’ (π
β Ring β (ringLModβπ
) β LMod) |
|
Theorem | rlmvnegg 13649 |
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 13650* |
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 13651 |
Ring left-ideal function.
|
class LIdeal |
|
Syntax | crsp 13652 |
Ring span function.
|
class RSpan |
|
Definition | df-lidl 13653 |
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 13654 |
Define the linear span function in a ring (Ideal generator). (Contributed
by Stefan O'Rear, 4-Apr-2015.)
|
β’ RSpan = (LSpan β
ringLMod) |
|
Theorem | lidlvalg 13655 |
Value of the set of ring ideals. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
β’ (π β π β (LIdealβπ) = (LSubSpβ(ringLModβπ))) |
|
Theorem | rspvalg 13656 |
Value of the ring span function. (Contributed by Stefan O'Rear,
4-Apr-2015.)
|
β’ (π β π β (RSpanβπ) = (LSpanβ(ringLModβπ))) |
|
Theorem | lidlex 13657 |
Existence of the set of left ideals. (Contributed by Jim Kingdon,
27-Apr-2025.)
|
β’ (π β π β (LIdealβπ) β V) |
|
Theorem | rspex 13658 |
Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
|
β’ (π β π β (RSpanβπ) β V) |
|
Theorem | lidlmex 13659 |
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 13660 |
An ideal is a subset of the base set. (Contributed by Stefan O'Rear,
28-Mar-2015.)
|
β’ π΅ = (Baseβπ)
& β’ πΌ = (LIdealβπ) β β’ (π β πΌ β π β π΅) |
|
Theorem | lidlssbas 13661 |
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 13662 |
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 13663* |
Predicate of being a (left) ideal. (Contributed by Stefan O'Rear,
1-Apr-2015.)
|
β’ π = (LIdealβπ
)
& β’ π΅ = (Baseβπ
)
& β’ + =
(+gβπ
)
& β’ Β· =
(.rβπ
) β β’ (πΌ β π β (πΌ β π΅ β§ βπ π β πΌ β§ βπ₯ β π΅ βπ β πΌ βπ β πΌ ((π₯ Β· π) + π) β πΌ)) |
|
Theorem | rnglidlmcl 13664 |
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 13665* |
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 13666* |
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 13667 |
An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ 0 =
(0gβπ
) β β’ ((π
β Ring β§ πΌ β π) β 0 β πΌ) |
|
Theorem | lidlacl 13668 |
An ideal is closed under addition. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ + =
(+gβπ
) β β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β πΌ)) β (π + π) β πΌ) |
|
Theorem | lidlnegcl 13669 |
An ideal contains negatives. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ π = (invgβπ
) β β’ ((π
β Ring β§ πΌ β π β§ π β πΌ) β (πβπ) β πΌ) |
|
Theorem | lidlsubg 13670 |
An ideal is a subgroup of the additive group. (Contributed by Mario
Carneiro, 14-Jun-2015.)
|
β’ π = (LIdealβπ
) β β’ ((π
β Ring β§ πΌ β π) β πΌ β (SubGrpβπ
)) |
|
Theorem | lidlsubcl 13671 |
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 13672* |
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 13673 |
Every ring contains a zero ideal. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ 0 =
(0gβπ
) β β’ (π
β Ring β { 0 } β π) |
|
Theorem | lidl1 13674 |
Every ring contains a unit ideal. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
β’ π = (LIdealβπ
)
& β’ π΅ = (Baseβπ
) β β’ (π
β Ring β π΅ β π) |
|
Theorem | rspcl 13675 |
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 13676 |
The span of a set of ring elements contains those elements.
(Contributed by Stefan O'Rear, 3-Jan-2015.)
|
β’ πΎ = (RSpanβπ
)
& β’ π΅ = (Baseβπ
) β β’ ((π
β Ring β§ πΊ β π΅) β πΊ β (πΎβπΊ)) |
|
Theorem | rsp0 13677 |
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 13678 |
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 β§ πΌ β π β§ πΊ β πΌ) β (πΎβπΊ) β πΌ) |
|
7.6.3 Two-sided ideals and quotient
rings
|
|
Syntax | c2idl 13679 |
Ring two-sided ideal function.
|
class 2Ideal |
|
Definition | df-2idl 13680 |
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 13681 |
Definition of a two-sided ideal. (Contributed by Mario Carneiro,
14-Jun-2015.)
|
β’ πΌ = (LIdealβπ
)
& β’ π = (opprβπ
) & β’ π½ = (LIdealβπ) & β’ π = (2Idealβπ
)
β β’ (π
β π β π = (πΌ β© π½)) |
|
Theorem | 2idlmex 13682 |
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 13683* |
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 13684 |
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 13685 |
A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux,
9-Mar-2025.)
|
β’ (π β πΌ β (2Idealβπ
)) β β’ (π β πΌ β (LIdealβπ
)) |
|
Theorem | 2idlridld 13686 |
A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux,
9-Mar-2025.)
|
β’ (π β πΌ β (2Idealβπ
)) & β’ π =
(opprβπ
) β β’ (π β πΌ β (LIdealβπ)) |
|
Theorem | df2idl2rng 13687* |
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 13688* |
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 13689 |
Every ring contains a zero right ideal. (Contributed by AV,
13-Feb-2025.)
|
β’ π =
(LIdealβ(opprβπ
)) & β’ 0 =
(0gβπ
) β β’ (π
β Ring β { 0 } β π) |
|
Theorem | ridl1 13690 |
Every ring contains a unit right ideal. (Contributed by AV,
13-Feb-2025.)
|
β’ π =
(LIdealβ(opprβπ
)) & β’ π΅ = (Baseβπ
)
β β’ (π
β Ring β π΅ β π) |
|
Theorem | 2idl0 13691 |
Every ring contains a zero two-sided ideal. (Contributed by AV,
13-Feb-2025.)
|
β’ πΌ = (2Idealβπ
)
& β’ 0 =
(0gβπ
) β β’ (π
β Ring β { 0 } β πΌ) |
|
Theorem | 2idl1 13692 |
Every ring contains a unit two-sided ideal. (Contributed by AV,
13-Feb-2025.)
|
β’ πΌ = (2Idealβπ
)
& β’ π΅ = (Baseβπ
) β β’ (π
β Ring β π΅ β πΌ) |
|
Theorem | 2idlss 13693 |
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 13694 |
The base set of a two-sided ideal as structure. (Contributed by AV,
20-Feb-2025.)
|
β’ (π β πΌ β (2Idealβπ
)) & β’ π½ = (π
βΎs πΌ)
& β’ π΅ = (Baseβπ½) β β’ (π β π΅ = πΌ) |
|
Theorem | 2idlelbas 13695 |
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βπ
)))) |
|
7.7 The complex numbers as an algebraic
extensible structure
|
|
7.7.1 Definition and basic
properties
|
|
Syntax | cpsmet 13696 |
Extend class notation with the class of all pseudometric spaces.
|
class PsMet |
|
Syntax | cxmet 13697 |
Extend class notation with the class of all extended metric spaces.
|
class βMet |
|
Syntax | cmet 13698 |
Extend class notation with the class of all metrics.
|
class Met |
|
Syntax | cbl 13699 |
Extend class notation with the metric space ball function.
|
class ball |
|
Syntax | cfbas 13700 |
Extend class definition to include the class of filter bases.
|
class fBas |