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	fldgenfld 33401	A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field)
Theorem	primefldgen1 33402	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 33403	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 33404	A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ 𝑈 = (Unit‘𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑆)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶))))
Theorem	kerunit 33405	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 33406	Extend class notation with the scalar restriction operation.
class ↾v
Definition	df-resv 33407*	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 33408	The scalar restriction is a proper operator, so it can be used with ovprc1 7397. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ Rel dom ↾v
Theorem	resvval 33409	Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)))
Theorem	resvid2 33410	General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊)
Theorem	resvval2 33411	Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))
Theorem	resvsca 33412	Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅))
Theorem	resvlem 33413	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 33414	Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻))
Theorem	resvplusg 33415	+g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))
Theorem	resvvsca 33416	·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻))
Theorem	resvmulr 33417	.r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻))
Theorem	resv0g 33418	0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻))
Theorem	resv1r 33419	1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 1 = (1r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻))
Theorem	resvcmn 33420	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 33421	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 33422	The complex numbers form a field. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ ℂfld ∈ Field
Theorem	reofld 33423	The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ℝfld ∈ oField
Theorem	nn0omnd 33424	The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ oMnd
Theorem	gsumind 33425	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 33426	The field of the real numbers is Archimedean. See also arch 12423. (Contributed by Thierry Arnoux, 9-Apr-2018.)
⊢ ℝfld ∈ Archi
Theorem	nn0archi 33427	The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ Archi
Theorem	xrge0slmod 33428	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 33429*	The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺))    &   ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺))    &   ⊢ 0 = (0g‘𝑁)    ⇒   ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺)
Theorem	eqgvscpbl 33430	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 33431*	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 33432	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 33433*	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 33434*	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 33435*	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 33436*	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 33437*	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 33438	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 33439*	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 33440	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 33441	The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ (𝑋 ∈ 𝐴 → [𝑋](𝐴 × 𝐴) = 𝐴)
Theorem	qsxpid 33442	The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.)
⊢ (𝐴 ≠ ∅ → (𝐴 / (𝐴 × 𝐴)) = {𝐴})
Theorem	qusxpid 33443	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 33444	The quotient of a group 𝐺 by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐵))    ⇒   ⊢ (𝐺 ∈ Grp → (Base‘𝑄) = {𝐵})
Theorem	qustrivr 33445	Converse of qustriv 33444. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐻))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ (Base‘𝑄) = {𝐻}) → 𝐻 = 𝐵)
21.3.10.34  The ring of integers modulo ` N `
Theorem	znfermltl 33446	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 33447*	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 33448*	Variation on ellspd 21790. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ 𝑁 = (LSpan‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ LMod)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣))))))
Theorem	0ellsp 33449	Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑆))
Theorem	0nellinds 33450	The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.)
⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ¬ 0 ∈ 𝐹)
Theorem	rspsnid 33451	A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ (𝐾‘{𝐺}))
Theorem	elrsp 33452*	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 33453	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 33454*	In a principal ideal ring, ideals are principal. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ LPIR)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥}))
Theorem	rspidlid 33455	The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐾‘𝐼) = 𝐼)
Theorem	pidlnz 33456	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	lbslsp 33457*	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 33458	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 33459	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 33460*	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 33461	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 33462*	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 33463*	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.10.36  Ring associates, ring units
Theorem	dvdsruassoi 33464	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 33465*	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	dvdsruasso2 33466*	A reformulation of dvdsruasso 33465. (Proposed by Gerard Lang, 28-May-2025.) (Contributed by Thiery Arnoux, 29-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ ∃𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑈 ((𝑢 · 𝑋) = 𝑌 ∧ (𝑣 · 𝑌) = 𝑋 ∧ (𝑢 · 𝑣) = 1 )))
Theorem	dvdsrspss 33467	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 33468	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	unitprodclb 33469	A finite product is a unit iff all factors are units. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝐵)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹) ∈ 𝑈 ↔ ran 𝐹 ⊆ 𝑈))
21.3.10.37  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 33470*	Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝐴 ⊕ {𝑋}) ↔ ∃𝑥 ∈ 𝐴 𝑍 = (𝑥 + 𝑋)))
Theorem	lsmsnorb 33471*	The sumset of a group with a single element is the element's orbit by the group action. See gaorb 19271. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑔 + 𝑥) = 𝑦)}    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⊕ {𝑋}) = [𝑋] ∼ )
Theorem	lsmsnorb2 33472*	The sumset of a single element with a group is the element's orbit by the group action. See gaorb 19271. (Contributed by Thierry Arnoux, 24-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑥 + 𝑔) = 𝑦)}    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ({𝑋} ⊕ 𝐴) = [𝑋] ∼ )
Theorem	elringlsm 33473*	Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ × = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝐸 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝐸 × 𝐹) ↔ ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐹 𝑍 = (𝑥 · 𝑦)))
Theorem	elringlsmd 33474	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 33475	Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ × = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐸 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐸 × 𝐹) ⊆ 𝐵)
Theorem	ringlsmss1 33476	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 33477	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 33478	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 33479	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 33480	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 33481	The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅))    ⇒   ⊢ (𝜑 → (𝐼 ⊕ 𝐽) ∈ (LIdeal‘𝑅))
Theorem	lsmssass 33482	Group sum is associative, subset version (see lsmass 19633). (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈)))
Theorem	grplsm0l 33483	Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ({ 0 } ⊕ 𝐴) = 𝐴)
Theorem	grplsmid 33484	The direct sum of an element 𝑋 of a subgroup 𝐴 is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝐴) → ({𝑋} ⊕ 𝐴) = 𝐴)
21.3.10.38  The quotient map
Theorem	quslsm 33485	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 33486*	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 33487	The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025.)
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    ⇒   ⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → (0g‘𝑄) = 𝑁)
Theorem	qusima 33488*	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 33489*	The natural map from elements to their cosets is surjective. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (𝐵 / (𝐺 ~QG 𝑁))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → ran 𝐹 = 𝑈)
Theorem	nsgqus0 33490	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 33491*	Lemma for nsgmgc 33492. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    &   ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝑄))    ⇒   ⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ∈ (SubGrp‘𝐺))
Theorem	nsgmgc 33492*	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 33493*	Lemma for nsgqusf1o 33496. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) ∈ 𝑇)
Theorem	nsgqusf1olem2 33494*	Lemma for nsgqusf1o 33496. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → ran 𝐸 = 𝑇)
Theorem	nsgqusf1olem3 33495*	Lemma for nsgqusf1o 33496. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → ran 𝐹 = 𝑆)
Theorem	nsgqusf1o 33496*	The canonical projection homomorphism 𝐸 defines a bijective correspondence between the set 𝑆 of subgroups of 𝐺 containing a normal subgroup 𝑁 and the subgroups of the quotient group 𝐺 / 𝑁. This theorem is sometimes called the correspondence theorem, or the fourth isomorphism theorem. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → 𝐸:𝑆–1-1-onto→𝑇)
Theorem	lmhmqusker 33497*	A surjective module homomorphism 𝐹 from 𝐺 to 𝐻 induces an isomorphism 𝐽 from 𝑄 to 𝐻, where 𝑄 is the factor group of 𝐺 by 𝐹's kernel 𝐾. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 LMHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    ⇒   ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso 𝐻))
Theorem	lmicqusker 33498	The image 𝐻 of a module homomorphism 𝐹 is isomorphic with the quotient module 𝑄 over 𝐹's kernel 𝐾. This is part of what is sometimes called the first isomorphism theorem for modules. (Contributed by Thierry Arnoux, 10-Mar-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 LMHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻))    ⇒   ⊢ (𝜑 → 𝑄 ≃𝑚 𝐻)
21.3.10.39  Ideals
Theorem	lidlmcld 33499	An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	intlidl 33500	The intersection of a nonempty collection of ideals is an ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.)
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∩ 𝐶 ∈ (LIdeal‘𝑅))