 Home Metamath Proof ExplorerTheorem List (p. 337 of 424) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-27745) Hilbert Space Explorer (27746-29270) Users' Mathboxes (29271-42316)

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremrrndstprj2 33601* Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 33600 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
𝑋 = (ℝ ↑𝑚 𝐼)    &   𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))       (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹𝑋𝐺𝑋) ∧ (𝑅 ∈ ℝ+ ∧ ∀𝑛𝐼 ((𝐹𝑛)𝑀(𝐺𝑛)) < 𝑅)) → (𝐹(ℝn𝐼)𝐺) < (𝑅 · (√‘(#‘𝐼))))

Theoremrrncmslem 33602* Lemma for rrncms 33603. (Contributed by Jeff Madsen, 6-Jun-2014.) (Revised by Mario Carneiro, 13-Sep-2015.)
𝑋 = (ℝ ↑𝑚 𝐼)    &   𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   𝐽 = (MetOpen‘(ℝn𝐼))    &   (𝜑𝐼 ∈ Fin)    &   (𝜑𝐹 ∈ (Cau‘(ℝn𝐼)))    &   (𝜑𝐹:ℕ⟶𝑋)    &   𝑃 = (𝑚𝐼 ↦ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹𝑡)‘𝑚))))       (𝜑𝐹 ∈ dom (⇝𝑡𝐽))

Theoremrrncms 33603 Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
𝑋 = (ℝ ↑𝑚 𝐼)       (𝐼 ∈ Fin → (ℝn𝐼) ∈ (CMet‘𝑋))

Theoremrepwsmet 33604 The supremum metric on ℝ↑𝐼 is a metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
𝑌 = ((ℂflds ℝ) ↑s 𝐼)    &   𝐷 = (dist‘𝑌)    &   𝑋 = (ℝ ↑𝑚 𝐼)       (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋))

Theoremrrnequiv 33605 The supremum metric on ℝ↑𝐼 is equivalent to the n metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
𝑌 = ((ℂflds ℝ) ↑s 𝐼)    &   𝐷 = (dist‘𝑌)    &   𝑋 = (ℝ ↑𝑚 𝐼)    &   (𝜑𝐼 ∈ Fin)       ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn𝐼)𝐺) ∧ (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺))))

Theoremrrntotbnd 33606 A set in Euclidean space is totally bounded iff its is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
𝑋 = (ℝ ↑𝑚 𝐼)    &   𝑀 = ((ℝn𝐼) ↾ (𝑌 × 𝑌))       (𝐼 ∈ Fin → (𝑀 ∈ (TotBnd‘𝑌) ↔ 𝑀 ∈ (Bnd‘𝑌)))

Theoremrrnheibor 33607 Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
𝑋 = (ℝ ↑𝑚 𝐼)    &   𝑀 = ((ℝn𝐼) ↾ (𝑌 × 𝑌))    &   𝑇 = (MetOpen‘𝑀)    &   𝑈 = (MetOpen‘(ℝn𝐼))       ((𝐼 ∈ Fin ∧ 𝑌𝑋) → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌))))

20.19.12  Intervals (continued)

Theoremismrer1 33608* An isometry between and ℝ↑1. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
𝑅 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   𝐹 = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥}))       (𝐴𝑉𝐹 ∈ (𝑅 Ismty (ℝn‘{𝐴})))

Theoremreheibor 33609 Heine-Borel theorem for real numbers. A subset of is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
𝑀 = ((abs ∘ − ) ↾ (𝑌 × 𝑌))    &   𝑇 = (MetOpen‘𝑀)    &   𝑈 = (topGen‘ran (,))       (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌))))

Theoremiccbnd 33610 A closed interval in is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Sep-2015.)
𝐽 = (𝐴[,]𝐵)    &   𝑀 = ((abs ∘ − ) ↾ (𝐽 × 𝐽))       ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑀 ∈ (Bnd‘𝐽))

TheoremicccmpALT 33611 A closed interval in is compact. Alternate proof of icccmp 22609 using the Heine-Borel theorem heibor 33591. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Aug-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
𝐽 = (𝐴[,]𝐵)    &   𝑀 = ((abs ∘ − ) ↾ (𝐽 × 𝐽))    &   𝑇 = (MetOpen‘𝑀)       ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp)

20.19.13  Operation properties

Syntaxcass 33612 Extend class notation with a device to add associativity to internal operations.
class Ass

Definitiondf-ass 33613* A device to add associativity to various sorts of internal operations. The definition is meaningful when 𝑔 is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
Ass = {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}

Syntaxcexid 33614 Extend class notation with the class of all the internal operations with an identity element.
class ExId

Definitiondf-exid 33615* A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
ExId = {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}

Theoremisass 33616* The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
𝑋 = dom dom 𝐺       (𝐺𝐴 → (𝐺 ∈ Ass ↔ ∀𝑥𝑋𝑦𝑋𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))

Theoremisexid 33617* The predicate 𝐺 has a left and right identity element. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝑋 = dom dom 𝐺       (𝐺𝐴 → (𝐺 ∈ ExId ↔ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦)))

20.19.14  Groups and related structures

Syntaxcmagm 33618 Extend class notation with the class of all magmas.
class Magma

Definitiondf-mgmOLD 33619* Obsolete version of df-mgm 17223 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
Magma = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}

TheoremismgmOLD 33620 Obsolete version of ismgm 17224 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑋 = dom dom 𝐺       (𝐺𝐴 → (𝐺 ∈ Magma ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋))

TheoremclmgmOLD 33621 Obsolete version of mgmcl 17226 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑋 = dom dom 𝐺       ((𝐺 ∈ Magma ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)

TheoremopidonOLD 33622 Obsolete version of mndpfo 17295 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑋 = dom dom 𝐺       (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto𝑋)

TheoremrngopidOLD 33623 Obsolete version of mndpfo 17295 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
(𝐺 ∈ (Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺)

Theoremopidon2OLD 33624 Obsolete version of mndpfo 17295 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑋 = ran 𝐺       (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto𝑋)

Theoremisexid2 33625* If 𝐺 ∈ (Magma ∩ ExId ), then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝑋 = ran 𝐺       (𝐺 ∈ (Magma ∩ ExId ) → ∃𝑢𝑋𝑥𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))

Theoremexidu1 33626* Unicity of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝑋 = ran 𝐺       (𝐺 ∈ (Magma ∩ ExId ) → ∃!𝑢𝑋𝑥𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))

Theoremidrval 33627* The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐺)       (𝐺𝐴𝑈 = (𝑢𝑋𝑥𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))

Theoremiorlid 33628 A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐺)       (𝐺 ∈ (Magma ∩ ExId ) → 𝑈𝑋)

Theoremcmpidelt 33629 A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐺)       ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴𝑋) → ((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴))

Syntaxcsem 33630 Extend class notation with the class of all semi-groups.
class SemiGrp

Definitiondf-sgrOLD 33631 Obsolete version of df-sgrp 17265 as of 3-Feb-2020. A semi-group is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
SemiGrp = (Magma ∩ Ass)

TheoremsmgrpismgmOLD 33632 Obsolete version of sgrpmgm 17270 as of 3-Feb-2020. A semi-group is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
(𝐺 ∈ SemiGrp → 𝐺 ∈ Magma)

TheoremissmgrpOLD 33633* Obsolete version of issgrp 17266 as of 3-Feb-2020. The predicate "is a semi-group". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑋 = dom dom 𝐺       (𝐺𝐴 → (𝐺 ∈ SemiGrp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥𝑋𝑦𝑋𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))))

Theoremsmgrpmgm 33634 A semi-group is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
𝑋 = dom dom 𝐺       (𝐺 ∈ SemiGrp → 𝐺:(𝑋 × 𝑋)⟶𝑋)

TheoremsmgrpassOLD 33635* Obsolete version of sgrpass 17271 as of 3-Feb-2020. A semi-group is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑋 = dom dom 𝐺       (𝐺 ∈ SemiGrp → ∀𝑥𝑋𝑦𝑋𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))

Syntaxcmndo 33636 Extend class notation with the class of all monoids.
class MndOp

Definitiondf-mndo 33637 A monoid is a semi-group with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
MndOp = (SemiGrp ∩ ExId )

TheoremmndoissmgrpOLD 33638 Obsolete version of mndsgrp 17280 as of 3-Feb-2020. A monoid is a semi-group. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
(𝐺 ∈ MndOp → 𝐺 ∈ SemiGrp)

Theoremmndoisexid 33639 A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
(𝐺 ∈ MndOp → 𝐺 ∈ ExId )

TheoremmndoismgmOLD 33640 Obsolete version of mndmgm 17281 as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
(𝐺 ∈ MndOp → 𝐺 ∈ Magma)

Theoremmndomgmid 33641 A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.)
(𝐺 ∈ MndOp → 𝐺 ∈ (Magma ∩ ExId ))

Theoremismndo 33642* The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝑋 = dom dom 𝐺       (𝐺𝐴 → (𝐺 ∈ MndOp ↔ (𝐺 ∈ SemiGrp ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))))

Theoremismndo1 33643* The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝑋 = dom dom 𝐺       (𝐺𝐴 → (𝐺 ∈ MndOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥𝑋𝑦𝑋𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))))

Theoremismndo2 33644* The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝑋 = ran 𝐺       (𝐺𝐴 → (𝐺 ∈ MndOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥𝑋𝑦𝑋𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))))

Theoremgrpomndo 33645 A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
(𝐺 ∈ GrpOp → 𝐺 ∈ MndOp)

Theoremexidcl 33646 Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.)
𝑋 = ran 𝐺       ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)

Theoremexidreslem 33647* Lemma for exidres 33648 and exidresid 33649. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐺)    &   𝐻 = (𝐺 ↾ (𝑌 × 𝑌))       ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌) → (𝑈 ∈ dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)))

Theoremexidres 33648 The restriction of a binary operation with identity to a subset containing the identity has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐺)    &   𝐻 = (𝐺 ↾ (𝑌 × 𝑌))       ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌) → 𝐻 ∈ ExId )

Theoremexidresid 33649 The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐺)    &   𝐻 = (𝐺 ↾ (𝑌 × 𝑌))       (((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌) ∧ 𝐻 ∈ Magma) → (GId‘𝐻) = 𝑈)

Theoremablo4pnp 33650 A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.)
𝑋 = ran 𝐺    &   𝐷 = ( /𝑔𝐺)       ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))

Theoremgrpoeqdivid 33651 Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.)
𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐺)    &   𝐷 = ( /𝑔𝐺)       ((𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋) → (𝐴 = 𝐵 ↔ (𝐴𝐷𝐵) = 𝑈))

TheoremgrposnOLD 33652 The group operation for the singleton group. Obsolete, use grp1 17503. instead (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
𝐴 ∈ V       {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∈ GrpOp

20.19.15  Group homomorphism and isomorphism

SyntaxcghomOLD 33653 Obsolete version of cghm 17638 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.)
class GrpOpHom

Definitiondf-ghomOLD 33654* Obsolete version of df-ghm 17639 as of 15-Mar-2020. Define the set of group homomorphisms from 𝑔 to . (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
GrpOpHom = (𝑔 ∈ GrpOp, ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ∧ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝑔𝑦)))})

Theoremelghomlem1OLD 33655* Obsolete as of 15-Mar-2020. Lemma for elghomOLD 33657. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)𝐻(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))}       ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆)

Theoremelghomlem2OLD 33656* Obsolete as of 15-Mar-2020. Lemma for elghomOLD 33657. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)𝐻(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))}       ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝐹𝑥)𝐻(𝐹𝑦)) = (𝐹‘(𝑥𝐺𝑦)))))

TheoremelghomOLD 33657* Obsolete version of isghm 17641 as of 15-Mar-2020. Membership in the set of group homomorphisms from 𝐺 to 𝐻. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑋 = ran 𝐺    &   𝑊 = ran 𝐻       ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝐹:𝑋𝑊 ∧ ∀𝑥𝑋𝑦𝑋 ((𝐹𝑥)𝐻(𝐹𝑦)) = (𝐹‘(𝑥𝐺𝑦)))))

TheoremghomlinOLD 33658 Obsolete version of ghmlin 17646 as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑋 = ran 𝐺       (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴)𝐻(𝐹𝐵)) = (𝐹‘(𝐴𝐺𝐵)))

TheoremghomidOLD 33659 Obsolete version of ghmid 17647 as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑈 = (GId‘𝐺)    &   𝑇 = (GId‘𝐻)       ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹𝑈) = 𝑇)

Theoremghomf 33660 Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.)
𝑋 = ran 𝐺    &   𝑊 = ran 𝐻       ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋𝑊)

Theoremghomco 33661 The composition of two group homomorphisms is a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
(((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) ∧ (𝑆 ∈ (𝐺 GrpOpHom 𝐻) ∧ 𝑇 ∈ (𝐻 GrpOpHom 𝐾))) → (𝑇𝑆) ∈ (𝐺 GrpOpHom 𝐾))

Theoremghomdiv 33662 Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.)
𝑋 = ran 𝐺    &   𝐷 = ( /𝑔𝐺)    &   𝐶 = ( /𝑔𝐻)       (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹‘(𝐴𝐷𝐵)) = ((𝐹𝐴)𝐶(𝐹𝐵)))

Theoremgrpokerinj 33663 A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.)
𝑋 = ran 𝐺    &   𝑊 = (GId‘𝐺)    &   𝑌 = ran 𝐻    &   𝑈 = (GId‘𝐻)       ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹:𝑋1-1𝑌 ↔ (𝐹 “ {𝑈}) = {𝑊}))

20.19.16  Rings

Syntaxcrngo 33664 Extend class notation with the class of all unital rings.
class RingOps

Definitiondf-rngo 33665* Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.)
RingOps = {⟨𝑔, ⟩ ∣ ((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)))}

Theoremrelrngo 33666 The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
Rel RingOps

Theoremisrngo 33667* The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
𝑋 = ran 𝐺       (𝐻𝐴 → (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))))

Theoremisrngod 33668* Conditions that determine a ring. (Changed label from isringd 18566 to isrngod 33668-NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
(𝜑𝐺 ∈ AbelOp)    &   (𝜑𝑋 = ran 𝐺)    &   (𝜑𝐻:(𝑋 × 𝑋)⟶𝑋)    &   ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)))    &   ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)))    &   ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧)))    &   (𝜑𝑈𝑋)    &   ((𝜑𝑦𝑋) → (𝑈𝐻𝑦) = 𝑦)    &   ((𝜑𝑦𝑋) → (𝑦𝐻𝑈) = 𝑦)       (𝜑 → ⟨𝐺, 𝐻⟩ ∈ RingOps)

Theoremrngoi 33669* The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       (𝑅 ∈ RingOps → ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))

Theoremrngosm 33670 Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       (𝑅 ∈ RingOps → 𝐻:(𝑋 × 𝑋)⟶𝑋)

Theoremrngocl 33671 Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐻𝐵) ∈ 𝑋)

Theoremrngoid 33672* The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑢𝑋 ((𝑢𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑢) = 𝐴))

Theoremrngoideu 33673* The unit element of a ring is unique. (Contributed by NM, 4-Apr-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       (𝑅 ∈ RingOps → ∃!𝑢𝑋𝑥𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))

Theoremrngodi 33674 Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → (𝐴𝐻(𝐵𝐺𝐶)) = ((𝐴𝐻𝐵)𝐺(𝐴𝐻𝐶)))

Theoremrngodir 33675 Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → ((𝐴𝐺𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐺(𝐵𝐻𝐶)))

Theoremrngoass 33676 Associative law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = (𝐴𝐻(𝐵𝐻𝐶)))

Theoremrngo2 33677* A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑥𝑋 (𝐴𝐺𝐴) = ((𝑥𝐺𝑥)𝐻𝐴))

Theoremrngoablo 33678 A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)       (𝑅 ∈ RingOps → 𝐺 ∈ AbelOp)

Theoremrngoablo2 33679 In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
(⟨𝐺, 𝐻⟩ ∈ RingOps → 𝐺 ∈ AbelOp)

Theoremrngogrpo 33680 A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)       (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp)

Theoremrngone0 33681 The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       (𝑅 ∈ RingOps → 𝑋 ≠ ∅)

Theoremrngogcl 33682 Closure law for the addition (group) operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)

Theoremrngocom 33683 The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))

Theoremrngoaass 33684 The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))

Theoremrngoa32 33685 The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵))

Theoremrngoa4 33686 Rearrangement of 4 terms in a sum of ring elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐷𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷)))

Theoremrngorcan 33687 Right cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵))

Theoremrngolcan 33688 Left cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵))

Theoremrngo0cl 33689 A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑍 = (GId‘𝐺)       (𝑅 ∈ RingOps → 𝑍𝑋)

Theoremrngo0rid 33690 The additive identity of a ring is a right identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑍 = (GId‘𝐺)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝐴𝐺𝑍) = 𝐴)

Theoremrngo0lid 33691 The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑍 = (GId‘𝐺)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑍𝐺𝐴) = 𝐴)

Theoremrngolz 33692 The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
𝑍 = (GId‘𝐺)    &   𝑋 = ran 𝐺    &   𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑍𝐻𝐴) = 𝑍)

Theoremrngorz 33693 The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
𝑍 = (GId‘𝐺)    &   𝑋 = ran 𝐺    &   𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝐴𝐻𝑍) = 𝑍)

Theoremrngosn3 33694 Obsolete as of 25-Jan-2020. Use ring1zr 19256 or srg1zr 18510 instead. The only unital ring with a base set consisting in one element is the zero ring. (Contributed by FL, 13-Feb-2010.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ 𝐴𝐵) → (𝑋 = {𝐴} ↔ 𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩))

Theoremrngosn4 33695 Obsolete as of 25-Jan-2020. Use rngen1zr 19257 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑋 ≈ 1𝑜𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩))

Theoremrngosn6 33696 Obsolete as of 25-Jan-2020. Use ringen1zr 19258 or srgen1zr 18511 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑍 = (GId‘𝐺)       (𝑅 ∈ RingOps → (𝑋 ≈ 1𝑜𝑅 = ⟨{⟨⟨𝑍, 𝑍⟩, 𝑍⟩}, {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩))

Theoremrngonegcl 33697 A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑁 = (inv‘𝐺)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑁𝐴) ∈ 𝑋)