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
 
Theoremlspsnel 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 ∧ 𝑋 ∈ 𝑉) β†’ (π‘ˆ ∈ (π‘β€˜{𝑋}) ↔ βˆƒπ‘˜ ∈ 𝐾 π‘ˆ = (π‘˜ Β· 𝑋)))
 
Theoremlspsnvsi 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 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) β†’ (π‘β€˜{(𝑅 Β· 𝑋)}) βŠ† (π‘β€˜{𝑋}))
 
Theoremlspsnss2 13703* Comparable spans of singletons must have proportional vectors. (Contributed by NM, 7-Jun-2015.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜π‘†)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    β‡’   (πœ‘ β†’ ((π‘β€˜{𝑋}) βŠ† (π‘β€˜{π‘Œ}) ↔ βˆƒπ‘˜ ∈ 𝐾 𝑋 = (π‘˜ Β· π‘Œ)))
 
Theoremlspsnneg 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 ∧ 𝑋 ∈ 𝑉) β†’ (π‘β€˜{(π‘€β€˜π‘‹)}) = (π‘β€˜{𝑋}))
 
Theoremlspsnsub 13705 Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    β‡’   (πœ‘ β†’ (π‘β€˜{(𝑋 βˆ’ π‘Œ)}) = (π‘β€˜{(π‘Œ βˆ’ 𝑋)}))
 
Theoremlspsn0 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 })
 
Theoremlsp0 13707 Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.)
0 = (0gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   (π‘Š ∈ LMod β†’ (π‘β€˜βˆ…) = { 0 })
 
Theoremlspuni0 13708 Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.)
0 = (0gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   (π‘Š ∈ LMod β†’ βˆͺ (π‘β€˜βˆ…) = 0 )
 
Theoremlspun0 13709 The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    0 = (0gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 βŠ† 𝑉)    β‡’   (πœ‘ β†’ (π‘β€˜(𝑋 βˆͺ { 0 })) = (π‘β€˜π‘‹))
 
Theoremlspsneq0 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 ))
 
Theoremlspsneq0b 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 ))
 
Theoremlmodindp1 13712 Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    0 = (0gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    &   (πœ‘ β†’ (π‘β€˜{𝑋}) β‰  (π‘β€˜{π‘Œ}))    β‡’   (πœ‘ β†’ (𝑋 + π‘Œ) β‰  0 )
 
Theoremlsslsp 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 ∧ π‘ˆ ∈ 𝐿 ∧ 𝐺 βŠ† π‘ˆ) β†’ (π‘β€˜πΊ) = (π‘€β€˜πΊ))
 
Theoremlss0v 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 )
 
Theoremlsspropdg 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β€˜πΏ))
 
Theoremlsppropd 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
 
Syntaxcsra 13717 Extend class notation with the subring algebra generator.
class subringAlg
 
Syntaxcrglmod 13718 Extend class notation with the left module induced by a ring over itself.
class ringLMod
 
Definitiondf-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β€˜π‘€)⟩)))
 
Definitiondf-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β€˜π‘€)))
 
Theoremsraval 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β€˜π‘Š)⟩))
 
Theoremsralemg 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)    β‡’   (πœ‘ β†’ (πΈβ€˜π‘Š) = (πΈβ€˜π΄))
 
Theoremsrabaseg 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β€˜π΄))
 
Theoremsraaddgg 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β€˜π΄))
 
Theoremsramulrg 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β€˜π΄))
 
Theoremsrascag 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β€˜π΄))
 
Theoremsravscag 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β€˜π‘Š) = ( ·𝑠 β€˜π΄))
 
Theoremsraipg 13728 The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.)
(πœ‘ β†’ 𝐴 = ((subringAlg β€˜π‘Š)β€˜π‘†))    &   (πœ‘ β†’ 𝑆 βŠ† (Baseβ€˜π‘Š))    &   (πœ‘ β†’ π‘Š ∈ 𝑋)    β‡’   (πœ‘ β†’ (.rβ€˜π‘Š) = (Β·π‘–β€˜π΄))
 
Theoremsratsetg 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β€˜π΄))
 
Theoremsraex 13730 Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.)
(πœ‘ β†’ 𝐴 = ((subringAlg β€˜π‘Š)β€˜π‘†))    &   (πœ‘ β†’ 𝑆 βŠ† (Baseβ€˜π‘Š))    &   (πœ‘ β†’ π‘Š ∈ 𝑋)    β‡’   (πœ‘ β†’ 𝐴 ∈ V)
 
Theoremsratopng 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β€˜π΄))
 
Theoremsradsg 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β€˜π΄))
 
Theoremsraring 13733 Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
𝐴 = ((subringAlg β€˜π‘…)β€˜π‘‰)    &   π΅ = (Baseβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝑉 βŠ† 𝐡) β†’ 𝐴 ∈ Ring)
 
Theoremsralmod 13734 The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
𝐴 = ((subringAlg β€˜π‘Š)β€˜π‘†)    β‡’   (𝑆 ∈ (SubRingβ€˜π‘Š) β†’ 𝐴 ∈ LMod)
 
Theoremsralmod0g 13735 The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014.)
(πœ‘ β†’ 𝐴 = ((subringAlg β€˜π‘Š)β€˜π‘†))    &   (πœ‘ β†’ 0 = (0gβ€˜π‘Š))    &   (πœ‘ β†’ 𝑆 βŠ† (Baseβ€˜π‘Š))    &   (πœ‘ β†’ π‘Š ∈ 𝑋)    β‡’   (πœ‘ β†’ 0 = (0gβ€˜π΄))
 
Theoremissubrgd 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β€˜πΌ))
 
Theoremrlmfn 13737 ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
ringLMod Fn V
 
Theoremrlmvalg 13738 Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(π‘Š ∈ 𝑉 β†’ (ringLModβ€˜π‘Š) = ((subringAlg β€˜π‘Š)β€˜(Baseβ€˜π‘Š)))
 
Theoremrlmbasg 13739 Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑅 ∈ 𝑉 β†’ (Baseβ€˜π‘…) = (Baseβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmplusgg 13740 Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑅 ∈ 𝑉 β†’ (+gβ€˜π‘…) = (+gβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlm0g 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β€˜π‘…)))
 
Theoremrlmsubg 13742 Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
(𝑅 ∈ 𝑉 β†’ (-gβ€˜π‘…) = (-gβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmmulrg 13743 Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
(𝑅 ∈ 𝑉 β†’ (.rβ€˜π‘…) = (.rβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmscabas 13744 Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.)
(𝑅 ∈ 𝑋 β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜(ringLModβ€˜π‘…))))
 
Theoremrlmvscag 13745 Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑅 ∈ 𝑉 β†’ (.rβ€˜π‘…) = ( ·𝑠 β€˜(ringLModβ€˜π‘…)))
 
Theoremrlmtopng 13746 Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
(𝑅 ∈ 𝑉 β†’ (TopOpenβ€˜π‘…) = (TopOpenβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmdsg 13747 Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
(𝑅 ∈ 𝑉 β†’ (distβ€˜π‘…) = (distβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmlmod 13748 The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
(𝑅 ∈ Ring β†’ (ringLModβ€˜π‘…) ∈ LMod)
 
Theoremrlmvnegg 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β€˜π‘…)))
 
Theoremixpsnbasval 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
 
Syntaxclidl 13751 Ring left-ideal function.
class LIdeal
 
Syntaxcrsp 13752 Ring span function.
class RSpan
 
Definitiondf-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)
 
Definitiondf-rsp 13754 Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
RSpan = (LSpan ∘ ringLMod)
 
Theoremlidlvalg 13755 Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(π‘Š ∈ 𝑉 β†’ (LIdealβ€˜π‘Š) = (LSubSpβ€˜(ringLModβ€˜π‘Š)))
 
Theoremrspvalg 13756 Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
(π‘Š ∈ 𝑉 β†’ (RSpanβ€˜π‘Š) = (LSpanβ€˜(ringLModβ€˜π‘Š)))
 
Theoremlidlex 13757 Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.)
(π‘Š ∈ 𝑉 β†’ (LIdealβ€˜π‘Š) ∈ V)
 
Theoremrspex 13758 Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
(π‘Š ∈ 𝑉 β†’ (RSpanβ€˜π‘Š) ∈ V)
 
Theoremlidlmex 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)
 
Theoremlidlss 13760 An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.)
𝐡 = (Baseβ€˜π‘Š)    &   πΌ = (LIdealβ€˜π‘Š)    β‡’   (π‘ˆ ∈ 𝐼 β†’ π‘ˆ βŠ† 𝐡)
 
Theoremlidlssbas 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β€˜π‘…))
 
Theoremlidlbas 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β€˜πΌ) = π‘ˆ)
 
Theoremislidlm 13763* Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &   π΅ = (Baseβ€˜π‘…)    &    + = (+gβ€˜π‘…)    &    Β· = (.rβ€˜π‘…)    β‡’   (𝐼 ∈ π‘ˆ ↔ (𝐼 βŠ† 𝐡 ∧ βˆƒπ‘— 𝑗 ∈ 𝐼 ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 𝐼 ((π‘₯ Β· π‘Ž) + 𝑏) ∈ 𝐼))
 
Theoremrnglidlmcl 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 ∈ 𝐼) ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐼)) β†’ (𝑋 Β· π‘Œ) ∈ 𝐼)
 
Theoremdflidl2rng 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β€˜π‘…)) β†’ (𝐼 ∈ π‘ˆ ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 (π‘₯ Β· 𝑦) ∈ 𝐼))
 
Theoremisridlrng 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β€˜π‘…)) β†’ (𝐼 ∈ π‘ˆ ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 (𝑦 Β· π‘₯) ∈ 𝐼))
 
Theoremlidl0cl 13767 An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &    0 = (0gβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝐼 ∈ π‘ˆ) β†’ 0 ∈ 𝐼)
 
Theoremlidlacl 13768 An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &    + = (+gβ€˜π‘…)    β‡’   (((𝑅 ∈ Ring ∧ 𝐼 ∈ π‘ˆ) ∧ (𝑋 ∈ 𝐼 ∧ π‘Œ ∈ 𝐼)) β†’ (𝑋 + π‘Œ) ∈ 𝐼)
 
Theoremlidlnegcl 13769 An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &   π‘ = (invgβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝐼 ∈ π‘ˆ ∧ 𝑋 ∈ 𝐼) β†’ (π‘β€˜π‘‹) ∈ 𝐼)
 
Theoremlidlsubg 13770 An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝐼 ∈ π‘ˆ) β†’ 𝐼 ∈ (SubGrpβ€˜π‘…))
 
Theoremlidlsubcl 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 ∧ 𝐼 ∈ π‘ˆ) ∧ (𝑋 ∈ 𝐼 ∧ π‘Œ ∈ 𝐼)) β†’ (𝑋 βˆ’ π‘Œ) ∈ 𝐼)
 
Theoremdflidl2 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β€˜π‘…) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 (π‘₯ Β· 𝑦) ∈ 𝐼)))
 
Theoremlidl0 13773 Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &    0 = (0gβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ { 0 } ∈ π‘ˆ)
 
Theoremlidl1 13774 Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &   π΅ = (Baseβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ 𝐡 ∈ π‘ˆ)
 
Theoremrspcl 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 ∧ 𝐺 βŠ† 𝐡) β†’ (πΎβ€˜πΊ) ∈ π‘ˆ)
 
Theoremrspssid 13776 The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
𝐾 = (RSpanβ€˜π‘…)    &   π΅ = (Baseβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝐺 βŠ† 𝐡) β†’ 𝐺 βŠ† (πΎβ€˜πΊ))
 
Theoremrsp0 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 })
 
Theoremrspssp 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 ∧ 𝐼 ∈ π‘ˆ ∧ 𝐺 βŠ† 𝐼) β†’ (πΎβ€˜πΊ) βŠ† 𝐼)
 
Theoremlidlrsppropdg 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β€˜πΏ)))
 
Theoremrnglidlmmgm 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)
 
Theoremrnglidlmsgrp 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)
 
Theoremrnglidlrng 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
 
Syntaxc2idl 13783 Ring two-sided ideal function.
class 2Ideal
 
Definitiondf-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β€˜π‘Ÿ))))
 
Theorem2idlvalg 13785 Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
𝐼 = (LIdealβ€˜π‘…)    &   π‘‚ = (opprβ€˜π‘…)    &   π½ = (LIdealβ€˜π‘‚)    &   π‘‡ = (2Idealβ€˜π‘…)    β‡’   (𝑅 ∈ 𝑉 β†’ 𝑇 = (𝐼 ∩ 𝐽))
 
Theorem2idlmex 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)
 
Theoremisridl 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β€˜π‘…) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 (𝑦 Β· π‘₯) ∈ 𝐼)))
 
Theorem2idlelb 13788 Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
𝐼 = (LIdealβ€˜π‘…)    &   π‘‚ = (opprβ€˜π‘…)    &   π½ = (LIdealβ€˜π‘‚)    &   π‘‡ = (2Idealβ€˜π‘…)    β‡’   (π‘ˆ ∈ 𝑇 ↔ (π‘ˆ ∈ 𝐼 ∧ π‘ˆ ∈ 𝐽))
 
Theorem2idllidld 13789 A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
(πœ‘ β†’ 𝐼 ∈ (2Idealβ€˜π‘…))    β‡’   (πœ‘ β†’ 𝐼 ∈ (LIdealβ€˜π‘…))
 
Theorem2idlridld 13790 A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
(πœ‘ β†’ 𝐼 ∈ (2Idealβ€˜π‘…))    &   π‘‚ = (opprβ€˜π‘…)    β‡’   (πœ‘ β†’ 𝐼 ∈ (LIdealβ€˜π‘‚))
 
Theoremdf2idl2rng 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β€˜π‘…)) β†’ (𝐼 ∈ π‘ˆ ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 ((π‘₯ Β· 𝑦) ∈ 𝐼 ∧ (𝑦 Β· π‘₯) ∈ 𝐼)))
 
Theoremdf2idl2 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β€˜π‘…) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 ((π‘₯ Β· 𝑦) ∈ 𝐼 ∧ (𝑦 Β· π‘₯) ∈ 𝐼))))
 
Theoremridl0 13793 Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
π‘ˆ = (LIdealβ€˜(opprβ€˜π‘…))    &    0 = (0gβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ { 0 } ∈ π‘ˆ)
 
Theoremridl1 13794 Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
π‘ˆ = (LIdealβ€˜(opprβ€˜π‘…))    &   π΅ = (Baseβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ 𝐡 ∈ π‘ˆ)
 
Theorem2idl0 13795 Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
𝐼 = (2Idealβ€˜π‘…)    &    0 = (0gβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ { 0 } ∈ 𝐼)
 
Theorem2idl1 13796 Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
𝐼 = (2Idealβ€˜π‘…)    &   π΅ = (Baseβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ 𝐡 ∈ 𝐼)
 
Theorem2idlss 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β€˜π‘Š)    β‡’   (π‘ˆ ∈ 𝐼 β†’ π‘ˆ βŠ† 𝐡)
 
Theorem2idlbas 13798 The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
(πœ‘ β†’ 𝐼 ∈ (2Idealβ€˜π‘…))    &   π½ = (𝑅 β†Ύs 𝐼)    &   π΅ = (Baseβ€˜π½)    β‡’   (πœ‘ β†’ 𝐡 = 𝐼)
 
Theorem2idlelbas 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β€˜π‘…))))
 
Theoremrng2idlsubrng 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β€˜π‘…))
    < 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-15237
  Copyright terms: Public domain < Previous  Next >