P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	repwsmet 36001	The supremum metric on ℝ↑𝐼 is a metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
⊢ 𝑌 = ((ℂfld ↾s ℝ) ↑s 𝐼)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋))
Theorem	rrnequiv 36002	The supremum metric on ℝ↑𝐼 is equivalent to the ℝn metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
⊢ 𝑌 = ((ℂfld ↾s ℝ) ↑s 𝐼)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    ⇒   ⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))))
Theorem	rrntotbnd 36003	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.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((ℝn‘𝐼) ↾ (𝑌 × 𝑌))    ⇒   ⊢ (𝐼 ∈ Fin → (𝑀 ∈ (TotBnd‘𝑌) ↔ 𝑀 ∈ (Bnd‘𝑌)))
Theorem	rrnheibor 36004	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.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((ℝn‘𝐼) ↾ (𝑌 × 𝑌))    &   ⊢ 𝑇 = (MetOpen‘𝑀)    &   ⊢ 𝑈 = (MetOpen‘(ℝn‘𝐼))    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋) → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌))))
20.20.12  Intervals (continued)
Theorem	ismrer1 36005*	An isometry between ℝ and ℝ↑1. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑅 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ (𝑅 Ismty (ℝn‘{𝐴})))
Theorem	reheibor 36006	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‘𝑌))))
Theorem	iccbnd 36007	A closed interval in ℝ is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐽 = (𝐴[,]𝐵)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (𝐽 × 𝐽))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑀 ∈ (Bnd‘𝐽))
Theorem	icccmpALT 36008	A closed interval in ℝ is compact. Alternate proof of icccmp 23997 using the Heine-Borel theorem heibor 35988. (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.20.13  Operation properties
Syntax	cass 36009	Extend class notation with a device to add associativity to internal operations.
class Ass
Definition	df-ass 36010*	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 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}
Syntax	cexid 36011	Extend class notation with the class of all the internal operations with an identity element.
class ExId
Definition	df-exid 36012*	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 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}
Theorem	isass 36013*	The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Ass ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
Theorem	isexid 36014*	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.20.14  Groups and related structures
Syntax	cmagm 36015	Extend class notation with the class of all magmas.
class Magma
Definition	df-mgmOLD 36016*	Obsolete version of df-mgm 18335 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ Magma = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}
Theorem	ismgmOLD 36017	Obsolete version of ismgm 18336 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 ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋))
Theorem	clmgmOLD 36018	Obsolete version of mgmcl 18338 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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	opidonOLD 36019	Obsolete version of mndpfo 18417 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→𝑋)
Theorem	rngopidOLD 36020	Obsolete version of mndpfo 18417 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 𝐺)
Theorem	opidon2OLD 36021	Obsolete version of mndpfo 18417 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→𝑋)
Theorem	isexid2 36022*	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 ) → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))
Theorem	exidu1 36023*	Uniqueness 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 ) → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))
Theorem	idrval 36024*	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‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝐴 → 𝑈 = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))
Theorem	iorlid 36025	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 ) → 𝑈 ∈ 𝑋)
Theorem	cmpidelt 36026	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 ) ∧ 𝐴 ∈ 𝑋) → ((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴))
Syntax	csem 36027	Extend class notation with the class of all semigroups.
class SemiGrp
Definition	df-sgrOLD 36028	Obsolete version of df-sgrp 18384 as of 3-Feb-2020. A semigroup is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ SemiGrp = (Magma ∩ Ass)
Theorem	smgrpismgmOLD 36029	Obsolete version of sgrpmgm 18389 as of 3-Feb-2020. A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ SemiGrp → 𝐺 ∈ Magma)
Theorem	issmgrpOLD 36030*	Obsolete version of issgrp 18385 as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ SemiGrp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))))
Theorem	smgrpmgm 36031	A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ SemiGrp → 𝐺:(𝑋 × 𝑋)⟶𝑋)
Theorem	smgrpassOLD 36032*	Obsolete version of sgrpass 18390 as of 3-Feb-2020. A semigroup is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ SemiGrp → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))
Syntax	cmndo 36033	Extend class notation with the class of all monoids.
class MndOp
Definition	df-mndo 36034	A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ MndOp = (SemiGrp ∩ ExId )
Theorem	mndoissmgrpOLD 36035	Obsolete version of mndsgrp 18400 as of 3-Feb-2020. A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ MndOp → 𝐺 ∈ SemiGrp)
Theorem	mndoisexid 36036	A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ (𝐺 ∈ MndOp → 𝐺 ∈ ExId )
Theorem	mndoismgmOLD 36037	Obsolete version of mndmgm 18401 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)
Theorem	mndomgmid 36038	A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.)
⊢ (𝐺 ∈ MndOp → 𝐺 ∈ (Magma ∩ ExId ))
Theorem	ismndo 36039*	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 ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))))
Theorem	ismndo1 36040*	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 ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))))
Theorem	ismndo2 36041*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))))
Theorem	grpomndo 36042	A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ (𝐺 ∈ GrpOp → 𝐺 ∈ MndOp)
Theorem	exidcl 36043	Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	exidreslem 36044*	Lemma for exidres 36045 and exidresid 36046. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑈 ∈ dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)))
Theorem	exidres 36045	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 )
Theorem	exidresid 36046	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‘𝐻) = 𝑈)
Theorem	ablo4pnp 36047	A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))
Theorem	grpoeqdivid 36048	Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 = 𝐵 ↔ (𝐴𝐷𝐵) = 𝑈))
Theorem	grposnOLD 36049	The group operation for the singleton group. Obsolete, use grp1 18691. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∈ GrpOp
20.20.15  Group homomorphism and isomorphism
Syntax	cghomOLD 36050	Obsolete version of cghm 18840 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.)
class GrpOpHom
Definition	df-ghomOLD 36051*	Obsolete version of df-ghm 18841 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 36052*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 36054. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))}    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆)
Theorem	elghomlem2OLD 36053*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 36054. (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 36054*	Obsolete version of isghm 18843 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 36055	Obsolete version of ghmlin 18848 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 36056	Obsolete version of ghmid 18849 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 36057	Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑊 = ran 𝐻    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋⟶𝑊)
Theorem	ghomco 36058	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 36059	Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    &   ⊢ 𝐶 = ( /𝑔 ‘𝐻)    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐷𝐵)) = ((𝐹‘𝐴)𝐶(𝐹‘𝐵)))
Theorem	grpokerinj 36060	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.20.16  Rings
Syntax	crngo 36061	Extend class notation with the class of all unital rings.
class RingOps
Definition	df-rngo 36062*	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 36063	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 36064*	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 36065*	Conditions that determine a ring. (Changed label from isringd 19833 to isrngod 36065-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 36066*	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 36067	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 36068	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 36069*	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 36070*	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 → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))
Theorem	rngodi 36071	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 36072	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 36073	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 36074*	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 36075	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 36076	In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
⊢ (⟨𝐺, 𝐻⟩ ∈ RingOps → 𝐺 ∈ AbelOp)
Theorem	rngogrpo 36077	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 36078	The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → 𝑋 ≠ ∅)
Theorem	rngogcl 36079	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 36080	The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))
Theorem	rngoaass 36081	The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))
Theorem	rngoa32 36082	The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵))
Theorem	rngoa4 36083	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 36084	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 36085	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 36086	A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → 𝑍 ∈ 𝑋)
Theorem	rngo0rid 36087	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 36088	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 36089	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 36090	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 36091	Obsolete as of 25-Jan-2020. Use ring1zr 20555 or srg1zr 19774 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 36092	Obsolete as of 25-Jan-2020. Use rngen1zr 20556 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 36093	Obsolete as of 25-Jan-2020. Use ringen1zr 20557 or srgen1zr 19775 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 36094	A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋)
Theorem	rngoaddneg1 36095	Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑍)
Theorem	rngoaddneg2 36096	Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑍)
Theorem	rngosub 36097	Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁‘𝐵)))
Theorem	rngmgmbs4 36098*	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 36099	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 36100	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 𝐻)