HomeHome Intuitionistic Logic Explorer
Theorem List (p. 130 of 145)
< 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 - 12901-13000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmulgnn0dir 12901 Sum of group multiples, generalized to 0. (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑋𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
 
Theoremmulgdirlem 12902 Lemma for mulgdir 12903. (Contributed by Mario Carneiro, 13-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
 
Theoremmulgdir 12903 Sum of group multiples, generalized to . (Contributed by Mario Carneiro, 13-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
 
Theoremmulgp1 12904 Group multiple (exponentiation) operation at a successor, extended to . (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋))
 
Theoremmulgneg2 12905 Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 13-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &   𝐼 = (invg𝐺)       ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵) → (-𝑁 · 𝑋) = (𝑁 · (𝐼𝑋)))
 
Theoremmulgnnass 12906 Product of group multiples, for positive multiples in a semigroup. (Contributed by Mario Carneiro, 13-Dec-2014.) (Revised by AV, 29-Aug-2021.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)       ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
 
Theoremmulgnn0ass 12907 Product of group multiples, generalized to 0. (Contributed by Mario Carneiro, 13-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)       ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑋𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
 
Theoremmulgass 12908 Product of group multiples, generalized to . (Contributed by Mario Carneiro, 13-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)       ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
 
Theoremmulgassr 12909 Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)       ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵)) → ((𝑁 · 𝑀) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
 
Theoremmulgmodid 12910 Casting out multiples of the identity element leaves the group multiple unchanged. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &    · = (.g𝐺)       ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 mod 𝑀) · 𝑋) = (𝑁 · 𝑋))
 
Theoremmulgsubdir 12911 Distribution of group multiples over subtraction for group elements, subdir 8333 analog. (Contributed by Mario Carneiro, 13-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵)) → ((𝑀𝑁) · 𝑋) = ((𝑀 · 𝑋) (𝑁 · 𝑋)))
 
Theoremmhmmulg 12912 A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    × = (.g𝐻)       ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑁 ∈ ℕ0𝑋𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹𝑋)))
 
Theoremmulgpropdg 12913* Two structures with the same group-nature have the same group multiple function. 𝐾 is expected to either be V (when strong equality is available) or 𝐵 (when closure is available). (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
(𝜑· = (.g𝐺))    &   (𝜑× = (.g𝐻))    &   (𝜑𝐺𝑉)    &   (𝜑𝐻𝑊)    &   (𝜑𝐵 = (Base‘𝐺))    &   (𝜑𝐵 = (Base‘𝐻))    &   (𝜑𝐵𝐾)    &   ((𝜑 ∧ (𝑥𝐾𝑦𝐾)) → (𝑥(+g𝐺)𝑦) ∈ 𝐾)    &   ((𝜑 ∧ (𝑥𝐾𝑦𝐾)) → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝐻)𝑦))       (𝜑· = × )
 
Theoremsubmmulgcl 12914 Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015.)
= (.g𝐺)       ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0𝑋𝑆) → (𝑁 𝑋) ∈ 𝑆)
 
7.2.3  Abelian groups
 
7.2.3.1  Definition and basic properties
 
Syntaxccmn 12915 Extend class notation with class of all commutative monoids.
class CMnd
 
Syntaxcabl 12916 Extend class notation with class of all Abelian groups.
class Abel
 
Definitiondf-cmn 12917* Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g𝑔)𝑏) = (𝑏(+g𝑔)𝑎)}
 
Definitiondf-abl 12918 Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
Abel = (Grp ∩ CMnd)
 
Theoremisabl 12919 The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.)
(𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
 
Theoremablgrp 12920 An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
(𝐺 ∈ Abel → 𝐺 ∈ Grp)
 
Theoremablgrpd 12921 An Abelian group is a group, deduction form of ablgrp 12920. (Contributed by Rohan Ridenour, 3-Aug-2023.)
(𝜑𝐺 ∈ Abel)       (𝜑𝐺 ∈ Grp)
 
Theoremablcmn 12922 An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
(𝐺 ∈ Abel → 𝐺 ∈ CMnd)
 
Theoremiscmn 12923* The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)       (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
 
Theoremisabl2 12924* The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)       (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
 
Theoremcmnpropd 12925* If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.)
(𝜑𝐵 = (Base‘𝐾))    &   (𝜑𝐵 = (Base‘𝐿))    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))       (𝜑 → (𝐾 ∈ CMnd ↔ 𝐿 ∈ CMnd))
 
Theoremablpropd 12926* If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014.)
(𝜑𝐵 = (Base‘𝐾))    &   (𝜑𝐵 = (Base‘𝐿))    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))       (𝜑 → (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel))
 
Theoremablprop 12927 If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013.)
(Base‘𝐾) = (Base‘𝐿)    &   (+g𝐾) = (+g𝐿)       (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel)
 
Theoremiscmnd 12928* Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
(𝜑𝐵 = (Base‘𝐺))    &   (𝜑+ = (+g𝐺))    &   (𝜑𝐺 ∈ Mnd)    &   ((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥))       (𝜑𝐺 ∈ CMnd)
 
Theoremisabld 12929* Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.)
(𝜑𝐵 = (Base‘𝐺))    &   (𝜑+ = (+g𝐺))    &   (𝜑𝐺 ∈ Grp)    &   ((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥))       (𝜑𝐺 ∈ Abel)
 
Theoremisabli 12930* Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.)
𝐺 ∈ Grp    &   𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &   ((𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥))       𝐺 ∈ Abel
 
Theoremcmnmnd 12931 A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
(𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
 
Theoremcmncom 12932 A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ CMnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
 
Theoremablcom 12933 An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ Abel ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
 
Theoremcmn32 12934 Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ CMnd ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
 
Theoremcmn4 12935 Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ CMnd ∧ (𝑋𝐵𝑌𝐵) ∧ (𝑍𝐵𝑊𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
 
Theoremcmn12 12936 Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ CMnd ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍)))
 
Theoremabl32 12937 Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)    &   (𝜑𝑍𝐵)       (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
 
Theoremcmnmndd 12938 A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.)
(𝜑𝐺 ∈ CMnd)       (𝜑𝐺 ∈ Mnd)
 
Theoremrinvmod 12939* Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovimo 6062. (Contributed by AV, 31-Dec-2023.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &    + = (+g𝐺)    &   (𝜑𝐺 ∈ CMnd)    &   (𝜑𝐴𝐵)       (𝜑 → ∃*𝑤𝐵 (𝐴 + 𝑤) = 0 )
 
Theoremablinvadd 12940 The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &   𝑁 = (invg𝐺)       ((𝐺 ∈ Abel ∧ 𝑋𝐵𝑌𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁𝑋) + (𝑁𝑌)))
 
Theoremablsub2inv 12941 Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)    &   𝑁 = (invg𝐺)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)       (𝜑 → ((𝑁𝑋) (𝑁𝑌)) = (𝑌 𝑋))
 
Theoremablsubadd 12942 Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Abel ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) = 𝑍 ↔ (𝑌 + 𝑍) = 𝑋))
 
Theoremablsub4 12943 Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Abel ∧ (𝑋𝐵𝑌𝐵) ∧ (𝑍𝐵𝑊𝐵)) → ((𝑋 + 𝑌) (𝑍 + 𝑊)) = ((𝑋 𝑍) + (𝑌 𝑊)))
 
Theoremabladdsub4 12944 Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Abel ∧ (𝑋𝐵𝑌𝐵) ∧ (𝑍𝐵𝑊𝐵)) → ((𝑋 + 𝑌) = (𝑍 + 𝑊) ↔ (𝑋 𝑍) = (𝑊 𝑌)))
 
Theoremabladdsub 12945 Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Abel ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) 𝑍) = ((𝑋 𝑍) + 𝑌))
 
Theoremablpncan2 12946 Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Abel ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 + 𝑌) 𝑋) = 𝑌)
 
Theoremablpncan3 12947 A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Abel ∧ (𝑋𝐵𝑌𝐵)) → (𝑋 + (𝑌 𝑋)) = 𝑌)
 
Theoremablsubsub 12948 Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)    &   (𝜑𝑍𝐵)       (𝜑 → (𝑋 (𝑌 𝑍)) = ((𝑋 𝑌) + 𝑍))
 
Theoremablsubsub4 12949 Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)    &   (𝜑𝑍𝐵)       (𝜑 → ((𝑋 𝑌) 𝑍) = (𝑋 (𝑌 + 𝑍)))
 
Theoremablpnpcan 12950 Cancellation law for mixed addition and subtraction. (pnpcan 8186 analog.) (Contributed by NM, 29-May-2015.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)    &   (𝜑𝑍𝐵)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)    &   (𝜑𝑍𝐵)       (𝜑 → ((𝑋 + 𝑌) (𝑋 + 𝑍)) = (𝑌 𝑍))
 
Theoremablnncan 12951 Cancellation law for group subtraction. (nncan 8176 analog.) (Contributed by NM, 7-Apr-2015.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)       (𝜑 → (𝑋 (𝑋 𝑌)) = 𝑌)
 
Theoremablsub32 12952 Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)    &   (𝜑𝑍𝐵)       (𝜑 → ((𝑋 𝑌) 𝑍) = ((𝑋 𝑍) 𝑌))
 
Theoremablnnncan 12953 Cancellation law for group subtraction. (nnncan 8182 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)    &   (𝜑𝑍𝐵)       (𝜑 → ((𝑋 (𝑌 𝑍)) 𝑍) = (𝑋 𝑌))
 
Theoremablnnncan1 12954 Cancellation law for group subtraction. (nnncan1 8183 analog.) (Contributed by NM, 7-Apr-2015.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)    &   (𝜑𝐺 ∈ Abel)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)    &   (𝜑𝑍𝐵)       (𝜑 → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑍 𝑌))
 
Theoremablsubsub23 12955 Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.)
𝑉 = (Base‘𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Abel ∧ (𝐴𝑉𝐵𝑉𝐶𝑉)) → ((𝐴 𝐵) = 𝐶 ↔ (𝐴 𝐶) = 𝐵))
 
Theoremsubcmnd 12956 A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.)
(𝜑𝐻 = (𝐺s 𝑆))    &   (𝜑𝐺 ∈ CMnd)    &   (𝜑𝐻 ∈ Mnd)    &   (𝜑𝑆𝑉)       (𝜑𝐻 ∈ CMnd)
 
7.3  Rings
 
7.3.1  Multiplicative Group
 
Syntaxcmgp 12957 Multiplicative group.
class mulGrp
 
Definitiondf-mgp 12958 Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and we get a group if we restrict to the elements that have inverses. This allows us to formalize such notions as "the multiplication operation of a ring is a monoid" or "the multiplicative identity" in terms of the identity of a monoid (df-ur 12969). (Contributed by Mario Carneiro, 21-Dec-2014.)
mulGrp = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(+g‘ndx), (.r𝑤)⟩))
 
Theoremfnmgp 12959 The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
mulGrp Fn V
 
Theoremmgpvalg 12960 Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.)
𝑀 = (mulGrp‘𝑅)    &    · = (.r𝑅)       (𝑅𝑉𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩))
 
Theoremmgpplusgg 12961 Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.)
𝑀 = (mulGrp‘𝑅)    &    · = (.r𝑅)       (𝑅𝑉· = (+g𝑀))
 
Theoremmgpex 12962 Existence of the multiplication group. If 𝑅 is known to be a semiring, see srgmgp 12977. (Contributed by Jim Kingdon, 10-Jan-2025.)
𝑀 = (mulGrp‘𝑅)       (𝑅𝑉𝑀 ∈ V)
 
Theoremmgpbasg 12963 Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
𝑀 = (mulGrp‘𝑅)    &   𝐵 = (Base‘𝑅)       (𝑅𝑉𝐵 = (Base‘𝑀))
 
Theoremmgpscag 12964 The multiplication monoid has the same (if any) scalars as the original ring. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.)
𝑀 = (mulGrp‘𝑅)    &   𝑆 = (Scalar‘𝑅)       (𝑅𝑉𝑆 = (Scalar‘𝑀))
 
Theoremmgptsetg 12965 Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
𝑀 = (mulGrp‘𝑅)       (𝑅𝑉 → (TopSet‘𝑅) = (TopSet‘𝑀))
 
Theoremmgptopng 12966 Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
𝑀 = (mulGrp‘𝑅)    &   𝐽 = (TopOpen‘𝑅)       (𝑅𝑉𝐽 = (TopOpen‘𝑀))
 
Theoremmgpdsg 12967 Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
𝑀 = (mulGrp‘𝑅)    &   𝐵 = (dist‘𝑅)       (𝑅𝑉𝐵 = (dist‘𝑀))
 
7.3.2  Ring unity (multiplicative identity)

In Wikipedia "Identity element", see https://en.wikipedia.org/wiki/Identity_element (18-Jan-2025): "... an identity with respect to multiplication is called a multiplicative identity (often denoted as 1). ... The distinction between additive and multiplicative identity is used most often for sets that support both binary operations, such as rings, integral domains, and fields. The multiplicative identity is often called unity in the latter context (a ring with unity). This should not be confused with a unit in ring theory, which is any element having a multiplicative inverse. By its own definition, unity itself is necessarily a unit."

Calling the multiplicative identity of a ring a unity is taken from the definition of a ring with unity in section 17.3 of [BeauregardFraleigh] p. 135, "A ring ( R , + , . ) is a ring with unity if R is not the zero ring and ( R , . ) is a monoid. In this case, the identity element of ( R , . ) is denoted by 1 and is called the unity of R." This definition of a "ring with unity" corresponds to our definition of a unital ring (see df-ring 13007).

Some authors call the multiplicative identity "unit" or "unit element" (for example in section I, 2.2 of [BourbakiAlg1] p. 14, definition in section 1.3 of [Hall] p. 4, or in section I, 1 of [Lang] p. 3), whereas other authors use the term "unit" for an element having a multiplicative inverse (for example in section 17.3 of [BeauregardFraleigh] p. 135, in definition in [Roman] p. 26, or even in section II, 1 of [Lang] p. 84). Sometimes, the multiplicative identity is simply called "one" (see, for example, chapter 8 in [Schechter] p. 180).

To avoid this ambiguity of the term "unit", also mentioned in Wikipedia, we call the multiplicative identity of a structure with a multiplication (usually a ring) a "ring unity", or straightly "multiplicative identity".

The term "unit" will be used for an element having a multiplicative inverse (see https://us.metamath.org/mpeuni/df-unit.html 13007 in set.mm), and we have "the ring unity is a unit", see https://us.metamath.org/mpeuni/1unit.html 13007.

 
Syntaxcur 12968 Extend class notation with ring unity.
class 1r
 
Definitiondf-ur 12969 Define the multiplicative identity, i.e., the monoid identity (df-0g 12655) of the multiplicative monoid (df-mgp 12958) of a ring-like structure. This multiplicative identity is also called "ring unity" or "unity element".

This definition works by transferring the multiplicative operation from the .r slot to the +g slot and then looking at the element which is then the 0g element, that is an identity with respect to the operation which started out in the .r slot.

See also dfur2g 12971, which derives the "traditional" definition as the unique element of a ring which is left- and right-neutral under multiplication. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)

1r = (0g ∘ mulGrp)
 
Theoremringidvalg 12970 The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
𝐺 = (mulGrp‘𝑅)    &    1 = (1r𝑅)       (𝑅𝑉1 = (0g𝐺))
 
Theoremdfur2g 12971* The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)    &    1 = (1r𝑅)       (𝑅𝑉1 = (℩𝑒(𝑒𝐵 ∧ ∀𝑥𝐵 ((𝑒 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑒) = 𝑥))))
 
7.3.3  Semirings
 
Syntaxcsrg 12972 Extend class notation with the class of all semirings.
class SRing
 
Definitiondf-srg 12973* Define class of all semirings. A semiring is a set equipped with two everywhere-defined internal operations, whose first one is an additive commutative monoid structure and the second one is a multiplicative monoid structure, and where multiplication is (left- and right-) distributive over addition. Like with rings, the additive identity is an absorbing element of the multiplicative law, but in the case of semirings, this has to be part of the definition, as it cannot be deduced from distributivity alone. Definition of [Golan] p. 1. Note that our semirings are unital. Such semirings are sometimes called "rigs", being "rings without negatives". (Contributed by Thierry Arnoux, 21-Mar-2018.)
SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
 
Theoremissrg 12974* The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018.)
𝐵 = (Base‘𝑅)    &   𝐺 = (mulGrp‘𝑅)    &    + = (+g𝑅)    &    · = (.r𝑅)    &    0 = (0g𝑅)       (𝑅 ∈ SRing ↔ (𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀𝑥𝐵 (∀𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 ))))
 
Theoremsrgcmn 12975 A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
(𝑅 ∈ SRing → 𝑅 ∈ CMnd)
 
Theoremsrgmnd 12976 A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
(𝑅 ∈ SRing → 𝑅 ∈ Mnd)
 
Theoremsrgmgp 12977 A semiring is a monoid under multiplication. (Contributed by Thierry Arnoux, 21-Mar-2018.)
𝐺 = (mulGrp‘𝑅)       (𝑅 ∈ SRing → 𝐺 ∈ Mnd)
 
Theoremsrgdilem 12978 Lemma for srgdi 12983 and srgdir 12984. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    + = (+g𝑅)    &    · = (.r𝑅)       ((𝑅 ∈ SRing ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))))
 
Theoremsrgcl 12979 Closure of the multiplication operation of a semiring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)       ((𝑅 ∈ SRing ∧ 𝑋𝐵𝑌𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
 
Theoremsrgass 12980 Associative law for the multiplication operation of a semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)       ((𝑅 ∈ SRing ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍)))
 
Theoremsrgideu 12981* The unity element of a semiring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)       (𝑅 ∈ SRing → ∃!𝑢𝐵𝑥𝐵 ((𝑢 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑢) = 𝑥))
 
Theoremsrgfcl 12982 Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by AV, 24-Aug-2021.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)       ((𝑅 ∈ SRing ∧ · Fn (𝐵 × 𝐵)) → · :(𝐵 × 𝐵)⟶𝐵)
 
Theoremsrgdi 12983 Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    + = (+g𝑅)    &    · = (.r𝑅)       ((𝑅 ∈ SRing ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)))
 
Theoremsrgdir 12984 Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    + = (+g𝑅)    &    · = (.r𝑅)       ((𝑅 ∈ SRing ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
 
Theoremsrgidcl 12985 The unity element of a semiring belongs to the base set of the semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    1 = (1r𝑅)       (𝑅 ∈ SRing → 1𝐵)
 
Theoremsrg0cl 12986 The zero element of a semiring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    0 = (0g𝑅)       (𝑅 ∈ SRing → 0𝐵)
 
Theoremsrgidmlem 12987 Lemma for srglidm 12988 and srgridm 12989. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)    &    1 = (1r𝑅)       ((𝑅 ∈ SRing ∧ 𝑋𝐵) → (( 1 · 𝑋) = 𝑋 ∧ (𝑋 · 1 ) = 𝑋))
 
Theoremsrglidm 12988 The unity element of a semiring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)    &    1 = (1r𝑅)       ((𝑅 ∈ SRing ∧ 𝑋𝐵) → ( 1 · 𝑋) = 𝑋)
 
Theoremsrgridm 12989 The unity element of a semiring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)    &    1 = (1r𝑅)       ((𝑅 ∈ SRing ∧ 𝑋𝐵) → (𝑋 · 1 ) = 𝑋)
 
Theoremissrgid 12990* Properties showing that an element 𝐼 is the unity element of a semiring. (Contributed by NM, 7-Aug-2013.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)    &    1 = (1r𝑅)       (𝑅 ∈ SRing → ((𝐼𝐵 ∧ ∀𝑥𝐵 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥)) ↔ 1 = 𝐼))
 
Theoremsrgacl 12991 Closure of the addition operation of a semiring. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    + = (+g𝑅)       ((𝑅 ∈ SRing ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
 
Theoremsrgcom 12992 Commutativity of the additive group of a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    + = (+g𝑅)       ((𝑅 ∈ SRing ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
 
Theoremsrgrz 12993 The zero of a semiring is a right-absorbing element. (Contributed by Thierry Arnoux, 1-Apr-2018.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)    &    0 = (0g𝑅)       ((𝑅 ∈ SRing ∧ 𝑋𝐵) → (𝑋 · 0 ) = 0 )
 
Theoremsrglz 12994 The zero of a semiring is a left-absorbing element. (Contributed by AV, 23-Aug-2019.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)    &    0 = (0g𝑅)       ((𝑅 ∈ SRing ∧ 𝑋𝐵) → ( 0 · 𝑋) = 0 )
 
Theoremsrgisid 12995* In a semiring, the only left-absorbing element is the additive identity. Remark in [Golan] p. 1. (Contributed by Thierry Arnoux, 1-May-2018.)
𝐵 = (Base‘𝑅)    &    · = (.r𝑅)    &    0 = (0g𝑅)    &   (𝜑𝑅 ∈ SRing)    &   (𝜑𝑍𝐵)    &   ((𝜑𝑥𝐵) → (𝑍 · 𝑥) = 𝑍)       (𝜑𝑍 = 0 )
 
Theoremsrg1zr 12996 The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.)
𝐵 = (Base‘𝑅)    &    + = (+g𝑅)    &    = (.r𝑅)       (((𝑅 ∈ SRing ∧ + Fn (𝐵 × 𝐵) ∧ Fn (𝐵 × 𝐵)) ∧ 𝑍𝐵) → (𝐵 = {𝑍} ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
Theoremsrgen1zr 12997 The only semiring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.)
𝐵 = (Base‘𝑅)    &    + = (+g𝑅)    &    = (.r𝑅)    &   𝑍 = (0g𝑅)       ((𝑅 ∈ SRing ∧ + Fn (𝐵 × 𝐵) ∧ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
Theoremsrgmulgass 12998 An associative property between group multiple and ring multiplication for semirings. (Contributed by AV, 23-Aug-2019.)
𝐵 = (Base‘𝑅)    &    · = (.g𝑅)    &    × = (.r𝑅)       ((𝑅 ∈ SRing ∧ (𝑁 ∈ ℕ0𝑋𝐵𝑌𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))
 
Theoremsrgpcomp 12999 If two elements of a semiring commute, they also commute if one of the elements is raised to a higher power. (Contributed by AV, 23-Aug-2019.)
𝑆 = (Base‘𝑅)    &    × = (.r𝑅)    &   𝐺 = (mulGrp‘𝑅)    &    = (.g𝐺)    &   (𝜑𝑅 ∈ SRing)    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐾 ∈ ℕ0)    &   (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))       (𝜑 → ((𝐾 𝐵) × 𝐴) = (𝐴 × (𝐾 𝐵)))
 
Theoremsrgpcompp 13000 If two elements of a semiring commute, they also commute if the elements are raised to a higher power. (Contributed by AV, 23-Aug-2019.)
𝑆 = (Base‘𝑅)    &    × = (.r𝑅)    &   𝐺 = (mulGrp‘𝑅)    &    = (.g𝐺)    &   (𝜑𝑅 ∈ SRing)    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐾 ∈ ℕ0)    &   (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (((𝑁 𝐴) × (𝐾 𝐵)) × 𝐴) = (((𝑁 + 1) 𝐴) × (𝐾 𝐵)))
    < 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-14485
  Copyright terms: Public domain < Previous  Next >