P. 383 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38201-38300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ablo4pnp 38201	A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))
Theorem	grpoeqdivid 38202	Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 = 𝐵 ↔ (𝐴𝐷𝐵) = 𝑈))
Theorem	grposnOLD 38203	The group operation for the singleton group. Obsolete, use grp1 19023. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∈ GrpOp
21.24.15  Group homomorphism and isomorphism
Syntax	cghomOLD 38204	Obsolete version of cghm 19187 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.)
class GrpOpHom
Definition	df-ghomOLD 38205*	Obsolete version of df-ghm 19188 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 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))})
Theorem	elghomlem1OLD 38206*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 38208. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))}    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆)
Theorem	elghomlem2OLD 38207*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 38208. (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 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦)))))
Theorem	elghomOLD 38208*	Obsolete version of isghm 19190 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 𝐻) ↔ (𝐹:𝑋⟶𝑊 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦)))))
Theorem	ghomlinOLD 38209	Obsolete version of ghmlin 19196 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 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴)𝐻(𝐹‘𝐵)) = (𝐹‘(𝐴𝐺𝐵)))
Theorem	ghomidOLD 38210	Obsolete version of ghmid 19197 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 𝐻)) → (𝐹‘𝑈) = 𝑇)
Theorem	ghomf 38211	Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑊 = ran 𝐻    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋⟶𝑊)
Theorem	ghomco 38212	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 𝐾))
Theorem	ghomdiv 38213	Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    &   ⊢ 𝐶 = ( /𝑔 ‘𝐻)    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐷𝐵)) = ((𝐹‘𝐴)𝐶(𝐹‘𝐵)))
Theorem	grpokerinj 38214	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→𝑌 ↔ (◡𝐹 “ {𝑈}) = {𝑊}))
21.24.16  Rings
Syntax	crngo 38215	Extend class notation with the class of all unital rings.
class RingOps
Definition	df-rngo 38216*	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 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)))}
Theorem	relrngo 38217	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
Theorem	isrngo 38218*	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 ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))))
Theorem	isrngod 38219*	Conditions that determine a ring. (Changed label from isringd 20272 to isrngod 38219-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)
Theorem	rngoi 38220*	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 ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))
Theorem	rngosm 38221	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 → 𝐻:(𝑋 × 𝑋)⟶𝑋)
Theorem	rngocl 38222	Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) ∈ 𝑋)
Theorem	rngoid 38223*	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 ∧ 𝐴 ∈ 𝑋) → ∃𝑢 ∈ 𝑋 ((𝑢𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑢) = 𝐴))
Theorem	rngoideu 38224*	The unity 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 → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))
Theorem	rngodi 38225	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 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐺𝐶)) = ((𝐴𝐻𝐵)𝐺(𝐴𝐻𝐶)))
Theorem	rngodir 38226	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 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐺(𝐵𝐻𝐶)))
Theorem	rngoass 38227	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 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = (𝐴𝐻(𝐵𝐻𝐶)))
Theorem	rngo2 38228*	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 ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝑋 (𝐴𝐺𝐴) = ((𝑥𝐺𝑥)𝐻𝐴))
Theorem	rngoablo 38229	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)
Theorem	rngoablo2 38230	In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
⊢ (⟨𝐺, 𝐻⟩ ∈ RingOps → 𝐺 ∈ AbelOp)
Theorem	rngogrpo 38231	A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    ⇒   ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp)
Theorem	rngone0 38232	The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → 𝑋 ≠ ∅)
Theorem	rngogcl 38233	Closure law for the addition (group) operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	rngocom 38234	The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))
Theorem	rngoaass 38235	The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))
Theorem	rngoa32 38236	The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵))
Theorem	rngoa4 38237	Rearrangement of 4 terms in a sum of ring elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷)))
Theorem	rngorcan 38238	Right cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵))
Theorem	rngolcan 38239	Left cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵))
Theorem	rngo0cl 38240	A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → 𝑍 ∈ 𝑋)
Theorem	rngo0rid 38241	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 ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴)
Theorem	rngo0lid 38242	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 ∧ 𝐴 ∈ 𝑋) → (𝑍𝐺𝐴) = 𝐴)
Theorem	rngolz 38243	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 ∧ 𝐴 ∈ 𝑋) → (𝑍𝐻𝐴) = 𝑍)
Theorem	rngorz 38244	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 ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻𝑍) = 𝑍)
Theorem	rngosn3 38245	Obsolete as of 25-Jan-2020. Use ring1zr 20753 or srg1zr 20196 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 ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ 𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩))
Theorem	rngosn4 38246	Obsolete as of 25-Jan-2020. Use rngen1zr 20754 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 ∧ 𝐴 ∈ 𝑋) → (𝑋 ≈ 1o ↔ 𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩))
Theorem	rngosn6 38247	Obsolete as of 25-Jan-2020. Use ringen1zr 20755 or srgen1zr 20197 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 → (𝑋 ≈ 1o ↔ 𝑅 = ⟨{⟨⟨𝑍, 𝑍⟩, 𝑍⟩}, {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩))
Theorem	rngonegcl 38248	A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋)
Theorem	rngoaddneg1 38249	Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑍)
Theorem	rngoaddneg2 38250	Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑍)
Theorem	rngosub 38251	Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁‘𝐵)))
Theorem	rngmgmbs4 38252*	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 𝐺 = 𝑋)
Theorem	rngodm1dm2 38253	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 𝐻)
Theorem	rngorn1 38254	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 𝐻)
Theorem	rngorn1eq 38255	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 𝐻)
Theorem	rngomndo 38256	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)
Theorem	rngoidmlem 38257	The unity element 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 ∧ 𝐴 ∈ 𝑋) → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴))
Theorem	rngolidm 38258	The unity element 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 ∧ 𝐴 ∈ 𝑋) → (𝑈𝐻𝐴) = 𝐴)
Theorem	rngoridm 38259	The unity element 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 ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻𝑈) = 𝐴)
Theorem	rngo1cl 38260	The unity element of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010.) (New usage is discouraged.)
⊢ 𝑋 = ran (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋)
Theorem	rngoueqz 38261	Obsolete as of 23-Jan-2020. Use 0ring01eqbi 20509 instead. In a unital ring the zero equals the ring unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o ↔ 𝑈 = 𝑍))
Theorem	rngonegmn1l 38262	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 ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = ((𝑁‘𝑈)𝐻𝐴))
Theorem	rngonegmn1r 38263	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 ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈)))
Theorem	rngoneglmul 38264	Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = ((𝑁‘𝐴)𝐻𝐵))
Theorem	rngonegrmul 38265	Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = (𝐴𝐻(𝑁‘𝐵)))
Theorem	rngosubdi 38266	Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐷𝐶)) = ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶)))
Theorem	rngosubdir 38267	Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶)))
Theorem	zerdivemp1x 38268*	In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv 20282. (Contributed by Jeff Madsen, 18-Apr-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ ∃𝑎 ∈ 𝑋 (𝑎𝐻𝐴) = 𝑈) → (𝐵 ∈ 𝑋 → ((𝐴𝐻𝐵) = 𝑍 → 𝐵 = 𝑍)))
21.24.17  Division Rings
Syntax	cdrng 38269	Extend class notation with the class of all division rings.
class DivRingOps
Definition	df-drngo 38270*	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)}
Theorem	isdivrngo 38271	The predicate "is a division ring". (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
⊢ (𝐻 ∈ 𝐴 → (⟨𝐺, 𝐻⟩ ∈ DivRingOps ↔ (⟨𝐺, 𝐻⟩ ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)))
Theorem	drngoi 38272	The properties of a division ring. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
Theorem	gidsn 38273	Obsolete as of 23-Jan-2020. Use mnd1id 18748 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‘{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}) = 𝐴
Theorem	zrdivrng 38274	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
Theorem	dvrunz 38275	In a division ring the ring 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 → 𝑈 ≠ 𝑍)
Theorem	isgrpda 38276*	Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.)
⊢ (𝜑 → 𝑋 ∈ V)    &   ⊢ (𝜑 → 𝐺:(𝑋 × 𝑋)⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑈𝐺𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑛 ∈ 𝑋 (𝑛𝐺𝑥) = 𝑈)    ⇒   ⊢ (𝜑 → 𝐺 ∈ GrpOp)
Theorem	isdrngo1 38277	The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
Theorem	divrngcl 38278	The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ DivRingOps ∧ 𝐴 ∈ (𝑋 ∖ {𝑍}) ∧ 𝐵 ∈ (𝑋 ∖ {𝑍})) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ {𝑍}))
Theorem	isdrngo2 38279*	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 ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))
Theorem	isdrngo3 38280*	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 ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))
21.24.18  Ring homomorphisms
Syntax	crngohom 38281	Extend class notation with the class of ring homomorphisms.
class RingOpsHom
Syntax	crngoiso 38282	Extend class notation with the class of ring isomorphisms.
class RingOpsIso
Syntax	crisc 38283	Extend class notation with the ring isomorphism relation.
class ≃𝑟
Definition	df-rngohom 38284*	Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ RingOpsHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st ‘𝑠) ↑m ran (1st ‘𝑟)) ∣ ((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))))})
Theorem	rngohomval 38285*	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) → (𝑅 RingOpsHom 𝑆) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))})
Theorem	isrngohom 38286*	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) → (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ↔ (𝐹:𝑋⟶𝑌 ∧ (𝐹‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))))))
Theorem	rngohomf 38287	A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹:𝑋⟶𝑌)
Theorem	rngohomcl 38288	Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ 𝑌)
Theorem	rngohom1 38289	A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.)
⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑈 = (GId‘𝐻)    &   ⊢ 𝐾 = (2nd ‘𝑆)    &   ⊢ 𝑉 = (GId‘𝐾)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑈) = 𝑉)
Theorem	rngohomadd 38290	Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐺𝐵)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵)))
Theorem	rngohommul 38291	Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝐾 = (2nd ‘𝑆)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵)))
Theorem	rngogrphom 38292	A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐽 = (1st ‘𝑆)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹 ∈ (𝐺 GrpOpHom 𝐽))
Theorem	rngohom0 38293	A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑊 = (GId‘𝐽)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑍) = 𝑊)
Theorem	rngohomsub 38294	Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐻 = ( /𝑔 ‘𝐺)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝐾 = ( /𝑔 ‘𝐽)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵)))
Theorem	rngohomco 38295	The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇))
Theorem	rngokerinj 38296	A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑊 = (GId‘𝐺)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    &   ⊢ 𝑍 = (GId‘𝐽)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹:𝑋–1-1→𝑌 ↔ (◡𝐹 “ {𝑍}) = {𝑊}))
Definition	df-rngoiso 38297*	Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ RingOpsIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1st ‘𝑟)–1-1-onto→ran (1st ‘𝑠)})
Theorem	rngoisoval 38298*	The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsIso 𝑆) = {𝑓 ∈ (𝑅 RingOpsHom 𝑆) ∣ 𝑓:𝑋–1-1-onto→𝑌})
Theorem	isrngoiso 38299	The predicate "is a ring isomorphism between 𝑅 and 𝑆". (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋–1-1-onto→𝑌)))
Theorem	rngoiso1o 38300	A ring isomorphism is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹:𝑋–1-1-onto→𝑌)