P. 198 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19701-19800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	islssd 19701*	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 19702	A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉)
Theorem	lssel 19703	A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ 𝑉)
Theorem	lss1 19704	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 19705	The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → ∪ 𝑆 = 𝑉)
Theorem	lssn0 19706	A subspace is not empty. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝑆 → 𝑈 ≠ ∅)
Theorem	00lss 19707	The empty structure has no subspaces (for use with fvco4i 6756). (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ ∅ = (LSubSp‘∅)
Theorem	lsscl 19708	Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝑆 ∧ (𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → ((𝑍 · 𝑋) + 𝑌) ∈ 𝑈)
Theorem	lssvsubcl 19709	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 19710	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 19902. Can it be used along with lspsnne1 19883, lspsnne2 19884 to shorten this proof? (Contributed by NM, 14-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝑋 + 𝑌) ∈ 𝑈)
Theorem	lssvancl2 19711	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 19712	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 19713	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 19714	The zero subspace is included in every subspace. (sh0le 29211 analog.) (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → { 0 } ⊆ 𝑋)
Theorem	lssle0 19715	No subspace is smaller than the zero subspace. (shle0 29213 analog.) (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝑋 ⊆ { 0 } ↔ 𝑋 = { 0 }))
Theorem	lssne0 19716*	A nonzero subspace has a nonzero vector. (shne0i 29219 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 8-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑋 ∈ 𝑆 → (𝑋 ≠ { 0 } ↔ ∃𝑦 ∈ 𝑋 𝑦 ≠ 0 ))
Theorem	lssvneln0 19717	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 19718	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 19719*	Conclude subspace ordering from nonzero vector membership. (ssrdv 3972 analog.) (Contributed by NM, 17-Aug-2014.) (Revised by AV, 13-Jul-2022.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈))    ⇒   ⊢ (𝜑 → 𝑇 ⊆ 𝑈)
Theorem	lssvacl 19720	Closure of vector addition in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ + = (+g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 + 𝑌) ∈ 𝑈)
Theorem	lssvscl 19721	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 19722	Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈)
Theorem	lsssubg 19723	All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊))
Theorem	lsssssubg 19724	All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑊))
Theorem	islss3 19725	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 19726	A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod)
Theorem	lsslss 19727	The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑇 = (LSubSp‘𝑋)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑉 ∈ 𝑇 ↔ (𝑉 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑈)))
Theorem	islss4 19728*	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 19729*	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 19730	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 19731	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 19732	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 19733	Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑆 ∈ (ACS‘𝐵))
Theorem	prdsvscacl 19734*	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 19735*	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 19736	A structure power of a left module is a left module. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ LMod)
Syntax	clspn 19737	Extend class notation with span of a set of vectors.
class LSpan
Definition	df-lsp 19738*	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 19739*	The span function for a left vector space (or a left module). (df-span 29080 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝑁 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡}))
Theorem	lspf 19740	The span operator on a left module maps subsets to subsets. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑁:𝒫 𝑉⟶𝑆)
Theorem	lspval 19741*	The span of a set of vectors (in a left module). (spanval 29104 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) = ∩ {𝑡 ∈ 𝑆 ∣ 𝑈 ⊆ 𝑡})
Theorem	lspcl 19742	The span of a set of vectors is a subspace. (spancl 29107 analog.) (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) ∈ 𝑆)
Theorem	lspsncl 19743	The span of a singleton is a subspace (frequently used special case of lspcl 19742). (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆)
Theorem	lspprcl 19744	The span of a pair is a subspace (frequently used special case of lspcl 19742). (Contributed by NM, 11-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ 𝑆)
Theorem	lsptpcl 19745	The span of an unordered triple is a subspace (frequently used special case of lspcl 19742). (Contributed by NM, 22-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌, 𝑍}) ∈ 𝑆)
Theorem	lspsnsubg 19746	The span of a singleton is an additive subgroup (frequently used special case of lspcl 19742). (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊))
Theorem	00lsp 19747	fvco4i 6756 lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ ∅ = (LSpan‘∅)
Theorem	lspid 19748	The span of a subspace is itself. (spanid 29118 analog.) (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘𝑈) = 𝑈)
Theorem	lspssv 19749	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 19750	Span preserves subset ordering. (spanss 29119 analog.) (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ (𝑁‘𝑈))
Theorem	lspssid 19751	A set of vectors is a subset of its span. (spanss2 29116 analog.) (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (𝑁‘𝑈))
Theorem	lspidm 19752	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 19753	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 19754	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 19755	Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝑈 = (LSubSp‘𝑊)    &   ⊢ 𝐾 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (mrCls‘𝑈)    ⇒   ⊢ (𝑊 ∈ LMod → 𝐾 = 𝐹)
Theorem	lspsnss 19756	The span of the singleton of a subspace member is included in the subspace. (spansnss 29342 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘{𝑋}) ⊆ 𝑈)
Theorem	lspsnel3 19757	A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn3 29343 analog.) (Contributed by NM, 4-Jul-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋}))    ⇒   ⊢ (𝜑 → 𝑌 ∈ 𝑈)
Theorem	lspprss 19758	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 19759	A vector belongs to the span of its singleton. (spansnid 29334 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝑁‘{𝑋}))
Theorem	lspsnel6 19760	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	lspsnel5 19761	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	lspsnel5a 19762	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 19763	A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lspprid2 19764	A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lspprvacl 19765	The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lssats2 19766*	A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑈 = ∪ 𝑥 ∈ 𝑈 (𝑁‘{𝑥}))
Theorem	lspsneli 19767	A scalar product with a vector belongs to the span of its singleton. (spansnmul 29335 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 · 𝑋) ∈ (𝑁‘{𝑋}))
Theorem	lspsn 19768*	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	lspsnel 19769*	Member of span of the singleton of a vector. (elspansn 29337 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑈 ∈ (𝑁‘{𝑋}) ↔ ∃𝑘 ∈ 𝐾 𝑈 = (𝑘 · 𝑋)))
Theorem	lspsnvsi 19770	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 19771*	Comparable spans of singletons must have proportional vectors. See lspsneq 19888 for equal span version. (Contributed by NM, 7-Jun-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ 𝐾 𝑋 = (𝑘 · 𝑌)))
Theorem	lspsnneg 19772	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 19773	Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) = (𝑁‘{(𝑌 − 𝑋)}))
Theorem	lspsn0 19774	Span of the singleton of the zero vector. (spansn0 29312 analog.) (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑁‘{ 0 }) = { 0 })
Theorem	lsp0 19775	Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑁‘∅) = { 0 })
Theorem	lspuni0 19776	Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → ∪ (𝑁‘∅) = 0 )
Theorem	lspun0 19777	The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑋 ∪ { 0 })) = (𝑁‘𝑋))
Theorem	lspsneq0 19778	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 19779	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 19780	Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 )
Theorem	lsslsp 19781	Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) TODO: Shouldn't we swap 𝑀‘𝐺 and 𝑁‘𝐺 since we are computing a property of 𝑁‘𝐺? (Like we say sin 0 = 0 and not 0 = sin 0.) - NM 15-Mar-2015.
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑀 = (LSpan‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑋)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈) → (𝑀‘𝐺) = (𝑁‘𝐺))
Theorem	lss0v 19782	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 19783*	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 19784*	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.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐾)))    &   ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐿)))    &   ⊢ (𝜑 → 𝐾 ∈ V)    &   ⊢ (𝜑 → 𝐿 ∈ V)    ⇒   ⊢ (𝜑 → (LSpan‘𝐾) = (LSpan‘𝐿))
10.5.3  Homomorphisms and isomorphisms of left modules
Syntax	clmhm 19785	Extend class notation with the generator of left module hom-sets.
class LMHom
Syntax	clmim 19786	The class of left module isomorphism sets.
class LMIso
Syntax	clmic 19787	The class of the left module isomorphism relation.
class ≃𝑚
Definition	df-lmhm 19788*	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 19789*	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 19790	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 19791	Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ Rel dom LMHom
Theorem	lmimfn 19792	Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ LMIso Fn (LMod × LMod)
Theorem	islmhm 19793*	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 19794*	Property of a module homomorphism, similar to ismhm 17952. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐸 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    ⇒   ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐸 (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦)))))
Theorem	lmhmlem 19795	Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾)))
Theorem	lmhmsca 19796	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 19797	A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	lmhmlmod2 19798	A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod)
Theorem	lmhmlmod1 19799	A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod)
Theorem	lmhmf 19800	A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝐵⟶𝐶)