P. 328 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32701-32800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ofldlt1 32701	In an ordered field, the ring unity is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ 0 = (0g‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ < = (lt‘𝐹)    ⇒   ⊢ (𝐹 ∈ oField → 0 < 1 )
Theorem	ofldchr 32702	The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018.) (Proof shortened by AV, 6-Oct-2020.)
⊢ (𝐹 ∈ oField → (chr‘𝐹) = 0)
Theorem	suborng 32703	Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oRing)
Theorem	subofld 32704	Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ((𝐹 ∈ oField ∧ (𝐹 ↾s 𝐴) ∈ Field) → (𝐹 ↾s 𝐴) ∈ oField)
Theorem	isarchiofld 32705*	Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐻 = (ℤRHom‘𝑊)    &   ⊢ < = (lt‘𝑊)    ⇒   ⊢ (𝑊 ∈ oField → (𝑊 ∈ Archi ↔ ∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)))
21.3.9.20  Ring homomorphisms - misc additions
Theorem	rhmdvd 32706	A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ 𝑈 = (Unit‘𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑆)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶))))
Theorem	kerunit 32707	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.9.21  Scalar restriction operation
Syntax	cresv 32708	Extend class notation with the scalar restriction operation.
class ↾v
Definition	df-resv 32709*	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 32710	The scalar restriction is a proper operator, so it can be used with ovprc1 7450. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ Rel dom ↾v
Theorem	resvval 32711	Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)))
Theorem	resvid2 32712	General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊)
Theorem	resvval2 32713	Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))
Theorem	resvsca 32714	Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅))
Theorem	resvlem 32715	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	resvlemOLD 32716	Obsolete version of resvlem 32715 as of 31-Oct-2024. Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐶 = (𝐸‘𝑊)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 ≠ 5    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅))
Theorem	resvbas 32717	Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻))
Theorem	resvbasOLD 32718	Obsolete proof of resvbas 32717 as of 31-Oct-2024. Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻))
Theorem	resvplusg 32719	+g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))
Theorem	resvplusgOLD 32720	Obsolete proof of resvplusg 32719 as of 31-Oct-2024. +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))
Theorem	resvvsca 32721	·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻))
Theorem	resvvscaOLD 32722	Obsolete proof of resvvsca 32721 as of 31-Oct-2024. ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻))
Theorem	resvmulr 32723	.r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻))
Theorem	resvmulrOLD 32724	Obsolete proof of resvmulr 32723 as of 31-Oct-2024. ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻))
Theorem	resv0g 32725	0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻))
Theorem	resv1r 32726	1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 1 = (1r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻))
Theorem	resvcmn 32727	Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd))
21.3.9.22  The commutative ring of gaussian integers
Theorem	gzcrng 32728	The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.)
⊢ (ℂfld ↾s ℤ[i]) ∈ CRing
21.3.9.23  The archimedean ordered field of real numbers
Theorem	reofld 32729	The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ℝfld ∈ oField
Theorem	nn0omnd 32730	The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ oMnd
Theorem	rearchi 32731	The field of the real numbers is Archimedean. See also arch 12473. (Contributed by Thierry Arnoux, 9-Apr-2018.)
⊢ ℝfld ∈ Archi
Theorem	nn0archi 32732	The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ Archi
Theorem	xrge0slmod 32733	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.9.24  The quotient map and quotient modules
Theorem	qusker 32734*	The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺))    &   ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺))    &   ⊢ 0 = (0g‘𝑁)    ⇒   ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺)
Theorem	eqgvscpbl 32735	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 32736*	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 32737	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 32738*	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 32739*	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 32740*	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 32741*	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 32742*	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 32743	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 32744*	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 32745	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)
Theorem	ecxpid 32746	The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ (𝑋 ∈ 𝐴 → [𝑋](𝐴 × 𝐴) = 𝐴)
Theorem	eqg0el 32747	Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ ∼ = (𝐺 ~QG 𝐻)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺)) → ([𝑋] ∼ = 𝐻 ↔ 𝑋 ∈ 𝐻))
Theorem	qsxpid 32748	The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.)
⊢ (𝐴 ≠ ∅ → (𝐴 / (𝐴 × 𝐴)) = {𝐴})
Theorem	qusxpid 32749	The Group quotient equivalence relation for the whole group is the cartesian product, i.e. all elements are in the same equivalence class. (Contributed by Thierry Arnoux, 16-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝐺 ~QG 𝐵) = (𝐵 × 𝐵))
Theorem	qustriv 32750	The quotient of a group 𝐺 by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐵))    ⇒   ⊢ (𝐺 ∈ Grp → (Base‘𝑄) = {𝐵})
Theorem	qustrivr 32751	Converse of qustriv 32750. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐻))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ (Base‘𝑄) = {𝐻}) → 𝐻 = 𝐵)
21.3.9.25  The ring of integers modulo ` N `
Theorem	fermltlchr 32752	A generalization of Fermat's little theorem in a commutative ring 𝐹 of prime characteristic. See fermltl 16721. (Contributed by Thierry Arnoux, 9-Jan-2024.)
⊢ 𝑃 = (chr‘𝐹)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐹))    &   ⊢ 𝐴 = ((ℤRHom‘𝐹)‘𝐸)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐸 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝑃 ↑ 𝐴) = 𝐴)
Theorem	znfermltl 32753	Fermat's little theorem in ℤ/nℤ. (Contributed by Thierry Arnoux, 24-Jul-2024.)
⊢ 𝑍 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑍))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵) → (𝑃 ↑ 𝐴) = 𝐴)
21.3.9.26  Independent sets and families
Theorem	islinds5 32754*	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 32755*	Variation on ellspd 21576. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝑁 = (LSpan‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣))))))
Theorem	0ellsp 32756	Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑆))
Theorem	0nellinds 32757	The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.)
⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ¬ 0 ∈ 𝐹)
Theorem	rspsnel 32758*	Membership in a principal ideal. Analogous to lspsnel 20758. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝐼 ∈ (𝐾‘{𝑋}) ↔ ∃𝑥 ∈ 𝐵 𝐼 = (𝑥 · 𝑋)))
Theorem	rspsnid 32759	A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ (𝐾‘{𝐺}))
Theorem	elrsp 32760*	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	rspidlid 32761	The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐾‘𝐼) = 𝐼)
Theorem	pidlnz 32762	A principal ideal generated by a nonzero element is not the zero ideal. (Contributed by Thierry Arnoux, 11-Apr-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐾‘{𝑋}) ≠ { 0 })
Theorem	dvdsruassoi 32763	If two elements 𝑋 and 𝑌 of a ring 𝑅 are unit multiples, then they are associates, i.e. each divides the other. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → (𝑉 · 𝑋) = 𝑌)    ⇒   ⊢ (𝜑 → (𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋))
Theorem	dvdsruasso 32764*	Two elements 𝑋 and 𝑌 of a ring 𝑅 are associates, i.e. each divides the other, iff they are unit multiples of each other. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌))
Theorem	dvdsrspss 32765	In a ring, an element 𝑋 divides 𝑌 iff the ideal generated by 𝑌 is a subset of the ideal generated by 𝑋 (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ (𝐾‘{𝑌}) ⊆ (𝐾‘{𝑋})))
Theorem	rspsnasso 32766	Two elements 𝑋 and 𝑌 of a ring 𝑅 are associates, i.e. each divides the other, iff the ideals they generate are equal. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ (𝐾‘{𝑌}) = (𝐾‘{𝑋})))
Theorem	lbslsp 32767*	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 32768	Any singleton of a nonzero element is an independent set. (Contributed by Thierry Arnoux, 5-Aug-2023.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LIndS‘𝑊))
Theorem	lindflbs 32769	Conditions for an independent family to be a basis. (Contributed by Thierry Arnoux, 21-Jul-2023.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑂 = (0g‘𝑊)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑆 ∈ NzRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼–1-1→𝐵)    ⇒   ⊢ (𝜑 → (ran 𝐹 ∈ (LBasis‘𝑊) ↔ (𝐹 LIndF 𝑊 ∧ (𝑁‘ran 𝐹) = 𝐵)))
Theorem	islbs5 32770*	An equivalent formulation of the basis predicate in a vector space, using a function 𝐹 for generating the base. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑂 = (0g‘𝑊)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑆 ∈ NzRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼–1-1→𝐵)    ⇒   ⊢ (𝜑 → (ran 𝐹 ∈ (LBasis‘𝑊) ↔ (∀𝑎 ∈ (𝐾 ↑m 𝐼)((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑎 ∘f · 𝐹)) = 𝑂) → 𝑎 = (𝐼 × { 0 })) ∧ (𝑁‘ran 𝐹) = 𝐵)))
Theorem	linds2eq 32771	Deduce equality of elements in an independent set. (Contributed by Thierry Arnoux, 18-Jul-2023.)
⊢ 𝐹 = (Base‘(Scalar‘𝑊))    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐵 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐾 ≠ 0 )    &   ⊢ (𝜑 → (𝐾 · 𝑋) = (𝐿 · 𝑌))    ⇒   ⊢ (𝜑 → (𝑋 = 𝑌 ∧ 𝐾 = 𝐿))
Theorem	lindfpropd 32772*	Property deduction for linearly independent families. (Contributed by Thierry Arnoux, 16-Jul-2023.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐿)))    &   ⊢ (𝜑 → (0g‘(Scalar‘𝐾)) = (0g‘(Scalar‘𝐿)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ (Base‘𝐾))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 LIndF 𝐾 ↔ 𝑋 LIndF 𝐿))
Theorem	lindspropd 32773*	Property deduction for linearly independent sets. (Contributed by Thierry Arnoux, 16-Jul-2023.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐿)))    &   ⊢ (𝜑 → (0g‘(Scalar‘𝐾)) = (0g‘(Scalar‘𝐿)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ (Base‘𝐾))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (LIndS‘𝐾) = (LIndS‘𝐿))
21.3.9.27  Subgroup sum / Sumset / Minkowski sum The sumset (also called the Minkowski sum) of two subsets 𝐴 and 𝐵, is defined to be the set of all sums of an element from 𝐴 with an element from 𝐵. The sumset operation can be used for both group (additive) operations and ring (multiplicative) operations.
Theorem	elgrplsmsn 32774*	Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝐴 ⊕ {𝑋}) ↔ ∃𝑥 ∈ 𝐴 𝑍 = (𝑥 + 𝑋)))
Theorem	lsmsnorb 32775*	The sumset of a group with a single element is the element's orbit by the group action. See gaorb 19212. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑔 + 𝑥) = 𝑦)}    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⊕ {𝑋}) = [𝑋] ∼ )
Theorem	lsmsnorb2 32776*	The sumset of a single element with a group is the element's orbit by the group action. See gaorb 19212. (Contributed by Thierry Arnoux, 24-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑥 + 𝑔) = 𝑦)}    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ({𝑋} ⊕ 𝐴) = [𝑋] ∼ )
Theorem	elringlsm 32777*	Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ × = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝐸 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝐸 × 𝐹) ↔ ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐹 𝑍 = (𝑥 · 𝑦)))
Theorem	elringlsmd 32778	Membership in a product of two subsets of a ring, one direction. (Contributed by Thierry Arnoux, 13-Apr-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ × = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝐸 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ (𝐸 × 𝐹))
Theorem	ringlsmss 32779	Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ × = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐸 × 𝐹) ⊆ 𝐵)
Theorem	ringlsmss1 32780	The product of an ideal 𝐼 of a commutative ring 𝑅 with some set E is a subset of the ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ × = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐸 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    ⇒   ⊢ (𝜑 → (𝐼 × 𝐸) ⊆ 𝐼)
Theorem	ringlsmss2 32781	The product with an ideal of a ring is a subset of that ideal. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ × = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    ⇒   ⊢ (𝜑 → (𝐸 × 𝐼) ⊆ 𝐼)
Theorem	lsmsnpridl 32782	The product of the ring with a single element is equal to the principal ideal generated by that element. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ × = (LSSum‘𝐺)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 × {𝑋}) = (𝐾‘{𝑋}))
Theorem	lsmsnidl 32783	The product of the ring with a single element is a principal ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ × = (LSSum‘𝐺)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 × {𝑋}) ∈ (LPIdeal‘𝑅))
Theorem	lsmidllsp 32784	The sum of two ideals is the ideal generated by their union. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅))    ⇒   ⊢ (𝜑 → (𝐼 ⊕ 𝐽) = (𝐾‘(𝐼 ∪ 𝐽)))
Theorem	lsmidl 32785	The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅))    ⇒   ⊢ (𝜑 → (𝐼 ⊕ 𝐽) ∈ (LIdeal‘𝑅))
Theorem	lsmssass 32786	Group sum is associative, subset version (see lsmass 19578). (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈)))
Theorem	grplsm0l 32787	Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ({ 0 } ⊕ 𝐴) = 𝐴)
Theorem	grplsmid 32788	The direct sum of an element 𝑋 of a subgroup 𝐴 is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝐴) → ({𝑋} ⊕ 𝐴) = 𝐴)
21.3.9.28  The quotient map
Theorem	qusmul 32789	Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.)
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ([𝑋](𝑅 ~QG 𝐼) × [𝑌](𝑅 ~QG 𝐼)) = [(𝑋 · 𝑌)](𝑅 ~QG 𝐼))
Theorem	quslsm 32790	Express the image by the quotient map in terms of direct sum. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → [𝑋](𝐺 ~QG 𝑆) = ({𝑋} ⊕ 𝑆))
Theorem	qusbas2 32791*	Alternate definition of the group quotient set, as the set of all cosets of the form ({𝑥} ⊕ 𝑁). (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → (𝐵 / (𝐺 ~QG 𝑁)) = ran (𝑥 ∈ 𝐵 ↦ ({𝑥} ⊕ 𝑁)))
Theorem	qus0g 32792	The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025.)
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    ⇒   ⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → (0g‘𝑄) = 𝑁)
Theorem	qusima 32793*	The image of a subgroup by the natural map from elements to their cosets. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → (𝐸‘𝐻) = (𝐹 “ 𝐻))
Theorem	qusrn 32794*	The natural map from elements to their cosets is surjective. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (𝐵 / (𝐺 ~QG 𝑁))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → ran 𝐹 = 𝑈)
Theorem	nsgqus0 32795	A normal subgroup 𝑁 is a member of all subgroups 𝐹 of the quotient group by 𝑁. In fact, it is the identity element of the quotient group. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    ⇒   ⊢ ((𝑁 ∈ (NrmSGrp‘𝐺) ∧ 𝐹 ∈ (SubGrp‘𝑄)) → 𝑁 ∈ 𝐹)
Theorem	nsgmgclem 32796*	Lemma for nsgmgc 32797. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    &   ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝑄))    ⇒   ⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ∈ (SubGrp‘𝐺))
Theorem	nsgmgc 32797*	There is a monotone Galois connection between the lattice of subgroups of a group 𝐺 containing a normal subgroup 𝑁 and the lattice of subgroups of the quotient group 𝐺 / 𝑁. This is sometimes called the lattice theorem. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ 𝐽 = (𝑉MGalConn𝑊)    &   ⊢ 𝑉 = (toInc‘𝑆)    &   ⊢ 𝑊 = (toInc‘𝑇)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → 𝐸𝐽𝐹)
Theorem	nsgqusf1olem1 32798*	Lemma for nsgqusf1o 32801. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) ∈ 𝑇)
Theorem	nsgqusf1olem2 32799*	Lemma for nsgqusf1o 32801. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → ran 𝐸 = 𝑇)
Theorem	nsgqusf1olem3 32800*	Lemma for nsgqusf1o 32801. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → ran 𝐹 = 𝑆)