P. 213 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21201-21300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lssset 21201*	The set of all (not necessarily closed) linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 15-Jul-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝑆 = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
Theorem	islss 21202*	The predicate "is a subspace" (of a left module or left vector space). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈))
Theorem	islssd 21203*	Properties that determine a subspace of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐹))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑊))    &   ⊢ (𝜑 → + = (+g‘𝑊))    &   ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))    &   ⊢ (𝜑 → 𝑆 = (LSubSp‘𝑊))    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑈 ≠ ∅)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	lssss 21204	A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉)
Theorem	lssel 21205	A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ 𝑉)
Theorem	lss1 21206	The set of vectors in a left module is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑉 ∈ 𝑆)
Theorem	lssuni 21207	The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → ∪ 𝑆 = 𝑉)
Theorem	lssn0 21208	A subspace is not empty. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝑆 → 𝑈 ≠ ∅)
Theorem	00lss 21209	The empty structure has no subspaces (for use with fvco4i 6985). (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ ∅ = (LSubSp‘∅)
Theorem	lsscl 21210	Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝑆 ∧ (𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → ((𝑍 · 𝑋) + 𝑌) ∈ 𝑈)
Theorem	lssvacl 21211	Closure of vector addition in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ + = (+g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 + 𝑌) ∈ 𝑈)
Theorem	lssvsubcl 21212	Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ − = (-g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 − 𝑌) ∈ 𝑈)
Theorem	lssvancl1 21213	Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. TODO: notice similarity to lspindp3 21407. Can it be used along with lspsnne1 21388, lspsnne2 21389 to shorten this proof? (Contributed by NM, 14-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝑋 + 𝑌) ∈ 𝑈)
Theorem	lssvancl2 21214	Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝑌 + 𝑋) ∈ 𝑈)
Theorem	lss0cl 21215	The zero vector belongs to every subspace. (Contributed by NM, 12-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 0 ∈ 𝑈)
Theorem	lsssn0 21216	The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → { 0 } ∈ 𝑆)
Theorem	lss0ss 21217	The zero subspace is included in every subspace. (sh0le 32035 analog.) (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → { 0 } ⊆ 𝑋)
Theorem	lssle0 21218	No subspace is smaller than the zero subspace. (shle0 32037 analog.) (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝑋 ⊆ { 0 } ↔ 𝑋 = { 0 }))
Theorem	lssne0 21219*	A nonzero subspace has a nonzero vector. (shne0i 32043 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 8-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑋 ∈ 𝑆 → (𝑋 ≠ { 0 } ↔ ∃𝑦 ∈ 𝑋 𝑦 ≠ 0 ))
Theorem	lssvneln0 21220	A vector 𝑋 which doesn't belong to a subspace 𝑈 is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 19-Jul-2022.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 0 )
Theorem	lssneln0 21221	A vector 𝑋 which doesn't belong to a subspace 𝑈 is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 17-Jul-2022.) (Proof shortened by AV, 19-Jul-2022.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
Theorem	lssssr 21222*	Conclude subspace ordering from nonzero vector membership. (ssrdv 3937 analog.) (Contributed by NM, 17-Aug-2014.) (Revised by AV, 13-Jul-2022.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈))    ⇒   ⊢ (𝜑 → 𝑇 ⊆ 𝑈)
Theorem	lssvscl 21223	Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈)) → (𝑋 · 𝑌) ∈ 𝑈)
Theorem	lssvnegcl 21224	Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈)
Theorem	lsssubg 21225	All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊))
Theorem	lsssssubg 21226	All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑊))
Theorem	islss3 21227	A linear subspace of a module is a subset which is a module in its own right. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)))
Theorem	lsslmod 21228	A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod)
Theorem	lsslss 21229	The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑇 = (LSubSp‘𝑋)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑉 ∈ 𝑇 ↔ (𝑉 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑈)))
Theorem	islss4 21230*	A linear subspace is a subgroup which respects scalar multiplication. (Contributed by Stefan O'Rear, 11-Dec-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑈 ∈ 𝑆 ↔ (𝑈 ∈ (SubGrp‘𝑊) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝑈 (𝑎 · 𝑏) ∈ 𝑈)))
Theorem	lss1d 21231*	One-dimensional subspace (or zero-dimensional if 𝑋 is the zero vector). (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∈ 𝑆)
Theorem	lssintcl 21232	The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝑆)
Theorem	lssincl 21233	The intersection of two subspaces is a subspace. (Contributed by NM, 7-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ∩ 𝑈) ∈ 𝑆)
Theorem	lssmre 21234	The subspaces of a module comprise a Moore system on the vectors of the module. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑆 ∈ (Moore‘𝐵))
Theorem	lssacs 21235	Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑆 ∈ (ACS‘𝐵))
Theorem	prdsvscacl 21236*	Pointwise scalar multiplication is closed in products of modules. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶LMod)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Scalar‘(𝑅‘𝑥)) = 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵)
Theorem	prdslmodd 21237*	The product of a family of left modules is a left module. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶LMod)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆)    ⇒   ⊢ (𝜑 → 𝑌 ∈ LMod)
Theorem	pwslmod 21238	A structure power of a left module is a left module. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ LMod)
Syntax	clspn 21239	Extend class notation with span of a set of vectors.
class LSpan
Definition	df-lsp 21240*	Define span of a set of vectors of a left module or left vector space. (Contributed by NM, 8-Dec-2013.)
⊢ LSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
Theorem	lspfval 21241*	The span function for a left vector space (or a left module). (df-span 31904 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝑁 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡}))
Theorem	lspf 21242	The span function on a left module maps subsets to subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑁:𝒫 𝑉⟶𝑆)
Theorem	lspval 21243*	The span of a set of vectors (in a left module). (spanval 31928 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) = ∩ {𝑡 ∈ 𝑆 ∣ 𝑈 ⊆ 𝑡})
Theorem	lspcl 21244	The span of a set of vectors is a subspace. (spancl 31931 analog.) (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) ∈ 𝑆)
Theorem	lspsncl 21245	The span of a singleton is a subspace (frequently used special case of lspcl 21244). (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆)
Theorem	lspprcl 21246	The span of a pair is a subspace (frequently used special case of lspcl 21244). (Contributed by NM, 11-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ 𝑆)
Theorem	lsptpcl 21247	The span of an unordered triple is a subspace (frequently used special case of lspcl 21244). (Contributed by NM, 22-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌, 𝑍}) ∈ 𝑆)
Theorem	lspsnsubg 21248	The span of a singleton is an additive subgroup (frequently used special case of lspcl 21244). (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊))
Theorem	00lsp 21249	fvco4i 6985 lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ ∅ = (LSpan‘∅)
Theorem	lspid 21250	The span of a subspace is itself. (spanid 31942 analog.) (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘𝑈) = 𝑈)
Theorem	lspssv 21251	A span is a set of vectors. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) ⊆ 𝑉)
Theorem	lspss 21252	Span preserves subset ordering. (spanss 31943 analog.) (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ (𝑁‘𝑈))
Theorem	lspssid 21253	A set of vectors is a subset of its span. (spanss2 31940 analog.) (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (𝑁‘𝑈))
Theorem	lspidm 21254	The span of a set of vectors is idempotent. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘(𝑁‘𝑈)) = (𝑁‘𝑈))
Theorem	lspun 21255	The span of union is the span of the union of spans. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉) → (𝑁‘(𝑇 ∪ 𝑈)) = (𝑁‘((𝑁‘𝑇) ∪ (𝑁‘𝑈))))
Theorem	lspssp 21256	If a set of vectors is a subset of a subspace, then the span of those vectors is also contained in the subspace. (Contributed by Mario Carneiro, 4-Sep-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ 𝑈)
Theorem	mrclsp 21257	Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝑈 = (LSubSp‘𝑊)    &   ⊢ 𝐾 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (mrCls‘𝑈)    ⇒   ⊢ (𝑊 ∈ LMod → 𝐾 = 𝐹)
Theorem	lspsnss 21258	The span of the singleton of a subspace member is included in the subspace. (spansnss 32166 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘{𝑋}) ⊆ 𝑈)
Theorem	ellspsn3 21259	A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn3 32167 analog.) (Contributed by NM, 4-Jul-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋}))    ⇒   ⊢ (𝜑 → 𝑌 ∈ 𝑈)
Theorem	lspprss 21260	The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈)
Theorem	lspsnid 21261	A vector belongs to the span of its singleton. (spansnid 32158 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝑁‘{𝑋}))
Theorem	ellspsn6 21262	Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ 𝑈)))
Theorem	ellspsn5b 21263	Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝑁‘{𝑋}) ⊆ 𝑈))
Theorem	ellspsn5 21264	Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ 𝑈)
Theorem	lspprid1 21265	A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lspprid2 21266	A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lspprvacl 21267	The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lssats2 21268*	A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑈 = ∪ 𝑥 ∈ 𝑈 (𝑁‘{𝑥}))
Theorem	ellspsni 21269	A scalar product with a vector belongs to the span of its singleton. (spansnmul 32159 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 · 𝑋) ∈ (𝑁‘{𝑋}))
Theorem	lspsn 21270*	Span of the singleton of a vector. (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) = {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})
Theorem	ellspsn 21271*	Member of span of the singleton of a vector. (elspansn 32161 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑈 ∈ (𝑁‘{𝑋}) ↔ ∃𝑘 ∈ 𝐾 𝑈 = (𝑘 · 𝑋)))
Theorem	lspsnvsi 21272	Span of a scalar product of a singleton. (Contributed by NM, 23-Apr-2014.) (Proof shortened by Mario Carneiro, 4-Sep-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑁‘{(𝑅 · 𝑋)}) ⊆ (𝑁‘{𝑋}))
Theorem	lspsnss2 21273*	Comparable spans of singletons must have proportional vectors. See lspsneq 21393 for equal span version. (Contributed by NM, 7-Jun-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ 𝐾 𝑋 = (𝑘 · 𝑌)))
Theorem	lspsnneg 21274	Negation does not change the span of a singleton. (Contributed by NM, 24-Apr-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑀 = (invg‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{(𝑀‘𝑋)}) = (𝑁‘{𝑋}))
Theorem	lspsnsub 21275	Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) = (𝑁‘{(𝑌 − 𝑋)}))
Theorem	lspsn0 21276	Span of the singleton of the zero vector. (spansn0 32136 analog.) (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑁‘{ 0 }) = { 0 })
Theorem	lsp0 21277	Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑁‘∅) = { 0 })
Theorem	lspuni0 21278	Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → ∪ (𝑁‘∅) = 0 )
Theorem	lspun0 21279	The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑋 ∪ { 0 })) = (𝑁‘𝑋))
Theorem	lspsneq0 21280	Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑁‘{𝑋}) = { 0 } ↔ 𝑋 = 0 ))
Theorem	lspsneq0b 21281	Equal singleton spans imply both arguments are zero or both are nonzero. (Contributed by NM, 21-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 = 0 ↔ 𝑌 = 0 ))
Theorem	lmodindp1 21282	Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 )
Theorem	lsslsp 21283	Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) Terms in the equation were swapped as proposed by NM on 15-Mar-2015. (Revised by AV, 18-Apr-2025.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑀 = (LSpan‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑋)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈) → (𝑁‘𝐺) = (𝑀‘𝐺))
Theorem	lss0v 21284	The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑍 = (0g‘𝑋)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿) → 𝑍 = 0 )
Theorem	lsspropd 21285*	If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐾)))    &   ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐿)))    ⇒   ⊢ (𝜑 → (LSubSp‘𝐾) = (LSubSp‘𝐿))
Theorem	lsppropd 21286*	If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 24-Apr-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐾)))    &   ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐿)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (LSpan‘𝐾) = (LSpan‘𝐿))
10.5.3  Homomorphisms and isomorphisms of left modules
Syntax	clmhm 21287	Extend class notation with the generator of left module hom-sets.
class LMHom
Syntax	clmim 21288	The class of left module isomorphism sets.
class LMIso
Syntax	clmic 21289	The class of the left module isomorphism relation.
class ≃𝑚
Definition	df-lmhm 21290*	A homomorphism of left modules is a group homomorphism which additionally preserves the scalar product. This requires both structures to be left modules over the same ring. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ LMHom = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))})
Definition	df-lmim 21291*	An isomorphism of modules is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group and scalar operations. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ LMIso = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑔 ∈ (𝑠 LMHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})
Definition	df-lmic 21292	Two modules are said to be isomorphic iff they are connected by at least one isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ ≃𝑚 = (◡ LMIso “ (V ∖ 1o))
Theorem	reldmlmhm 21293	Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ Rel dom LMHom
Theorem	lmimfn 21294	Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ LMIso Fn (LMod × LMod)
Theorem	islmhm 21295*	Property of being a homomorphism of left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof shortened by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐸 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐸 (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦)))))
Theorem	islmhm3 21296*	Property of a module homomorphism, similar to ismhm 18973. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐸 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    ⇒   ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐸 (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦)))))
Theorem	lmhmlem 21297	Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾)))
Theorem	lmhmsca 21298	A homomorphism of left modules constrains both modules to the same ring of scalars. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐿 = 𝐾)
Theorem	lmghm 21299	A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	lmhmlmod2 21300	A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod)