P. 337 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rloc0g 33601	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 33602	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 33603*	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 33604	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 33605*	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 33606	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 33607	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 33608	A product over a domain is zero exactly when one of the factors is zero. Generalization of domneq0 20818 for any number of factors. See also domnprodn0 33607. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹) = 0 ↔ 0 ∈ ran 𝐹))
Theorem	domnpropd 33609*	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 33610*	If two structures have the same components (properties), one is a integral domain iff the other one is. See also domnpropd 33609. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn))
Theorem	idomrcan 33611	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	1rrg 33612	The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 1 ∈ 𝐸)
Theorem	rrgsubm 33613	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 33614	A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn)
Theorem	subridom 33615	A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn)
Theorem	subrfld 33616	A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn)
Theorem	ricnzr1 33617	A ring isomorphism maps a nonzero ring to a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing) → 𝑆 ∈ NzRing)
Theorem	ricdomn1 33618	A ring isomorphism maps a domain to a domain. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn) → 𝑆 ∈ Domn)
Theorem	ricdomn 33619	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 33620	Declare the syntax for the Euclidean function index extractor.
class EuclF
Definition	df-euf 33621	Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33623 instead. (New usage is discouraged.)
⊢ EuclF = Slot ;21
Theorem	eufndx 33622	Index value of the Euclidean function slot. Use ndxarg 17262. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.)
⊢ (EuclF‘ndx) = ;21
Theorem	eufid 33623	Utility theorem: index-independent form of df-euf 33621. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ EuclF = Slot (EuclF‘ndx)
Syntax	cedom 33624	Declare the syntax for the Euclidean Domain.
class EDomn
Definition	df-edom 33625*	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	rndrhmcl 33626	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 33627	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 33628	A subring of a sub-division-ring is a sub-division-ring. See also subsubrg 20708. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝐵 ∈ (SubDRing‘𝑆) ↔ (𝐵 ∈ (SubDRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	sdrgdvcl 33629	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 33630	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 33631	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 33632	Syntax for the field of fractions of a given integral domain.
class Frac
Definition	df-frac 33633	Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.)
⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟)))
Theorem	fracval 33634	Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.)
⊢ ( Frac ‘𝑅) = (𝑅 RLocal (RLReg‘𝑅))
Theorem	fracbas 33635	The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐹 = ( Frac ‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝐸)    ⇒   ⊢ ((𝐵 × 𝐸) / ∼ ) = (Base‘𝐹)
Theorem	fracerl 33636	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 33637*	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 33638	The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field)
Theorem	idomsubr 33639*	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 33640	Syntax for a function generating sub-fields.
class fldGen
Definition	df-fldgen 33641*	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 33644). If the base structure is a field, this is a subfield (see fldgenfld 33650 and fldsdrgfld 20912). 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 33642*	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 33643	The field generated by a set of elements contains those elements. See lspssid 21117. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ (𝐹 fldGen 𝑆))
Theorem	fldgensdrg 33644	A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹))
Theorem	fldgenssv 33645	A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵)
Theorem	fldgenss 33646	Generated subfields preserve subset ordering. ( see lspss 21116 and spanss 31711) (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆))
Theorem	fldgenidfld 33647	The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹))    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆)
Theorem	fldgenssp 33648	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 33649	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 33650	A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field)
Theorem	primefldgen1 33651	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 33652	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 33653	A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ 𝑈 = (Unit‘𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑆)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶))))
Theorem	kerunit 33654	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 33655	Extend class notation with the scalar restriction operation.
class ↾v
Definition	df-resv 33656*	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 33657	The scalar restriction is a proper operator, so it can be used with ovprc1 7451. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ Rel dom ↾v
Theorem	resvval 33658	Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)))
Theorem	resvid2 33659	General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊)
Theorem	resvval2 33660	Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))
Theorem	resvsca 33661	Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅))
Theorem	resvlem 33662	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 33663	Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻))
Theorem	resvplusg 33664	+g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))
Theorem	resvvsca 33665	·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻))
Theorem	resvmulr 33666	.r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻))
Theorem	resv0g 33667	0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻))
Theorem	resv1r 33668	1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 1 = (1r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻))
Theorem	resvcmn 33669	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 33670	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 33671	The complex numbers form a field. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ ℂfld ∈ Field
Theorem	reofld 33672	The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ℝfld ∈ oField
Theorem	nn0omnd 33673	The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ oMnd
Theorem	gsumind 33674	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 33675	The field of the real numbers is Archimedean. See also arch 12507. (Contributed by Thierry Arnoux, 9-Apr-2018.)
⊢ ℝfld ∈ Archi
Theorem	nn0archi 33676	The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ Archi
Theorem	xrge0slmod 33677	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 33678*	The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺))    &   ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺))    &   ⊢ 0 = (0g‘𝑁)    ⇒   ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺)
Theorem	eqgvscpbl 33679	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 33680*	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 33681	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 33682*	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 33683*	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 33684*	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 33685*	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 33686*	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 33687	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 33688*	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 33689	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)
21.3.10.34  The ring of integers modulo ` N `
Theorem	znfermltl 33690	Fermat's little theorem in ℤ/nℤ. (Contributed by Thierry Arnoux, 24-Jul-2024.)
⊢ 𝑍 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑍))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵) → (𝑃 ↑ 𝐴) = 𝐴)
21.3.10.35  Independent sets and families
Theorem	islinds5 33691*	A set is linearly independent if and only if it has no non-trivial representations of zero. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑂 = (0g‘𝑊)    &   ⊢ 0 = (0g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵) → (𝑉 ∈ (LIndS‘𝑊) ↔ ∀𝑎 ∈ (𝐾 ↑m 𝑉)((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣))) = 𝑂) → 𝑎 = (𝑉 × { 0 }))))
Theorem	ellspds 33692*	Variation on ellspd 21963. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝑁 = (LSpan‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣))))))
Theorem	0ellsp 33693	Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑆))
Theorem	0nellinds 33694	The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.)
⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ¬ 0 ∈ 𝐹)
Theorem	elrsp 33695*	Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑁 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝐼) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝐼)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑖 ∈ 𝐼 ↦ ((𝑎‘𝑖) · 𝑖))))))
Theorem	ellpi 33696	Elementhood in a left principal ideal in terms of the "divides" relation. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝐾‘{𝑋}) ↔ 𝑋 ∥ 𝑌))
Theorem	lpirlidllpi 33697*	In a principal ideal ring, ideals are principal. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ LPIR)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥}))
Theorem	rspidlid 33698	The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐾‘𝐼) = 𝐼)
Theorem	lbslsp 33699*	Any element of a left module 𝑀 can be expressed as a linear combination of the elements of a basis 𝑉 of 𝑀. (Contributed by Thierry Arnoux, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    &   ⊢ (𝜑 → 𝑉 ∈ (LBasis‘𝑀))    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣))))))
Theorem	lindssn 33700	Any singleton of a nonzero element is an independent set. (Contributed by Thierry Arnoux, 5-Aug-2023.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LIndS‘𝑊))