P. 335 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33401-33500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	erld2 33401*	Main property of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑆)    &   ⊢ (𝜑 → [⟨𝑋, 𝑌⟩] ∼ = [⟨𝑍, 𝑊⟩] ∼ )    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ 𝑆 (𝑡 · (𝑋 · 𝑊)) = (𝑡 · (𝑍 · 𝑌)))
Theorem	elrlocbasi 33402*	Membership in the basis of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑋 ∈ ((𝐵 × 𝑆) / ∼ ))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝑆 𝑋 = [⟨𝑎, 𝑏⟩] ∼ )
Theorem	rlocbas 33403	The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ 𝑊 = (𝐵 × 𝑆)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑊 / ∼ ) = (Base‘𝐿))
Theorem	rlocaddval 33404	Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑆)    &   ⊢ ⊕ = (+g‘𝐿)    ⇒   ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊕ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨((𝐸 · 𝐻) + (𝐹 · 𝐺)), (𝐺 · 𝐻)⟩] ∼ )
Theorem	rlocmulval 33405	Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑆)    &   ⊢ ⊗ = (.r‘𝐿)    ⇒   ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊗ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] ∼ )
Theorem	rloccring 33406	The ring localization 𝐿 of a commutative ring 𝑅 by a multiplicatively closed set 𝑆 is itself a commutative ring. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    ⇒   ⊢ (𝜑 → 𝐿 ∈ CRing)
Theorem	rloc0g 33407	The zero of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ 𝑂 = [⟨ 0 , 1 ⟩] ∼    ⇒   ⊢ (𝜑 → 𝑂 = (0g‘𝐿))
Theorem	rloc1r 33408	The multiplicative identity of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ 𝐼 = [⟨ 1 , 1 ⟩] ∼    ⇒   ⊢ (𝜑 → 𝐼 = (1r‘𝐿))
Theorem	rlocf1 33409*	The embedding 𝐹 of a ring 𝑅 into its localization 𝐿. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [⟨𝑥, 1 ⟩] ∼ )    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝑆 ⊆ (RLReg‘𝑅))    ⇒   ⊢ (𝜑 → (𝐹:𝐵–1-1→((𝐵 × 𝑆) / ∼ ) ∧ 𝐹 ∈ (𝑅 RingHom 𝐿)))
Theorem	rlocinvunit 33410	In the localization of a ring 𝑅 at 𝑆, inverses of elements of 𝑆 are units. (Contributed by Thierry Arnoux, 6-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ 𝑊 = (Unit‘𝐿)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    ⇒   ⊢ (𝜑 → [⟨ 1 , 𝑄⟩] ∼ ∈ 𝑊)
Theorem	rlocisunit 33411*	Characterize the units of the localization 𝐿 of a ring 𝑅 at 𝑆 as the elements with a "numerator" 𝑃 in the saturation 𝑇 of 𝑆. (Contributed by Thierry Arnoux, 6-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ 𝑊 = (Unit‘𝐿)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    &   ⊢ 𝑇 = {𝑟 ∈ 𝐵 ∣ ∃𝑠 ∈ 𝐵 (𝑟 · 𝑠) ∈ 𝑆}    ⇒   ⊢ (𝜑 → ([⟨𝑃, 𝑄⟩] ∼ ∈ 𝑊 ↔ 𝑃 ∈ 𝑇))
21.3.10.22  Integral Domains
Theorem	domnmuln0rd 33412	In a domain, factors of a nonzero product are nonzero. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 · 𝑌) ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ))
Theorem	domnprodn0 33413	In a domain, a finite product of nonzero terms is nonzero. (Contributed by Thierry Arnoux, 6-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐹 ∈ Word (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 )
Theorem	domnprodeq0 33414	A product over a domain is zero exactly when one of the factors is zero. Generalization of domneq0 20730 for any number of factors. See also domnprodn0 33413. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹) = 0 ↔ 0 ∈ ran 𝐹))
Theorem	domnpropd 33415*	If two structures have the same components (properties), one is a domain iff the other one is. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Domn ↔ 𝐿 ∈ Domn))
Theorem	idompropd 33416*	If two structures have the same components (properties), one is a integral domain iff the other one is. See also domnpropd 33415. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn))
Theorem	idomrcan 33417	Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof shortened by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	domnlcanOLD 33418	Obsolete version of domnlcan 20743 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑌 = 𝑍)
Theorem	domnlcanbOLD 33419	Obsolete version of domnlcanb 20742 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 8-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = (𝑋 · 𝑍) ↔ 𝑌 = 𝑍))
Theorem	idomrcanOLD 33420	Obsolete version of idomrcan 33417 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → (𝑌 · 𝑋) = (𝑍 · 𝑋))    ⇒   ⊢ (𝜑 → 𝑌 = 𝑍)
Theorem	1rrg 33421	The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 1 ∈ 𝐸)
Theorem	rrgsubm 33422	The left regular elements of a ring form a submonoid of the multiplicative group. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝐸 ∈ (SubMnd‘𝑀))
Theorem	subrdom 33423	A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn)
Theorem	subridom 33424	A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn)
Theorem	subrfld 33425	A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn)
Theorem	ricnzr1 33426	A ring isomorphism maps a nonzero ring to a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing) → 𝑆 ∈ NzRing)
Theorem	ricdomn1 33427	A ring isomorphism maps a domain to a domain. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn) → 𝑆 ∈ Domn)
Theorem	ricdomn 33428	A ring is a domain if and only if an isomorphic ring is a domain. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ Domn ↔ 𝑆 ∈ Domn))
21.3.10.23  Euclidean Domains
Syntax	ceuf 33429	Declare the syntax for the Euclidean function index extractor.
class EuclF
Definition	df-euf 33430	Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33432 instead. (New usage is discouraged.)
⊢ EuclF = Slot ;21
Theorem	eufndx 33431	Index value of the Euclidean function slot. Use ndxarg 17208. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.)
⊢ (EuclF‘ndx) = ;21
Theorem	eufid 33432	Utility theorem: index-independent form of df-euf 33430. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ EuclF = Slot (EuclF‘ndx)
Syntax	cedom 33433	Declare the syntax for the Euclidean Domain.
class EDomn
Definition	df-edom 33434*	Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))}
21.3.10.24  Division Rings
Theorem	ringinveu 33435	If a ring unit element 𝑋 admits both a left inverse 𝑌 and a right inverse 𝑍, they are equal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 · 𝑋) = 1 )    &   ⊢ (𝜑 → (𝑋 · 𝑍) = 1 )    ⇒   ⊢ (𝜑 → 𝑍 = 𝑌)
Theorem	isdrng4 33436*	A division ring is a ring in which 1 ≠ 0 and every nonzero element has a left and right inverse. (Contributed by Thierry Arnoux, 2-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝑅 ∈ DivRing ↔ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))))
Theorem	rndrhmcl 33437	The image of a division ring by a ring homomorphism is a division ring. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝑅 = (𝑁 ↾s ran 𝐹)    &   ⊢ 0 = (0g‘𝑁)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁))    &   ⊢ (𝜑 → ran 𝐹 ≠ { 0 })    &   ⊢ (𝜑 → 𝑀 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
21.3.10.25  The field of rational numbers
Theorem	qfld 33438	The field of rational numbers is a field. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 𝑄 ∈ Field
21.3.10.26  Subfields
Theorem	subsdrg 33439	A subring of a sub-division-ring is a sub-division-ring. See also subsubrg 20620. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝐵 ∈ (SubDRing‘𝑆) ↔ (𝐵 ∈ (SubDRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	sdrgdvcl 33440	A sub-division-ring is closed under the ring division operation. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ / = (/r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 / 𝑌) ∈ 𝐴)
Theorem	sdrginvcl 33441	A sub-division-ring is closed under the ring inverse operation. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubDRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐴)
Theorem	primefldchr 33442	The characteristic of a prime field is the same as the characteristic of the main field. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝑃 = (𝑅 ↾s ∩ (SubDRing‘𝑅))    ⇒   ⊢ (𝑅 ∈ DivRing → (chr‘𝑃) = (chr‘𝑅))
21.3.10.27  Field of fractions
Syntax	cfrac 33443	Syntax for the field of fractions of a given integral domain.
class Frac
Definition	df-frac 33444	Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.)
⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟)))
Theorem	fracval 33445	Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.)
⊢ ( Frac ‘𝑅) = (𝑅 RLocal (RLReg‘𝑅))
Theorem	fracbas 33446	The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐹 = ( Frac ‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝐸)    ⇒   ⊢ ((𝐵 × 𝐸) / ∼ ) = (Base‘𝐹)
Theorem	fracerl 33447	Rewrite the ring localization equivalence relation in the case of a field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL (RLReg‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (RLReg‘𝑅))    &   ⊢ (𝜑 → 𝐻 ∈ (RLReg‘𝑅))    ⇒   ⊢ (𝜑 → (⟨𝐸, 𝐹⟩ ∼ ⟨𝐺, 𝐻⟩ ↔ (𝐸 · 𝐻) = (𝐺 · 𝐹)))
Theorem	fracf1 33448*	The embedding of a commutative ring 𝑅 into its field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ∼ = (𝑅 ~RL 𝐸)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [⟨𝑥, 1 ⟩] ∼ )    ⇒   ⊢ (𝜑 → (𝐹:𝐵–1-1→((𝐵 × 𝐸) / ∼ ) ∧ 𝐹 ∈ (𝑅 RingHom ( Frac ‘𝑅))))
Theorem	fracfld 33449	The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field)
Theorem	idomsubr 33450*	Every integral domain is isomorphic with a subring of some field. (Proposed by Gerard Lang, 10-May-2025.) (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ Field ∃𝑠 ∈ (SubRing‘𝑓)𝑅 ≃𝑟 (𝑓 ↾s 𝑠))
21.3.10.28  Field extensions generated by a set
Syntax	cfldgen 33451	Syntax for a function generating sub-fields.
class fldGen
Definition	df-fldgen 33452*	Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg 33455). If the base structure is a field, this is a subfield (see fldgenfld 33461 and fldsdrgfld 20820). In general this will be used in the context of fields, hence the name fldGen. (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025.)
⊢ fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎})
Theorem	fldgenval 33453*	Value of the field generating function: (𝐹 fldGen 𝑆) is the smallest sub-division-ring of 𝐹 containing 𝑆. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) = ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎})
Theorem	fldgenssid 33454	The field generated by a set of elements contains those elements. See lspssid 21025. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ (𝐹 fldGen 𝑆))
Theorem	fldgensdrg 33455	A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹))
Theorem	fldgenssv 33456	A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵)
Theorem	fldgenss 33457	Generated subfields preserve subset ordering. ( see lspss 21024 and spanss 31490) (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆))
Theorem	fldgenidfld 33458	The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹))    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆)
Theorem	fldgenssp 33459	The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ 𝑆)
Theorem	fldgenid 33460	The subfield of a field 𝐹 generated by the whole base set of 𝐹 is 𝐹 itself. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝐵) = 𝐵)
Theorem	fldgenfld 33461	A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field)
Theorem	primefldgen1 33462	The prime field of a division ring is the subfield generated by the multiplicative identity element. In general, we should write "prime division ring", but since most later usages are in the case where the ambient ring is commutative, we keep the term "prime field". (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → ∩ (SubDRing‘𝑅) = (𝑅 fldGen { 1 }))
Theorem	1fldgenq 33463	The field of rational numbers ℚ is generated by 1 in ℂfld, that is, ℚ is the prime field of ℂfld. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ (ℂfld fldGen {1}) = ℚ
21.3.10.29  Ring homomorphisms - misc additions
Theorem	rhmdvd 33464	A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ 𝑈 = (Unit‘𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑆)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶))))
Theorem	kerunit 33465	If a unit element lies in the kernel of a ring homomorphism, then 0 = 1, i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝑈 ∩ (◡𝐹 “ { 0 })) ≠ ∅) → 1 = 0 )
21.3.10.30  Scalar restriction operation
Syntax	cresv 33466	Extend class notation with the scalar restriction operation.
class ↾v
Definition	df-resv 33467*	Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.)
⊢ ↾v = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)))
Theorem	reldmresv 33468	The scalar restriction is a proper operator, so it can be used with ovprc1 7424. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ Rel dom ↾v
Theorem	resvval 33469	Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)))
Theorem	resvid2 33470	General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊)
Theorem	resvval2 33471	Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))
Theorem	resvsca 33472	Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅))
Theorem	resvlem 33473	Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐶 = (𝐸‘𝑊)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅))
Theorem	resvbas 33474	Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻))
Theorem	resvplusg 33475	+g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))
Theorem	resvvsca 33476	·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻))
Theorem	resvmulr 33477	.r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻))
Theorem	resv0g 33478	0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻))
Theorem	resv1r 33479	1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 1 = (1r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻))
Theorem	resvcmn 33480	Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd))
21.3.10.31  The commutative ring of gaussian integers
Theorem	gzcrng 33481	The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.)
⊢ (ℂfld ↾s ℤ[i]) ∈ CRing
21.3.10.32  The archimedean ordered field of real numbers
Theorem	cnfldfld 33482	The complex numbers form a field. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ ℂfld ∈ Field
Theorem	reofld 33483	The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ℝfld ∈ oField
Theorem	nn0omnd 33484	The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ oMnd
Theorem	gsumind 33485	The group sum of an indicator function of the set 𝐴 gives the size of 𝐴. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → (ℂfld Σg ((𝟭‘𝑂)‘𝐴)) = (♯‘𝐴))
Theorem	rearchi 33486	The field of the real numbers is Archimedean. See also arch 12468. (Contributed by Thierry Arnoux, 9-Apr-2018.)
⊢ ℝfld ∈ Archi
Theorem	nn0archi 33487	The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ Archi
Theorem	xrge0slmod 33488	The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞))    &   ⊢ 𝑊 = (𝐺 ↾v (0[,)+∞))    ⇒   ⊢ 𝑊 ∈ SLMod
21.3.10.33  The quotient map and quotient modules
Theorem	qusker 33489*	The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺))    &   ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺))    &   ⊢ 0 = (0g‘𝑁)    ⇒   ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺)
Theorem	eqgvscpbl 33490	The left coset equivalence relation is compatible with the scalar multiplication operation. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ∼ = (𝑀 ~QG 𝐺)    &   ⊢ 𝑆 = (Base‘(Scalar‘𝑀))    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 ∼ 𝑌 → (𝐾 · 𝑋) ∼ (𝐾 · 𝑌)))
Theorem	qusvscpbl 33491*	The quotient map distributes over the scalar multiplication. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ∼ = (𝑀 ~QG 𝐺)    &   ⊢ 𝑆 = (Base‘(Scalar‘𝑀))    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑆)    &   ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺))    &   ⊢ ∙ = ( ·𝑠 ‘𝑁)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝑀 ~QG 𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑈) = (𝐹‘𝑉) → (𝐹‘(𝐾 · 𝑈)) = (𝐹‘(𝐾 · 𝑉))))
Theorem	qusvsval 33492	Value of the scalar multiplication operation on the quotient structure. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ∼ = (𝑀 ~QG 𝐺)    &   ⊢ 𝑆 = (Base‘(Scalar‘𝑀))    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑆)    &   ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺))    &   ⊢ ∙ = ( ·𝑠 ‘𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐾 ∙ [𝑋](𝑀 ~QG 𝐺)) = [(𝐾 · 𝑋)](𝑀 ~QG 𝐺))
Theorem	imaslmod 33493*	The image structure of a left module is a left module. (Contributed by Thierry Arnoux, 15-May-2023.)
⊢ (𝜑 → 𝑁 = (𝐹 “s 𝑀))    &   ⊢ 𝑉 = (Base‘𝑀)    &   ⊢ 𝑆 = (Base‘(Scalar‘𝑀))    &   ⊢ + = (+g‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 · 𝑎)) = (𝐹‘(𝑘 · 𝑏))))    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑁 ∈ LMod)
Theorem	imasmhm 33494*	Given a function 𝐹 with homomorphic properties, build the image of a monoid. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ + = (+g‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ (𝜑 → 𝑊 ∈ Mnd)    ⇒   ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Mnd ∧ 𝐹 ∈ (𝑊 MndHom (𝐹 “s 𝑊))))
Theorem	imasghm 33495*	Given a function 𝐹 with homomorphic properties, build the image of a group. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ + = (+g‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ (𝜑 → 𝑊 ∈ Grp)    ⇒   ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Grp ∧ 𝐹 ∈ (𝑊 GrpHom (𝐹 “s 𝑊))))
Theorem	imasrhm 33496*	Given a function 𝐹 with homomorphic properties, build the image of a ring. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ + = (+g‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ · = (.r‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑊 ∈ Ring)    ⇒   ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Ring ∧ 𝐹 ∈ (𝑊 RingHom (𝐹 “s 𝑊))))
Theorem	imaslmhm 33497*	Given a function 𝐹 with homomorphic properties, build the image of a left module. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ + = (+g‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 × 𝑎)) = (𝐹‘(𝑘 × 𝑏))))    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ × = ( ·𝑠 ‘𝑊)    ⇒   ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ LMod ∧ 𝐹 ∈ (𝑊 LMHom (𝐹 “s 𝑊))))
Theorem	quslmod 33498	If 𝐺 is a submodule in 𝑀, then 𝑁 = 𝑀 / 𝐺 is a left module, called the quotient module of 𝑀 by 𝐺. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺))    &   ⊢ 𝑉 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀))    ⇒   ⊢ (𝜑 → 𝑁 ∈ LMod)
Theorem	quslmhm 33499*	If 𝐺 is a submodule of 𝑀, then the "natural map" from elements to their cosets is a left module homomorphism from 𝑀 to 𝑀 / 𝐺. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺))    &   ⊢ 𝑉 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑀 LMHom 𝑁))
Theorem	quslvec 33500	If 𝑆 is a vector subspace in 𝑊, then 𝑄 = 𝑊 / 𝑆 is a vector space, called the quotient space of 𝑊 by 𝑆. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝑄 = (𝑊 /s (𝑊 ~QG 𝑆))    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑊))    ⇒   ⊢ (𝜑 → 𝑄 ∈ LVec)