HomeHome Intuitionistic Logic Explorer
Theorem List (p. 137 of 152)
< 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 - 13601-13700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlspsnel 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 ∧ 𝑋 ∈ 𝑉) β†’ (π‘ˆ ∈ (π‘β€˜{𝑋}) ↔ βˆƒπ‘˜ ∈ 𝐾 π‘ˆ = (π‘˜ Β· 𝑋)))
 
Theoremlspsnvsi 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 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) β†’ (π‘β€˜{(𝑅 Β· 𝑋)}) βŠ† (π‘β€˜{𝑋}))
 
Theoremlspsnss2 13603* Comparable spans of singletons must have proportional vectors. (Contributed by NM, 7-Jun-2015.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜π‘†)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    β‡’   (πœ‘ β†’ ((π‘β€˜{𝑋}) βŠ† (π‘β€˜{π‘Œ}) ↔ βˆƒπ‘˜ ∈ 𝐾 𝑋 = (π‘˜ Β· π‘Œ)))
 
Theoremlspsnneg 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 ∧ 𝑋 ∈ 𝑉) β†’ (π‘β€˜{(π‘€β€˜π‘‹)}) = (π‘β€˜{𝑋}))
 
Theoremlspsnsub 13605 Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    β‡’   (πœ‘ β†’ (π‘β€˜{(𝑋 βˆ’ π‘Œ)}) = (π‘β€˜{(π‘Œ βˆ’ 𝑋)}))
 
Theoremlspsn0 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 })
 
Theoremlsp0 13607 Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.)
0 = (0gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   (π‘Š ∈ LMod β†’ (π‘β€˜βˆ…) = { 0 })
 
Theoremlspuni0 13608 Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.)
0 = (0gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   (π‘Š ∈ LMod β†’ βˆͺ (π‘β€˜βˆ…) = 0 )
 
Theoremlspun0 13609 The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    0 = (0gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 βŠ† 𝑉)    β‡’   (πœ‘ β†’ (π‘β€˜(𝑋 βˆͺ { 0 })) = (π‘β€˜π‘‹))
 
Theoremlspsneq0 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 ))
 
Theoremlspsneq0b 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 ))
 
Theoremlmodindp1 13612 Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    0 = (0gβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    &   (πœ‘ β†’ (π‘β€˜{𝑋}) β‰  (π‘β€˜{π‘Œ}))    β‡’   (πœ‘ β†’ (𝑋 + π‘Œ) β‰  0 )
 
Theoremlsslsp 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 ∧ π‘ˆ ∈ 𝐿 ∧ 𝐺 βŠ† π‘ˆ) β†’ (π‘β€˜πΊ) = (π‘€β€˜πΊ))
 
Theoremlss0v 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 )
 
Theoremlsspropdg 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β€˜πΏ))
 
Theoremlsppropd 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
 
Syntaxcsra 13617 Extend class notation with the subring algebra generator.
class subringAlg
 
Syntaxcrglmod 13618 Extend class notation with the left module induced by a ring over itself.
class ringLMod
 
Definitiondf-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β€˜π‘€)⟩)))
 
Definitiondf-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β€˜π‘€)))
 
Theoremsraval 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β€˜π‘Š)⟩))
 
Theoremsralemg 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)    β‡’   (πœ‘ β†’ (πΈβ€˜π‘Š) = (πΈβ€˜π΄))
 
Theoremsrabaseg 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β€˜π΄))
 
Theoremsraaddgg 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β€˜π΄))
 
Theoremsramulrg 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β€˜π΄))
 
Theoremsrascag 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β€˜π΄))
 
Theoremsravscag 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β€˜π‘Š) = ( ·𝑠 β€˜π΄))
 
Theoremsraipg 13628 The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.)
(πœ‘ β†’ 𝐴 = ((subringAlg β€˜π‘Š)β€˜π‘†))    &   (πœ‘ β†’ 𝑆 βŠ† (Baseβ€˜π‘Š))    &   (πœ‘ β†’ π‘Š ∈ 𝑋)    β‡’   (πœ‘ β†’ (.rβ€˜π‘Š) = (Β·π‘–β€˜π΄))
 
Theoremsratsetg 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β€˜π΄))
 
Theoremsraex 13630 Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.)
(πœ‘ β†’ 𝐴 = ((subringAlg β€˜π‘Š)β€˜π‘†))    &   (πœ‘ β†’ 𝑆 βŠ† (Baseβ€˜π‘Š))    &   (πœ‘ β†’ π‘Š ∈ 𝑋)    β‡’   (πœ‘ β†’ 𝐴 ∈ V)
 
Theoremsratopng 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β€˜π΄))
 
Theoremsradsg 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β€˜π΄))
 
Theoremsraring 13633 Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
𝐴 = ((subringAlg β€˜π‘…)β€˜π‘‰)    &   π΅ = (Baseβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝑉 βŠ† 𝐡) β†’ 𝐴 ∈ Ring)
 
Theoremsralmod 13634 The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
𝐴 = ((subringAlg β€˜π‘Š)β€˜π‘†)    β‡’   (𝑆 ∈ (SubRingβ€˜π‘Š) β†’ 𝐴 ∈ LMod)
 
Theoremsralmod0g 13635 The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014.)
(πœ‘ β†’ 𝐴 = ((subringAlg β€˜π‘Š)β€˜π‘†))    &   (πœ‘ β†’ 0 = (0gβ€˜π‘Š))    &   (πœ‘ β†’ 𝑆 βŠ† (Baseβ€˜π‘Š))    &   (πœ‘ β†’ π‘Š ∈ 𝑋)    β‡’   (πœ‘ β†’ 0 = (0gβ€˜π΄))
 
Theoremissubrgd 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β€˜πΌ))
 
Theoremrlmfn 13637 ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
ringLMod Fn V
 
Theoremrlmvalg 13638 Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(π‘Š ∈ 𝑉 β†’ (ringLModβ€˜π‘Š) = ((subringAlg β€˜π‘Š)β€˜(Baseβ€˜π‘Š)))
 
Theoremrlmbasg 13639 Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑅 ∈ 𝑉 β†’ (Baseβ€˜π‘…) = (Baseβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmplusgg 13640 Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑅 ∈ 𝑉 β†’ (+gβ€˜π‘…) = (+gβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlm0g 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β€˜π‘…)))
 
Theoremrlmsubg 13642 Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
(𝑅 ∈ 𝑉 β†’ (-gβ€˜π‘…) = (-gβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmmulrg 13643 Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
(𝑅 ∈ 𝑉 β†’ (.rβ€˜π‘…) = (.rβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmscabas 13644 Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.)
(𝑅 ∈ 𝑋 β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜(ringLModβ€˜π‘…))))
 
Theoremrlmvscag 13645 Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(𝑅 ∈ 𝑉 β†’ (.rβ€˜π‘…) = ( ·𝑠 β€˜(ringLModβ€˜π‘…)))
 
Theoremrlmtopng 13646 Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
(𝑅 ∈ 𝑉 β†’ (TopOpenβ€˜π‘…) = (TopOpenβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmdsg 13647 Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
(𝑅 ∈ 𝑉 β†’ (distβ€˜π‘…) = (distβ€˜(ringLModβ€˜π‘…)))
 
Theoremrlmlmod 13648 The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
(𝑅 ∈ Ring β†’ (ringLModβ€˜π‘…) ∈ LMod)
 
Theoremrlmvnegg 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β€˜π‘…)))
 
Theoremixpsnbasval 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
 
Syntaxclidl 13651 Ring left-ideal function.
class LIdeal
 
Syntaxcrsp 13652 Ring span function.
class RSpan
 
Definitiondf-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)
 
Definitiondf-rsp 13654 Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
RSpan = (LSpan ∘ ringLMod)
 
Theoremlidlvalg 13655 Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
(π‘Š ∈ 𝑉 β†’ (LIdealβ€˜π‘Š) = (LSubSpβ€˜(ringLModβ€˜π‘Š)))
 
Theoremrspvalg 13656 Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
(π‘Š ∈ 𝑉 β†’ (RSpanβ€˜π‘Š) = (LSpanβ€˜(ringLModβ€˜π‘Š)))
 
Theoremlidlex 13657 Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.)
(π‘Š ∈ 𝑉 β†’ (LIdealβ€˜π‘Š) ∈ V)
 
Theoremrspex 13658 Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
(π‘Š ∈ 𝑉 β†’ (RSpanβ€˜π‘Š) ∈ V)
 
Theoremlidlmex 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)
 
Theoremlidlss 13660 An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.)
𝐡 = (Baseβ€˜π‘Š)    &   πΌ = (LIdealβ€˜π‘Š)    β‡’   (π‘ˆ ∈ 𝐼 β†’ π‘ˆ βŠ† 𝐡)
 
Theoremlidlssbas 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β€˜π‘…))
 
Theoremlidlbas 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β€˜πΌ) = π‘ˆ)
 
Theoremislidlm 13663* Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &   π΅ = (Baseβ€˜π‘…)    &    + = (+gβ€˜π‘…)    &    Β· = (.rβ€˜π‘…)    β‡’   (𝐼 ∈ π‘ˆ ↔ (𝐼 βŠ† 𝐡 ∧ βˆƒπ‘— 𝑗 ∈ 𝐼 ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 𝐼 ((π‘₯ Β· π‘Ž) + 𝑏) ∈ 𝐼))
 
Theoremrnglidlmcl 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 ∈ 𝐼) ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐼)) β†’ (𝑋 Β· π‘Œ) ∈ 𝐼)
 
Theoremdflidl2rng 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β€˜π‘…)) β†’ (𝐼 ∈ π‘ˆ ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 (π‘₯ Β· 𝑦) ∈ 𝐼))
 
Theoremisridlrng 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β€˜π‘…)) β†’ (𝐼 ∈ π‘ˆ ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 (𝑦 Β· π‘₯) ∈ 𝐼))
 
Theoremlidl0cl 13667 An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &    0 = (0gβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝐼 ∈ π‘ˆ) β†’ 0 ∈ 𝐼)
 
Theoremlidlacl 13668 An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &    + = (+gβ€˜π‘…)    β‡’   (((𝑅 ∈ Ring ∧ 𝐼 ∈ π‘ˆ) ∧ (𝑋 ∈ 𝐼 ∧ π‘Œ ∈ 𝐼)) β†’ (𝑋 + π‘Œ) ∈ 𝐼)
 
Theoremlidlnegcl 13669 An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &   π‘ = (invgβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝐼 ∈ π‘ˆ ∧ 𝑋 ∈ 𝐼) β†’ (π‘β€˜π‘‹) ∈ 𝐼)
 
Theoremlidlsubg 13670 An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝐼 ∈ π‘ˆ) β†’ 𝐼 ∈ (SubGrpβ€˜π‘…))
 
Theoremlidlsubcl 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 ∧ 𝐼 ∈ π‘ˆ) ∧ (𝑋 ∈ 𝐼 ∧ π‘Œ ∈ 𝐼)) β†’ (𝑋 βˆ’ π‘Œ) ∈ 𝐼)
 
Theoremdflidl2 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β€˜π‘…) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 (π‘₯ Β· 𝑦) ∈ 𝐼)))
 
Theoremlidl0 13673 Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &    0 = (0gβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ { 0 } ∈ π‘ˆ)
 
Theoremlidl1 13674 Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
π‘ˆ = (LIdealβ€˜π‘…)    &   π΅ = (Baseβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ 𝐡 ∈ π‘ˆ)
 
Theoremrspcl 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 ∧ 𝐺 βŠ† 𝐡) β†’ (πΎβ€˜πΊ) ∈ π‘ˆ)
 
Theoremrspssid 13676 The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
𝐾 = (RSpanβ€˜π‘…)    &   π΅ = (Baseβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 𝐺 βŠ† 𝐡) β†’ 𝐺 βŠ† (πΎβ€˜πΊ))
 
Theoremrsp0 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 })
 
Theoremrspssp 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
 
Syntaxc2idl 13679 Ring two-sided ideal function.
class 2Ideal
 
Definitiondf-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β€˜π‘Ÿ))))
 
Theorem2idlvalg 13681 Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
𝐼 = (LIdealβ€˜π‘…)    &   π‘‚ = (opprβ€˜π‘…)    &   π½ = (LIdealβ€˜π‘‚)    &   π‘‡ = (2Idealβ€˜π‘…)    β‡’   (𝑅 ∈ 𝑉 β†’ 𝑇 = (𝐼 ∩ 𝐽))
 
Theorem2idlmex 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)
 
Theoremisridl 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β€˜π‘…) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 (𝑦 Β· π‘₯) ∈ 𝐼)))
 
Theorem2idlelb 13684 Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
𝐼 = (LIdealβ€˜π‘…)    &   π‘‚ = (opprβ€˜π‘…)    &   π½ = (LIdealβ€˜π‘‚)    &   π‘‡ = (2Idealβ€˜π‘…)    β‡’   (π‘ˆ ∈ 𝑇 ↔ (π‘ˆ ∈ 𝐼 ∧ π‘ˆ ∈ 𝐽))
 
Theorem2idllidld 13685 A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
(πœ‘ β†’ 𝐼 ∈ (2Idealβ€˜π‘…))    β‡’   (πœ‘ β†’ 𝐼 ∈ (LIdealβ€˜π‘…))
 
Theorem2idlridld 13686 A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
(πœ‘ β†’ 𝐼 ∈ (2Idealβ€˜π‘…))    &   π‘‚ = (opprβ€˜π‘…)    β‡’   (πœ‘ β†’ 𝐼 ∈ (LIdealβ€˜π‘‚))
 
Theoremdf2idl2rng 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β€˜π‘…)) β†’ (𝐼 ∈ π‘ˆ ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 ((π‘₯ Β· 𝑦) ∈ 𝐼 ∧ (𝑦 Β· π‘₯) ∈ 𝐼)))
 
Theoremdf2idl2 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β€˜π‘…) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐼 ((π‘₯ Β· 𝑦) ∈ 𝐼 ∧ (𝑦 Β· π‘₯) ∈ 𝐼))))
 
Theoremridl0 13689 Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
π‘ˆ = (LIdealβ€˜(opprβ€˜π‘…))    &    0 = (0gβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ { 0 } ∈ π‘ˆ)
 
Theoremridl1 13690 Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
π‘ˆ = (LIdealβ€˜(opprβ€˜π‘…))    &   π΅ = (Baseβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ 𝐡 ∈ π‘ˆ)
 
Theorem2idl0 13691 Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
𝐼 = (2Idealβ€˜π‘…)    &    0 = (0gβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ { 0 } ∈ 𝐼)
 
Theorem2idl1 13692 Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
𝐼 = (2Idealβ€˜π‘…)    &   π΅ = (Baseβ€˜π‘…)    β‡’   (𝑅 ∈ Ring β†’ 𝐡 ∈ 𝐼)
 
Theorem2idlss 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β€˜π‘Š)    β‡’   (π‘ˆ ∈ 𝐼 β†’ π‘ˆ βŠ† 𝐡)
 
Theorem2idlbas 13694 The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
(πœ‘ β†’ 𝐼 ∈ (2Idealβ€˜π‘…))    &   π½ = (𝑅 β†Ύs 𝐼)    &   π΅ = (Baseβ€˜π½)    β‡’   (πœ‘ β†’ 𝐡 = 𝐼)
 
Theorem2idlelbas 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
 
Syntaxcpsmet 13696 Extend class notation with the class of all pseudometric spaces.
class PsMet
 
Syntaxcxmet 13697 Extend class notation with the class of all extended metric spaces.
class ∞Met
 
Syntaxcmet 13698 Extend class notation with the class of all metrics.
class Met
 
Syntaxcbl 13699 Extend class notation with the metric space ball function.
class ball
 
Syntaxcfbas 13700 Extend class definition to include the class of filter bases.
class fBas
    < 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-15104
  Copyright terms: Public domain < Previous  Next >