HomeHome Intuitionistic Logic Explorer
Theorem List (p. 138 of 153)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 13701-13800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlspuni0 13701 Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.)
0 = (0g𝑊)    &   𝑁 = (LSpan‘𝑊)       (𝑊 ∈ LMod → (𝑁‘∅) = 0 )
 
Theoremlspun0 13702 The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.)
𝑉 = (Base‘𝑊)    &    0 = (0g𝑊)    &   𝑁 = (LSpan‘𝑊)    &   (𝜑𝑊 ∈ LMod)    &   (𝜑𝑋𝑉)       (𝜑 → (𝑁‘(𝑋 ∪ { 0 })) = (𝑁𝑋))
 
Theoremlspsneq0 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 ))
 
Theoremlspsneq0b 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 ))
 
Theoremlmodindp1 13705 Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.)
𝑉 = (Base‘𝑊)    &    + = (+g𝑊)    &    0 = (0g𝑊)    &   𝑁 = (LSpan‘𝑊)    &   (𝜑𝑊 ∈ LMod)    &   (𝜑𝑋𝑉)    &   (𝜑𝑌𝑉)    &   (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))       (𝜑 → (𝑋 + 𝑌) ≠ 0 )
 
Theoremlsslsp 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 ∧ 𝑈𝐿𝐺𝑈) → (𝑁𝐺) = (𝑀𝐺))
 
Theoremlss0v 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 )
 
Theoremlsspropdg 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‘𝐿))
 
Theoremlsppropd 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
 
Syntaxcsra 13710 Extend class notation with the subring algebra generator.
class subringAlg
 
Syntaxcrglmod 13711 Extend class notation with the left module induced by a ring over itself.
class ringLMod
 
Definitiondf-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𝑤)⟩)))
 
Definitiondf-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‘𝑤)))
 
Theoremsraval 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𝑊)⟩))
 
Theoremsralemg 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)       (𝜑 → (𝐸𝑊) = (𝐸𝐴))
 
Theoremsrabaseg 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‘𝐴))
 
Theoremsraaddgg 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𝐴))
 
Theoremsramulrg 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𝐴))
 
Theoremsrascag 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‘𝐴))
 
Theoremsravscag 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𝑊) = ( ·𝑠𝐴))
 
Theoremsraipg 13721 The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))    &   (𝜑𝑊𝑋)       (𝜑 → (.r𝑊) = (·𝑖𝐴))
 
Theoremsratsetg 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‘𝐴))
 
Theoremsraex 13723 Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))    &   (𝜑𝑊𝑋)       (𝜑𝐴 ∈ V)
 
Theoremsratopng 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‘𝐴))
 
Theoremsradsg 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‘𝐴))
 
Theoremsraring 13726 Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   𝐵 = (Base‘𝑅)       ((𝑅 ∈ Ring ∧ 𝑉𝐵) → 𝐴 ∈ Ring)
 
Theoremsralmod 13727 The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
𝐴 = ((subringAlg ‘𝑊)‘𝑆)       (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod)
 
Theoremsralmod0g 13728 The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑0 = (0g𝑊))    &   (𝜑𝑆 ⊆ (Base‘𝑊))    &   (𝜑𝑊𝑋)       (𝜑0 = (0g𝐴))
 
Theoremissubrgd 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‘𝐼))
 
Theoremrlmfn 13730 ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
ringLMod Fn V
 
Theoremrlmvalg 13731 Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑊𝑉 → (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊)))
 
Theoremrlmbasg 13732 Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑅𝑉 → (Base‘𝑅) = (Base‘(ringLMod‘𝑅)))
 
Theoremrlmplusgg 13733 Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑅𝑉 → (+g𝑅) = (+g‘(ringLMod‘𝑅)))
 
Theoremrlm0g 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‘𝑅)))
 
Theoremrlmsubg 13735 Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
(𝑅𝑉 → (-g𝑅) = (-g‘(ringLMod‘𝑅)))
 
Theoremrlmmulrg 13736 Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
(𝑅𝑉 → (.r𝑅) = (.r‘(ringLMod‘𝑅)))
 
Theoremrlmscabas 13737 Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.)
(𝑅𝑋 → (Base‘𝑅) = (Base‘(Scalar‘(ringLMod‘𝑅))))
 
Theoremrlmvscag 13738 Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑅𝑉 → (.r𝑅) = ( ·𝑠 ‘(ringLMod‘𝑅)))
 
Theoremrlmtopng 13739 Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
(𝑅𝑉 → (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅)))
 
Theoremrlmdsg 13740 Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
(𝑅𝑉 → (dist‘𝑅) = (dist‘(ringLMod‘𝑅)))
 
Theoremrlmlmod 13741 The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
(𝑅 ∈ Ring → (ringLMod‘𝑅) ∈ LMod)
 
Theoremrlmvnegg 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‘𝑅)))
 
Theoremixpsnbasval 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
 
Syntaxclidl 13744 Ring left-ideal function.
class LIdeal
 
Syntaxcrsp 13745 Ring span function.
class RSpan
 
Definitiondf-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)
 
Definitiondf-rsp 13747 Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
RSpan = (LSpan ∘ ringLMod)
 
Theoremlidlvalg 13748 Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑊𝑉 → (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊)))
 
Theoremrspvalg 13749 Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
(𝑊𝑉 → (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊)))
 
Theoremlidlex 13750 Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.)
(𝑊𝑉 → (LIdeal‘𝑊) ∈ V)
 
Theoremrspex 13751 Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
(𝑊𝑉 → (RSpan‘𝑊) ∈ V)
 
Theoremlidlmex 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)
 
Theoremlidlss 13753 An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.)
𝐵 = (Base‘𝑊)    &   𝐼 = (LIdeal‘𝑊)       (𝑈𝐼𝑈𝐵)
 
Theoremlidlssbas 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‘𝑅))
 
Theoremlidlbas 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‘𝐼) = 𝑈)
 
Theoremislidlm 13756* Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.)
𝑈 = (LIdeal‘𝑅)    &   𝐵 = (Base‘𝑅)    &    + = (+g𝑅)    &    · = (.r𝑅)       (𝐼𝑈 ↔ (𝐼𝐵 ∧ ∃𝑗 𝑗𝐼 ∧ ∀𝑥𝐵𝑎𝐼𝑏𝐼 ((𝑥 · 𝑎) + 𝑏) ∈ 𝐼))
 
Theoremrnglidlmcl 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𝐼) ∧ (𝑋𝐵𝑌𝐼)) → (𝑋 · 𝑌) ∈ 𝐼)
 
Theoremdflidl2rng 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‘𝑅)) → (𝐼𝑈 ↔ ∀𝑥𝐵𝑦𝐼 (𝑥 · 𝑦) ∈ 𝐼))
 
Theoremisridlrng 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‘𝑅)) → (𝐼𝑈 ↔ ∀𝑥𝐵𝑦𝐼 (𝑦 · 𝑥) ∈ 𝐼))
 
Theoremlidl0cl 13760 An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
𝑈 = (LIdeal‘𝑅)    &    0 = (0g𝑅)       ((𝑅 ∈ Ring ∧ 𝐼𝑈) → 0𝐼)
 
Theoremlidlacl 13761 An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.)
𝑈 = (LIdeal‘𝑅)    &    + = (+g𝑅)       (((𝑅 ∈ Ring ∧ 𝐼𝑈) ∧ (𝑋𝐼𝑌𝐼)) → (𝑋 + 𝑌) ∈ 𝐼)
 
Theoremlidlnegcl 13762 An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.)
𝑈 = (LIdeal‘𝑅)    &   𝑁 = (invg𝑅)       ((𝑅 ∈ Ring ∧ 𝐼𝑈𝑋𝐼) → (𝑁𝑋) ∈ 𝐼)
 
Theoremlidlsubg 13763 An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.)
𝑈 = (LIdeal‘𝑅)       ((𝑅 ∈ Ring ∧ 𝐼𝑈) → 𝐼 ∈ (SubGrp‘𝑅))
 
Theoremlidlsubcl 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 ∧ 𝐼𝑈) ∧ (𝑋𝐼𝑌𝐼)) → (𝑋 𝑌) ∈ 𝐼)
 
Theoremdflidl2 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‘𝑅) ∧ ∀𝑥𝐵𝑦𝐼 (𝑥 · 𝑦) ∈ 𝐼)))
 
Theoremlidl0 13766 Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
𝑈 = (LIdeal‘𝑅)    &    0 = (0g𝑅)       (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
 
Theoremlidl1 13767 Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
𝑈 = (LIdeal‘𝑅)    &   𝐵 = (Base‘𝑅)       (𝑅 ∈ Ring → 𝐵𝑈)
 
Theoremrspcl 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 ∧ 𝐺𝐵) → (𝐾𝐺) ∈ 𝑈)
 
Theoremrspssid 13769 The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
𝐾 = (RSpan‘𝑅)    &   𝐵 = (Base‘𝑅)       ((𝑅 ∈ Ring ∧ 𝐺𝐵) → 𝐺 ⊆ (𝐾𝐺))
 
Theoremrsp0 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 })
 
Theoremrspssp 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 ∧ 𝐼𝑈𝐺𝐼) → (𝐾𝐺) ⊆ 𝐼)
 
Theoremlidlrsppropdg 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‘𝐿)))
 
Theoremrnglidlmmgm 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)
 
Theoremrnglidlmsgrp 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)
 
Theoremrnglidlrng 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
 
Syntaxc2idl 13776 Ring two-sided ideal function.
class 2Ideal
 
Definitiondf-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𝑟))))
 
Theorem2idlvalg 13778 Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
𝐼 = (LIdeal‘𝑅)    &   𝑂 = (oppr𝑅)    &   𝐽 = (LIdeal‘𝑂)    &   𝑇 = (2Ideal‘𝑅)       (𝑅𝑉𝑇 = (𝐼𝐽))
 
Theorem2idlmex 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)
 
Theoremisridl 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‘𝑅) ∧ ∀𝑥𝐵𝑦𝐼 (𝑦 · 𝑥) ∈ 𝐼)))
 
Theorem2idlelb 13781 Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
𝐼 = (LIdeal‘𝑅)    &   𝑂 = (oppr𝑅)    &   𝐽 = (LIdeal‘𝑂)    &   𝑇 = (2Ideal‘𝑅)       (𝑈𝑇 ↔ (𝑈𝐼𝑈𝐽))
 
Theorem2idllidld 13782 A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
(𝜑𝐼 ∈ (2Ideal‘𝑅))       (𝜑𝐼 ∈ (LIdeal‘𝑅))
 
Theorem2idlridld 13783 A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
(𝜑𝐼 ∈ (2Ideal‘𝑅))    &   𝑂 = (oppr𝑅)       (𝜑𝐼 ∈ (LIdeal‘𝑂))
 
Theoremdf2idl2rng 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‘𝑅)) → (𝐼𝑈 ↔ ∀𝑥𝐵𝑦𝐼 ((𝑥 · 𝑦) ∈ 𝐼 ∧ (𝑦 · 𝑥) ∈ 𝐼)))
 
Theoremdf2idl2 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‘𝑅) ∧ ∀𝑥𝐵𝑦𝐼 ((𝑥 · 𝑦) ∈ 𝐼 ∧ (𝑦 · 𝑥) ∈ 𝐼))))
 
Theoremridl0 13786 Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
𝑈 = (LIdeal‘(oppr𝑅))    &    0 = (0g𝑅)       (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
 
Theoremridl1 13787 Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
𝑈 = (LIdeal‘(oppr𝑅))    &   𝐵 = (Base‘𝑅)       (𝑅 ∈ Ring → 𝐵𝑈)
 
Theorem2idl0 13788 Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
𝐼 = (2Ideal‘𝑅)    &    0 = (0g𝑅)       (𝑅 ∈ Ring → { 0 } ∈ 𝐼)
 
Theorem2idl1 13789 Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
𝐼 = (2Ideal‘𝑅)    &   𝐵 = (Base‘𝑅)       (𝑅 ∈ Ring → 𝐵𝐼)
 
Theorem2idlss 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‘𝑊)       (𝑈𝐼𝑈𝐵)
 
Theorem2idlbas 13791 The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
(𝜑𝐼 ∈ (2Ideal‘𝑅))    &   𝐽 = (𝑅s 𝐼)    &   𝐵 = (Base‘𝐽)       (𝜑𝐵 = 𝐼)
 
Theorem2idlelbas 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𝑅))))
 
Theoremrng2idlsubrng 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‘𝑅))
 
Theoremrng2idlnsg 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‘𝑅))
 
Theoremrng2idl0 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𝑅) ∈ 𝐼)
 
Theoremrng2idlsubgsubrng 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‘𝑅))
 
Theoremrng2idlsubgnsg 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‘𝑅))
 
Theoremrng2idlsubg0 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𝑅) ∈ 𝐼)
 
Theorem2idlcpblrng 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‘𝑅)) → ((𝐴𝐸𝐶𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))
 
Theorem2idlcpbl 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 ∧ 𝑆𝐼) → ((𝐴𝐸𝐶𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15230
  Copyright terms: Public domain < Previous  Next >