P. 205 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20401-20500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rhmf 20401	A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐵⟶𝐶)
Theorem	rhmmul 20402	A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵)))
Theorem	isrhm2d 20403*	Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	isrhmd 20404*	Demonstration of ring homomorphism. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ⨣ = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	rhm1 20405	Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘ 1 ) = 𝑁)
Theorem	idrhm 20406	The identity homomorphism on a ring. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → ( I ↾ 𝐵) ∈ (𝑅 RingHom 𝑅))
Theorem	rhmf1o 20407	A ring homomorphism is bijective iff its converse is also a ring homomorphism. (Contributed by AV, 22-Oct-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 RingHom 𝑅)))
Theorem	isrim 20408	An isomorphism of rings is a bijective homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 12-Jan-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	isrimOLD 20409	Obsolete version of isrim 20408 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶)))
Theorem	rimf1o 20410	An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	rimrhmOLD 20411	Obsolete version of rimrhm 20412 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	rimrhm 20412	A ring isomorphism is a homomorphism. Compare gimghm 19203. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	rimgim 20413	An isomorphism of rings is an isomorphism of their additive groups. (Contributed by AV, 24-Dec-2019.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 GrpIso 𝑆))
Theorem	rimisrngim 20414	Each unital ring isomorphism is a non-unital ring isomorphism. (Contributed by AV, 30-Mar-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RngIso 𝑆))
Theorem	rhmfn 20415	The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.)
⊢ RingHom Fn (Ring × Ring)
Theorem	rhmval 20416	The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.)
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))))
Theorem	rhmco 20417	The composition of ring homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 RingHom 𝑈) ∧ 𝐺 ∈ (𝑆 RingHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RingHom 𝑈))
Theorem	pwsco1rhm 20418*	Right composition with a function on the index sets yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐴)    &   ⊢ 𝑍 = (𝑅 ↑s 𝐵)    &   ⊢ 𝐶 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 RingHom 𝑌))
Theorem	pwsco2rhm 20419*	Left composition with a ring homomorphism yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐴)    &   ⊢ 𝑍 = (𝑆 ↑s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    ⇒   ⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 RingHom 𝑍))
Theorem	brric 20420	The relation "is isomorphic to" for (unital) rings. (Contributed by AV, 24-Dec-2019.)
⊢ (𝑅 ≃𝑟 𝑆 ↔ (𝑅 RingIso 𝑆) ≠ ∅)
Theorem	brrici 20421	Prove isomorphic by an explicit isomorphism. (Contributed by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑅 ≃𝑟 𝑆)
Theorem	brric2 20422*	The relation "is isomorphic to" for (unital) rings. This theorem corresponds to Definition df-risc 37984 of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019.)
⊢ (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingIso 𝑆)))
Theorem	ricgic 20423	If two rings are (ring) isomorphic, their additive groups are (group) isomorphic. (Contributed by AV, 24-Dec-2019.)
⊢ (𝑅 ≃𝑟 𝑆 → 𝑅 ≃𝑔 𝑆)
Theorem	rhmdvdsr 20424	A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ / = (∥r‘𝑆)    ⇒   ⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ∥ 𝐵) → (𝐹‘𝐴) / (𝐹‘𝐵))
Theorem	rhmopp 20425	A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((oppr‘𝑅) RingHom (oppr‘𝑆)))
Theorem	elrhmunit 20426	Ring homomorphisms preserve unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.)
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴) ∈ (Unit‘𝑆))
Theorem	rhmunitinv 20427	Ring homomorphisms preserve the inverse of unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.)
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘((invr‘𝑅)‘𝐴)) = ((invr‘𝑆)‘(𝐹‘𝐴)))
10.3.11  Nonzero rings and zero rings
Syntax	cnzr 20428	The class of nonzero rings.
class NzRing
Definition	df-nzr 20429	A nonzero or nontrivial ring is a ring with at least two values, or equivalently where 1 and 0 are different. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)}
Theorem	isnzr 20430	Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 ≠ 0 ))
Theorem	nzrnz 20431	One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing → 1 ≠ 0 )
Theorem	nzrring 20432	A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.)
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
Theorem	nzrringOLD 20433	Obsolete version of nzrring 20432 as of 23-Feb-2025. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
Theorem	isnzr2 20434	Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 2o ≼ 𝐵))
Theorem	isnzr2hash 20435	Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 20434. (Contributed by AV, 14-Apr-2019.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 < (♯‘𝐵)))
Theorem	nzrpropd 20436*	If two structures have the same components (properties), one is a nonzero ring iff the other one is. (Contributed by SN, 21-Jun-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ NzRing ↔ 𝐿 ∈ NzRing))
Theorem	opprnzrb 20437	The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 20438. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing ↔ 𝑂 ∈ NzRing)
Theorem	opprnzr 20438	The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing → 𝑂 ∈ NzRing)
Theorem	ringelnzr 20439	A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 13-Jun-2015.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ∖ { 0 })) → 𝑅 ∈ NzRing)
Theorem	nzrunit 20440	A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ 0 )
Theorem	0ringnnzr 20441	A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019.)
⊢ (𝑅 ∈ Ring → ((♯‘(Base‘𝑅)) = 1 ↔ ¬ 𝑅 ∈ NzRing))
Theorem	0ring 20442	If a ring has only one element, it is the zero ring. According to Wikipedia ("Zero ring", 14-Apr-2019, https://en.wikipedia.org/wiki/Zero_ring): "The zero ring, denoted {0} or simply 0, consists of the one-element set {0} with the operations + and * defined so that 0 + 0 = 0 and 0 * 0 = 0.". (Contributed by AV, 14-Apr-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 𝐵 = { 0 })
Theorem	0ringdif 20443	A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ (Ring ∖ NzRing) ↔ (𝑅 ∈ Ring ∧ 𝐵 = { 0 }))
Theorem	0ringbas 20444	The base set of a zero ring, a ring which is not a nonzero ring, is the singleton of the zero element. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ (Ring ∖ NzRing) → 𝐵 = { 0 })
Theorem	0ring01eq 20445	In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-Apr-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 0 = 1 )
Theorem	01eq0ring 20446	If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019.) (Proof shortened by SN, 23-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 })
Theorem	01eq0ringOLD 20447	Obsolete version of 01eq0ring 20446 as of 23-Feb-2025. (Contributed by AV, 16-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 })
Theorem	0ring01eqbi 20448	In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by AV, 23-Jan-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐵 ≈ 1o ↔ 1 = 0 ))
Theorem	0ring1eq0 20449	In a zero ring, a ring which is not a nonzero ring, the ring unity equals the zero element. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ (Ring ∖ NzRing) → 1 = 0 )
Theorem	c0rhm 20450*	The constant mapping to zero is a ring homomorphism from any ring to the zero ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Ring ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑆 RingHom 𝑇))
Theorem	c0rnghm 20451*	The constant mapping to zero is a non-unital ring homomorphism from any non-unital ring to the zero ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑆 RngHom 𝑇))
Theorem	zrrnghm 20452*	The constant mapping to zero is a non-unital ring homomorphism from the zero ring to any non-unital ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑇 RngHom 𝑆))
Theorem	nrhmzr 20453	There is no ring homomorphism from the zero ring into a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ((𝑍 ∈ (Ring ∖ NzRing) ∧ 𝑅 ∈ NzRing) → (𝑍 RingHom 𝑅) = ∅)
10.3.12  Local rings
Syntax	clring 20454	Extend class notation with class of all local rings.
class LRing
Definition	df-lring 20455*	A local ring is a nonzero ring where for any two elements summing to one, at least one is invertible. Any field is a local ring; the ring of integers is an example of a ring which is not a local ring. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
⊢ LRing = {𝑟 ∈ NzRing ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑥(+g‘𝑟)𝑦) = (1r‘𝑟) → (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟)))}
Theorem	islring 20456*	The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ LRing ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 1 → (𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈))))
Theorem	lringnzr 20457	A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
⊢ (𝑅 ∈ LRing → 𝑅 ∈ NzRing)
Theorem	lringring 20458	A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
⊢ (𝑅 ∈ LRing → 𝑅 ∈ Ring)
Theorem	lringnz 20459	A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ LRing → 1 ≠ 0 )
Theorem	lringuplu 20460	If the sum of two elements of a local ring is invertible, then at least one of the summands must be invertible. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ LRing)    &   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈))
10.3.13  Subrings
10.3.13.1  Subrings of non-unital rings
Syntax	csubrng 20461	Extend class notation with all subrings of a non-unital ring.
class SubRng
Definition	df-subrng 20462*	Define a subring of a non-unital ring as a set of elements that is a non-unital ring in its own right. In this section, a subring of a non-unital ring is simply called "subring", unless it causes any ambiguity with SubRing. (Contributed by AV, 14-Feb-2025.)
⊢ SubRng = (𝑤 ∈ Rng ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Rng})
Theorem	issubrng 20463	The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) ↔ (𝑅 ∈ Rng ∧ (𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵))
Theorem	subrngss 20464	A subring is a subset. (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 ⊆ 𝐵)
Theorem	subrngid 20465	Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝐵 ∈ (SubRng‘𝑅))
Theorem	subrngrng 20466	A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝑆 ∈ Rng)
Theorem	subrngrcl 20467	Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.)
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝑅 ∈ Rng)
Theorem	subrngsubg 20468	A subring is a subgroup. (Contributed by AV, 14-Feb-2025.)
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
Theorem	subrngringnsg 20469	A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.)
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 ∈ (NrmSGrp‘𝑅))
Theorem	subrngbas 20470	Base set of a subring structure. (Contributed by AV, 14-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	subrng0 20471	A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 0 = (0g‘𝑆))
Theorem	subrngacl 20472	A subring is closed under addition. (Contributed by AV, 14-Feb-2025.)
⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴)
Theorem	subrngmcl 20473	A subring is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 20500. (Revised by AV, 14-Feb-2025.)
⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴)
Theorem	issubrng2 20474*	Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → (𝐴 ∈ (SubRng‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)))
Theorem	opprsubrng 20475	Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (SubRng‘𝑅) = (SubRng‘𝑂)
Theorem	subrngint 20476	The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.)
⊢ ((𝑆 ⊆ (SubRng‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubRng‘𝑅))
Theorem	subrngin 20477	The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.)
⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝐵 ∈ (SubRng‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRng‘𝑅))
Theorem	subrngmre 20478	The subrings of a non-unital ring are a Moore system. (Contributed by AV, 15-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → (SubRng‘𝑅) ∈ (Moore‘𝐵))
Theorem	subsubrng 20479	A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → (𝐵 ∈ (SubRng‘𝑆) ↔ (𝐵 ∈ (SubRng‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	subsubrng2 20480	The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → (SubRng‘𝑆) = ((SubRng‘𝑅) ∩ 𝒫 𝐴))
Theorem	rhmimasubrnglem 20481*	Lemma for rhmimasubrng 20482: Modified part of mhmima 18759. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 16-Feb-2025.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubRng‘𝑅)) → ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋))
Theorem	rhmimasubrng 20482	The homomorphic image of a subring is a subring. (Contributed by AV, 16-Feb-2025.)
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRng‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubRng‘𝑁))
Theorem	cntzsubrng 20483	Centralizers in a non-unital ring are subrings. (Contributed by AV, 17-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRng‘𝑅))
Theorem	subrngpropd 20484*	If two structures have the same ring components (properties), they have the same set of subrings. (Contributed by AV, 17-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (SubRng‘𝐾) = (SubRng‘𝐿))
10.3.13.2  Subrings of unital rings
Syntax	csubrg 20485	Extend class notation with all subrings of a ring.
class SubRing
Definition	df-subrg 20486*	Define a subring of a ring as a set of elements that is a ring in its own right and contains the multiplicative identity. The additional constraint is necessary because the multiplicative identity of a ring, unlike the additive identity of a ring/group or the multiplicative identity of a field, cannot be identified by a local property. Thus, it is possible for a subset of a ring to be a ring while not containing the true identity if it contains a false identity. For instance, the subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity ⟨1, 0⟩ which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ SubRing = (𝑤 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ((𝑤 ↾s 𝑠) ∈ Ring ∧ (1r‘𝑤) ∈ 𝑠)})
Theorem	issubrg 20487	The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof shortened by AV, 12-Oct-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))
Theorem	subrgss 20488	A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵)
Theorem	subrgid 20489	Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅))
Theorem	subrgring 20490	A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)
Theorem	subrgcrng 20491	A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ CRing)
Theorem	subrgrcl 20492	Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
Theorem	subrgsubg 20493	A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
Theorem	subrgsubrng 20494	A subring of a unital ring is a subring of a non-unital ring. (Contributed by AV, 30-Mar-2025.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubRng‘𝑅))
Theorem	subrg0 20495	A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 0 = (0g‘𝑆))
Theorem	subrg1cl 20496	A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴)
Theorem	subrgbas 20497	Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	subrg1 20498	A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 = (1r‘𝑆))
Theorem	subrgacl 20499	A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴)
Theorem	subrgmcl 20500	A subring is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) (Proof shortened by AV, 30-Mar-2025.)
⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴)