Theorem List for Intuitionistic Logic Explorer - 13701-13800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | lspuni0 13701 |
Union of the span of the empty set. (Contributed by NM,
14-Mar-2015.)
|
⊢ 0 =
(0g‘𝑊)
& ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → ∪ (𝑁‘∅) = 0 ) |
|
Theorem | lspun0 13702 |
The span of a union with the zero subspace. (Contributed by NM,
22-May-2015.)
|
⊢ 𝑉 = (Base‘𝑊)
& ⊢ 0 =
(0g‘𝑊)
& ⊢ 𝑁 = (LSpan‘𝑊)
& ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘(𝑋 ∪ { 0 })) = (𝑁‘𝑋)) |
|
Theorem | lspsneq0 13703 |
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 13704 |
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 13705 |
Two independent (non-colinear) vectors have nonzero sum. (Contributed
by NM, 22-Apr-2015.)
|
⊢ 𝑉 = (Base‘𝑊)
& ⊢ + =
(+g‘𝑊)
& ⊢ 0 =
(0g‘𝑊)
& ⊢ 𝑁 = (LSpan‘𝑊)
& ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉)
& ⊢ (𝜑 → 𝑌 ∈ 𝑉)
& ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 ) |
|
Theorem | lsslsp 13706 |
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 13707 |
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 13708* |
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 13709* |
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 13710 |
Extend class notation with the subring algebra generator.
|
class subringAlg |
|
Syntax | crglmod 13711 |
Extend class notation with the left module induced by a ring over
itself.
|
class ringLMod |
|
Definition | df-sra 13712* |
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 13713 |
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 13714 |
Lemma for srabaseg 13716 through sravscag 13720. (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 13715 |
Lemma for srabaseg 13716 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 13716 |
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 13717 |
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 13718 |
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 13719 |
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 13720 |
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 13721 |
The inner product operation of a subring algebra. (Contributed by
Thierry Arnoux, 16-Jun-2019.)
|
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → (.r‘𝑊) =
(·𝑖‘𝐴)) |
|
Theorem | sratsetg 13722 |
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 13723 |
Existence of a subring algebra. (Contributed by Jim Kingdon,
16-Apr-2025.)
|
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐴 ∈ V) |
|
Theorem | sratopng 13724 |
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 13725 |
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 13726 |
Condition for a subring algebra to be a ring. (Contributed by Thierry
Arnoux, 24-Jul-2023.)
|
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)
& ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ Ring) |
|
Theorem | sralmod 13727 |
The subring algebra is a left module. (Contributed by Stefan O'Rear,
27-Nov-2014.)
|
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) ⇒ ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod) |
|
Theorem | sralmod0g 13728 |
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 13729* |
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 13730 |
ringLMod is a function. (Contributed by Stefan O'Rear,
6-Dec-2014.)
|
⊢ ringLMod Fn V |
|
Theorem | rlmvalg 13731 |
Value of the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
⊢ (𝑊 ∈ 𝑉 → (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊))) |
|
Theorem | rlmbasg 13732 |
Base set of the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
⊢ (𝑅 ∈ 𝑉 → (Base‘𝑅) = (Base‘(ringLMod‘𝑅))) |
|
Theorem | rlmplusgg 13733 |
Vector addition in the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
⊢ (𝑅 ∈ 𝑉 → (+g‘𝑅) =
(+g‘(ringLMod‘𝑅))) |
|
Theorem | rlm0g 13734 |
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 13735 |
Subtraction in the ring module. (Contributed by Thierry Arnoux,
30-Jun-2019.)
|
⊢ (𝑅 ∈ 𝑉 → (-g‘𝑅) =
(-g‘(ringLMod‘𝑅))) |
|
Theorem | rlmmulrg 13736 |
Ring multiplication in the ring module. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
⊢ (𝑅 ∈ 𝑉 → (.r‘𝑅) =
(.r‘(ringLMod‘𝑅))) |
|
Theorem | rlmscabas 13737 |
Scalars in the ring module have the same base set. (Contributed by Jim
Kingdon, 29-Apr-2025.)
|
⊢ (𝑅 ∈ 𝑋 → (Base‘𝑅) =
(Base‘(Scalar‘(ringLMod‘𝑅)))) |
|
Theorem | rlmvscag 13738 |
Scalar multiplication in the ring module. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
⊢ (𝑅 ∈ 𝑉 → (.r‘𝑅) = (
·𝑠 ‘(ringLMod‘𝑅))) |
|
Theorem | rlmtopng 13739 |
Topology component of the ring module. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
⊢ (𝑅 ∈ 𝑉 → (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅))) |
|
Theorem | rlmdsg 13740 |
Metric component of the ring module. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
⊢ (𝑅 ∈ 𝑉 → (dist‘𝑅) = (dist‘(ringLMod‘𝑅))) |
|
Theorem | rlmlmod 13741 |
The ring module is a module. (Contributed by Stefan O'Rear,
6-Dec-2014.)
|
⊢ (𝑅 ∈ Ring → (ringLMod‘𝑅) ∈ LMod) |
|
Theorem | rlmvnegg 13742 |
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 13743* |
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 13744 |
Ring left-ideal function.
|
class LIdeal |
|
Syntax | crsp 13745 |
Ring span function.
|
class RSpan |
|
Definition | df-lidl 13746 |
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 13747 |
Define the linear span function in a ring (Ideal generator). (Contributed
by Stefan O'Rear, 4-Apr-2015.)
|
⊢ RSpan = (LSpan ∘
ringLMod) |
|
Theorem | lidlvalg 13748 |
Value of the set of ring ideals. (Contributed by Stefan O'Rear,
31-Mar-2015.)
|
⊢ (𝑊 ∈ 𝑉 → (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊))) |
|
Theorem | rspvalg 13749 |
Value of the ring span function. (Contributed by Stefan O'Rear,
4-Apr-2015.)
|
⊢ (𝑊 ∈ 𝑉 → (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊))) |
|
Theorem | lidlex 13750 |
Existence of the set of left ideals. (Contributed by Jim Kingdon,
27-Apr-2025.)
|
⊢ (𝑊 ∈ 𝑉 → (LIdeal‘𝑊) ∈ V) |
|
Theorem | rspex 13751 |
Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
|
⊢ (𝑊 ∈ 𝑉 → (RSpan‘𝑊) ∈ V) |
|
Theorem | lidlmex 13752 |
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 13753 |
An ideal is a subset of the base set. (Contributed by Stefan O'Rear,
28-Mar-2015.)
|
⊢ 𝐵 = (Base‘𝑊)
& ⊢ 𝐼 = (LIdeal‘𝑊) ⇒ ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵) |
|
Theorem | lidlssbas 13754 |
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 13755 |
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 13756* |
Predicate of being a (left) ideal. (Contributed by Stefan O'Rear,
1-Apr-2015.)
|
⊢ 𝑈 = (LIdeal‘𝑅)
& ⊢ 𝐵 = (Base‘𝑅)
& ⊢ + =
(+g‘𝑅)
& ⊢ · =
(.r‘𝑅) ⇒ ⊢ (𝐼 ∈ 𝑈 ↔ (𝐼 ⊆ 𝐵 ∧ ∃𝑗 𝑗 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐼 ((𝑥 · 𝑎) + 𝑏) ∈ 𝐼)) |
|
Theorem | rnglidlmcl 13757 |
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 13758* |
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 13759* |
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 13760 |
An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|
⊢ 𝑈 = (LIdeal‘𝑅)
& ⊢ 0 =
(0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 0 ∈ 𝐼) |
|
Theorem | lidlacl 13761 |
An ideal is closed under addition. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
⊢ 𝑈 = (LIdeal‘𝑅)
& ⊢ + =
(+g‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (𝑋 + 𝑌) ∈ 𝐼) |
|
Theorem | lidlnegcl 13762 |
An ideal contains negatives. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
⊢ 𝑈 = (LIdeal‘𝑅)
& ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼) |
|
Theorem | lidlsubg 13763 |
An ideal is a subgroup of the additive group. (Contributed by Mario
Carneiro, 14-Jun-2015.)
|
⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (SubGrp‘𝑅)) |
|
Theorem | lidlsubcl 13764 |
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 13765* |
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 13766 |
Every ring contains a zero ideal. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
⊢ 𝑈 = (LIdeal‘𝑅)
& ⊢ 0 =
(0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈) |
|
Theorem | lidl1 13767 |
Every ring contains a unit ideal. (Contributed by Stefan O'Rear,
3-Jan-2015.)
|
⊢ 𝑈 = (LIdeal‘𝑅)
& ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈) |
|
Theorem | rspcl 13768 |
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 13769 |
The span of a set of ring elements contains those elements.
(Contributed by Stefan O'Rear, 3-Jan-2015.)
|
⊢ 𝐾 = (RSpan‘𝑅)
& ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) |
|
Theorem | rsp0 13770 |
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 13771 |
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 13772* |
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 13773 |
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 13774 |
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 13775 |
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 13776 |
Ring two-sided ideal function.
|
class 2Ideal |
|
Definition | df-2idl 13777 |
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 13778 |
Definition of a two-sided ideal. (Contributed by Mario Carneiro,
14-Jun-2015.)
|
⊢ 𝐼 = (LIdeal‘𝑅)
& ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐽 = (LIdeal‘𝑂) & ⊢ 𝑇 = (2Ideal‘𝑅)
⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑇 = (𝐼 ∩ 𝐽)) |
|
Theorem | 2idlmex 13779 |
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 13780* |
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 13781 |
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 13782 |
A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux,
9-Mar-2025.)
|
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) ⇒ ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) |
|
Theorem | 2idlridld 13783 |
A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux,
9-Mar-2025.)
|
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝑂 =
(oppr‘𝑅) ⇒ ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑂)) |
|
Theorem | df2idl2rng 13784* |
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 13785* |
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 13786 |
Every ring contains a zero right ideal. (Contributed by AV,
13-Feb-2025.)
|
⊢ 𝑈 =
(LIdeal‘(oppr‘𝑅)) & ⊢ 0 =
(0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈) |
|
Theorem | ridl1 13787 |
Every ring contains a unit right ideal. (Contributed by AV,
13-Feb-2025.)
|
⊢ 𝑈 =
(LIdeal‘(oppr‘𝑅)) & ⊢ 𝐵 = (Base‘𝑅)
⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈) |
|
Theorem | 2idl0 13788 |
Every ring contains a zero two-sided ideal. (Contributed by AV,
13-Feb-2025.)
|
⊢ 𝐼 = (2Ideal‘𝑅)
& ⊢ 0 =
(0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝐼) |
|
Theorem | 2idl1 13789 |
Every ring contains a unit two-sided ideal. (Contributed by AV,
13-Feb-2025.)
|
⊢ 𝐼 = (2Ideal‘𝑅)
& ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝐼) |
|
Theorem | 2idlss 13790 |
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 13791 |
The base set of a two-sided ideal as structure. (Contributed by AV,
20-Feb-2025.)
|
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐽 = (𝑅 ↾s 𝐼)
& ⊢ 𝐵 = (Base‘𝐽) ⇒ ⊢ (𝜑 → 𝐵 = 𝐼) |
|
Theorem | 2idlelbas 13792 |
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 13793 |
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‘𝑅)) |
|
Theorem | rng2idlnsg 13794 |
A two-sided ideal of a non-unital ring which is a non-unital ring is a
normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|
⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng)
⇒ ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) |
|
Theorem | rng2idl0 13795 |
The zero (additive identity) of a non-unital ring is an element of each
two-sided ideal of the ring which is a non-unital ring. (Contributed by
AV, 20-Feb-2025.)
|
⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng)
⇒ ⊢ (𝜑 → (0g‘𝑅) ∈ 𝐼) |
|
Theorem | rng2idlsubgsubrng 13796 |
A two-sided ideal of a non-unital ring which is a subgroup of the ring
is a subring of the ring. (Contributed by AV, 11-Mar-2025.)
|
⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅)) ⇒ ⊢ (𝜑 → 𝐼 ∈ (SubRng‘𝑅)) |
|
Theorem | rng2idlsubgnsg 13797 |
A two-sided ideal of a non-unital ring which is a subgroup of the ring
is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|
⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅)) ⇒ ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) |
|
Theorem | rng2idlsubg0 13798 |
The zero (additive identity) of a non-unital ring is an element of each
two-sided ideal of the ring which is a subgroup of the ring.
(Contributed by AV, 20-Feb-2025.)
|
⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅)) ⇒ ⊢ (𝜑 → (0g‘𝑅) ∈ 𝐼) |
|
Theorem | 2idlcpblrng 13799 |
The coset equivalence relation for a two-sided ideal is compatible with
ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
Generalization for non-unital rings and two-sided ideals which are
subgroups of the additive group of the non-unital ring. (Revised by AV,
23-Feb-2025.)
|
⊢ 𝑋 = (Base‘𝑅)
& ⊢ 𝐸 = (𝑅 ~QG 𝑆)
& ⊢ 𝐼 = (2Ideal‘𝑅)
& ⊢ · =
(.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ (SubGrp‘𝑅)) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷))) |
|
Theorem | 2idlcpbl 13800 |
The coset equivalence relation for a two-sided ideal is compatible with
ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
(Proof shortened by AV, 31-Mar-2025.)
|
⊢ 𝑋 = (Base‘𝑅)
& ⊢ 𝐸 = (𝑅 ~QG 𝑆)
& ⊢ 𝐼 = (2Ideal‘𝑅)
& ⊢ · =
(.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷))) |