 Home Metamath Proof ExplorerTheorem List (p. 339 of 429) < 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-27903) Hilbert Space Explorer (27904-29428) Users' Mathboxes (29429-42879)

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

Theoremismndo 33801* 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 33802* 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 33803* 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 33804 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 33805 Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.)
𝑋 = ran 𝐺       ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)

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

Theoremexidres 33807 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 33808 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 33809 A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.)
𝑋 = ran 𝐺    &   𝐷 = ( /𝑔𝐺)       ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))

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

TheoremgrposnOLD 33811 The group operation for the singleton group. Obsolete, use grp1 17569. 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 33812 Obsolete version of cghm 17704 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.)
class GrpOpHom

Definitiondf-ghomOLD 33813* Obsolete version of df-ghm 17705 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 33814* Obsolete as of 15-Mar-2020. Lemma for elghomOLD 33816. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)𝐻(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))}       ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆)

Theoremelghomlem2OLD 33815* Obsolete as of 15-Mar-2020. Lemma for elghomOLD 33816. (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 33816* Obsolete version of isghm 17707 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 33817 Obsolete version of ghmlin 17712 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 33818 Obsolete version of ghmid 17713 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 33819 Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.)
𝑋 = ran 𝐺    &   𝑊 = ran 𝐻       ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋𝑊)

Theoremghomco 33820 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 33821 Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.)
𝑋 = ran 𝐺    &   𝐷 = ( /𝑔𝐺)    &   𝐶 = ( /𝑔𝐻)       (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹‘(𝐴𝐷𝐵)) = ((𝐹𝐴)𝐶(𝐹𝐵)))

Theoremgrpokerinj 33822 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 33823 Extend class notation with the class of all unital rings.
class RingOps

Definitiondf-rngo 33824* 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 33825 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 33826* 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 33827* Conditions that determine a ring. (Changed label from isringd 18631 to isrngod 33827-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 33828* 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 33829 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 33830 Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐻𝐵) ∈ 𝑋)

Theoremrngoid 33831* 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 33832* 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 33833 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 33834 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 33835 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 33836* 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 33837 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 33838 In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
(⟨𝐺, 𝐻⟩ ∈ RingOps → 𝐺 ∈ AbelOp)

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

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

Theoremrngogcl 33841 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 33842 The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺       ((𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))

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

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

Theoremrngoa4 33845 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 33846 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 33847 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 33848 A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑍 = (GId‘𝐺)       (𝑅 ∈ RingOps → 𝑍𝑋)

Theoremrngo0rid 33849 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 33850 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 33851 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 33852 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 33853 Obsolete as of 25-Jan-2020. Use ring1zr 19323 or srg1zr 18575 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 33854 Obsolete as of 25-Jan-2020. Use rngen1zr 19324 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 33855 Obsolete as of 25-Jan-2020. Use ringen1zr 19325 or srgen1zr 18576 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 33856 A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑁 = (inv‘𝐺)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑁𝐴) ∈ 𝑋)

𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑁 = (inv‘𝐺)    &   𝑍 = (GId‘𝐺)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝐴𝐺(𝑁𝐴)) = 𝑍)

𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑁 = (inv‘𝐺)    &   𝑍 = (GId‘𝐺)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((𝑁𝐴)𝐺𝐴) = 𝑍)

Theoremrngosub 33859 Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝑁 = (inv‘𝐺)    &   𝐷 = ( /𝑔𝐺)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁𝐵)))

Theoremrngmgmbs4 33860* The range of an internal operation with a left and right identity element equals its base set. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
((𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∃𝑢𝑋𝑥𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) → ran 𝐺 = 𝑋)

Theoremrngodm1dm2 33861 In a unital ring the domain of the first variable of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
𝐻 = (2nd𝑅)    &   𝐺 = (1st𝑅)       (𝑅 ∈ RingOps → dom dom 𝐺 = dom dom 𝐻)

Theoremrngorn1 33862 In a unital ring the range of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
𝐻 = (2nd𝑅)    &   𝐺 = (1st𝑅)       (𝑅 ∈ RingOps → ran 𝐺 = dom dom 𝐻)

Theoremrngorn1eq 33863 In a unital ring the range of the addition equals the range of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
𝐻 = (2nd𝑅)    &   𝐺 = (1st𝑅)       (𝑅 ∈ RingOps → ran 𝐺 = ran 𝐻)

Theoremrngomndo 33864 In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
𝐻 = (2nd𝑅)       (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)

Theoremrngoidmlem 33865 The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.)
𝐻 = (2nd𝑅)    &   𝑋 = ran (1st𝑅)    &   𝑈 = (GId‘𝐻)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴))

Theoremrngolidm 33866 The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.)
𝐻 = (2nd𝑅)    &   𝑋 = ran (1st𝑅)    &   𝑈 = (GId‘𝐻)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑈𝐻𝐴) = 𝐴)

Theoremrngoridm 33867 The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.)
𝐻 = (2nd𝑅)    &   𝑋 = ran (1st𝑅)    &   𝑈 = (GId‘𝐻)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝐴𝐻𝑈) = 𝐴)

Theoremrngo1cl 33868 The unit of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010.) (New usage is discouraged.)
𝑋 = ran (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑈 = (GId‘𝐻)       (𝑅 ∈ RingOps → 𝑈𝑋)

Theoremrngoueqz 33869 Obsolete as of 23-Jan-2020. Use 0ring01eqbi 19321 instead. In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑍 = (GId‘𝐺)    &   𝑈 = (GId‘𝐻)    &   𝑋 = ran 𝐺       (𝑅 ∈ RingOps → (𝑋 ≈ 1𝑜𝑈 = 𝑍))

Theoremrngonegmn1l 33870 Negation in a ring is the same as left multiplication by -1. (Contributed by Jeff Madsen, 10-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝑁 = (inv‘𝐺)    &   𝑈 = (GId‘𝐻)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑁𝐴) = ((𝑁𝑈)𝐻𝐴))

Theoremrngonegmn1r 33871 Negation in a ring is the same as right multiplication by -1. (Contributed by Jeff Madsen, 19-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝑁 = (inv‘𝐺)    &   𝑈 = (GId‘𝐻)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑁𝐴) = (𝐴𝐻(𝑁𝑈)))

Theoremrngoneglmul 33872 Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝑁 = (inv‘𝐺)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋) → (𝑁‘(𝐴𝐻𝐵)) = ((𝑁𝐴)𝐻𝐵))

Theoremrngonegrmul 33873 Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝑁 = (inv‘𝐺)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋) → (𝑁‘(𝐴𝐻𝐵)) = (𝐴𝐻(𝑁𝐵)))

Theoremrngosubdi 33874 Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝐷 = ( /𝑔𝐺)       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → (𝐴𝐻(𝐵𝐷𝐶)) = ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶)))

Theoremrngosubdir 33875 Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝐷 = ( /𝑔𝐺)       ((𝑅 ∈ RingOps ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → ((𝐴𝐷𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶)))

Theoremzerdivemp1x 33876* In a unitary ring a left invertible element is not a zero divisor. See also ringinvnzdiv 18639. (Contributed by Jeff Madsen, 18-Apr-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑍 = (GId‘𝐺)    &   𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐻)       ((𝑅 ∈ RingOps ∧ 𝐴𝑋 ∧ ∃𝑎𝑋 (𝑎𝐻𝐴) = 𝑈) → (𝐵𝑋 → ((𝐴𝐻𝐵) = 𝑍𝐵 = 𝑍)))

20.19.17  Division Rings

Syntaxcdrng 33877 Extend class notation with the class of all division rings.
class DivRingOps

Definitiondf-drngo 33878* Define the class of all division rings (sometimes called skew fields). A division ring is a unital ring where every element except the additive identity has a multiplicative inverse. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.)
DivRingOps = {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}

Theoremisdivrngo 33879 The predicate "is a division ring". (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
(𝐻𝐴 → (⟨𝐺, 𝐻⟩ ∈ DivRingOps ↔ (⟨𝐺, 𝐻⟩ ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)))

Theoremdrngoi 33880 The properties of a division ring. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝑍 = (GId‘𝐺)       (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))

Theoremgidsn 33881 Obsolete as of 23-Jan-2020. Use mnd1id 17379 instead. The identity element of the trivial group. (Contributed by FL, 21-Jun-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
𝐴 ∈ V       (GId‘{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}) = 𝐴

Theoremzrdivrng 33882 The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
𝐴 ∈ V        ¬ ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩ ∈ DivRingOps

Theoremdvrunz 33883 In a division ring the unit is different from the zero. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝑍 = (GId‘𝐺)    &   𝑈 = (GId‘𝐻)       (𝑅 ∈ DivRingOps → 𝑈𝑍)

Theoremisgrpda 33884* Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.)
(𝜑𝑋 ∈ V)    &   (𝜑𝐺:(𝑋 × 𝑋)⟶𝑋)    &   ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   (𝜑𝑈𝑋)    &   ((𝜑𝑥𝑋) → (𝑈𝐺𝑥) = 𝑥)    &   ((𝜑𝑥𝑋) → ∃𝑛𝑋 (𝑛𝐺𝑥) = 𝑈)       (𝜑𝐺 ∈ GrpOp)

Theoremisdrngo1 33885 The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑍 = (GId‘𝐺)    &   𝑋 = ran 𝐺       (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))

Theoremdivrngcl 33886 The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑍 = (GId‘𝐺)    &   𝑋 = ran 𝐺       ((𝑅 ∈ DivRingOps ∧ 𝐴 ∈ (𝑋 ∖ {𝑍}) ∧ 𝐵 ∈ (𝑋 ∖ {𝑍})) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ {𝑍}))

Theoremisdrngo2 33887* A division ring is a ring in which 1 ≠ 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑍 = (GId‘𝐺)    &   𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐻)       (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))

Theoremisdrngo3 33888* A division ring is a ring in which 1 ≠ 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑍 = (GId‘𝐺)    &   𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐻)       (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦𝑋 (𝑦𝐻𝑥) = 𝑈)))

20.19.18  Ring homomorphisms

Syntaxcrnghom 33889 Extend class notation with the class of ring homomorphisms.
class RngHom

Syntaxcrngiso 33890 Extend class notation with the class of ring isomorphisms.
class RngIso

Syntaxcrisc 33891 Extend class notation with the ring isomorphism relation.
class 𝑟

Definitiondf-rngohom 33892* Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
RngHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st𝑠) ↑𝑚 ran (1st𝑟)) ∣ ((𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠)) ∧ ∀𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))))})

Theoremrngohomval 33893* The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 22-Sep-2015.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐻)    &   𝐽 = (1st𝑆)    &   𝐾 = (2nd𝑆)    &   𝑌 = ran 𝐽    &   𝑉 = (GId‘𝐾)       ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RngHom 𝑆) = {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ((𝑓𝑈) = 𝑉 ∧ ∀𝑥𝑋𝑦𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓𝑥)𝐽(𝑓𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓𝑥)𝐾(𝑓𝑦))))})

Theoremisrngohom 33894* The predicate "is a ring homomorphism from 𝑅 to 𝑆." (Contributed by Jeff Madsen, 19-Jun-2010.)
𝐺 = (1st𝑅)    &   𝐻 = (2nd𝑅)    &   𝑋 = ran 𝐺    &   𝑈 = (GId‘𝐻)    &   𝐽 = (1st𝑆)    &   𝐾 = (2nd𝑆)    &   𝑌 = ran 𝐽    &   𝑉 = (GId‘𝐾)       ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RngHom 𝑆) ↔ (𝐹:𝑋𝑌 ∧ (𝐹𝑈) = 𝑉 ∧ ∀𝑥𝑋𝑦𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹𝑥)𝐽(𝐹𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹𝑥)𝐾(𝐹𝑦))))))

Theoremrngohomf 33895 A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝐽 = (1st𝑆)    &   𝑌 = ran 𝐽       ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:𝑋𝑌)

Theoremrngohomcl 33896 Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.)
𝐺 = (1st𝑅)    &   𝑋 = ran 𝐺    &   𝐽 = (1st𝑆)    &   𝑌 = ran 𝐽       (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝐴𝑋) → (𝐹𝐴) ∈ 𝑌)

Theoremrngohom1 33897 A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.)
𝐻 = (2nd𝑅)    &   𝑈 = (GId‘𝐻)    &   𝐾 = (2nd𝑆)    &   𝑉 = (GId‘𝐾)       ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹𝑈) = 𝑉)