P. 211 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21001-21100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lspidm 21001	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 21002	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 21003	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 21004	Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝑈 = (LSubSp‘𝑊)    &   ⊢ 𝐾 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (mrCls‘𝑈)    ⇒   ⊢ (𝑊 ∈ LMod → 𝐾 = 𝐹)
Theorem	lspsnss 21005	The span of the singleton of a subspace member is included in the subspace. (spansnss 31599 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘{𝑋}) ⊆ 𝑈)
Theorem	ellspsn3 21006	A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn3 31600 analog.) (Contributed by NM, 4-Jul-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋}))    ⇒   ⊢ (𝜑 → 𝑌 ∈ 𝑈)
Theorem	lspprss 21007	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 21008	A vector belongs to the span of its singleton. (spansnid 31591 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝑁‘{𝑋}))
Theorem	ellspsn6 21009	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 21010	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 21011	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 21012	A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lspprid2 21013	A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lspprvacl 21014	The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lssats2 21015*	A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑈 = ∪ 𝑥 ∈ 𝑈 (𝑁‘{𝑥}))
Theorem	ellspsni 21016	A scalar product with a vector belongs to the span of its singleton. (spansnmul 31592 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 · 𝑋) ∈ (𝑁‘{𝑋}))
Theorem	lspsn 21017*	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 21018*	Member of span of the singleton of a vector. (elspansn 31594 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑈 ∈ (𝑁‘{𝑋}) ↔ ∃𝑘 ∈ 𝐾 𝑈 = (𝑘 · 𝑋)))
Theorem	lspsnvsi 21019	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 21020*	Comparable spans of singletons must have proportional vectors. See lspsneq 21141 for equal span version. (Contributed by NM, 7-Jun-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ 𝐾 𝑋 = (𝑘 · 𝑌)))
Theorem	lspsnneg 21021	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 21022	Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) = (𝑁‘{(𝑌 − 𝑋)}))
Theorem	lspsn0 21023	Span of the singleton of the zero vector. (spansn0 31569 analog.) (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑁‘{ 0 }) = { 0 })
Theorem	lsp0 21024	Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑁‘∅) = { 0 })
Theorem	lspuni0 21025	Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → ∪ (𝑁‘∅) = 0 )
Theorem	lspun0 21026	The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑋 ∪ { 0 })) = (𝑁‘𝑋))
Theorem	lspsneq0 21027	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 21028	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 21029	Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 )
Theorem	lsslsp 21030	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	lsslspOLD 21031	Obsolete version of lsslsp 21030 as of 25-Apr-2025. 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. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑀 = (LSpan‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑋)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈) → (𝑀‘𝐺) = (𝑁‘𝐺))
Theorem	lss0v 21032	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 21033*	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 21034*	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 21035	Extend class notation with the generator of left module hom-sets.
class LMHom
Syntax	clmim 21036	The class of left module isomorphism sets.
class LMIso
Syntax	clmic 21037	The class of the left module isomorphism relation.
class ≃𝑚
Definition	df-lmhm 21038*	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 21039*	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 21040	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 21041	Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ Rel dom LMHom
Theorem	lmimfn 21042	Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ LMIso Fn (LMod × LMod)
Theorem	islmhm 21043*	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 21044*	Property of a module homomorphism, similar to ismhm 18810. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐸 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    ⇒   ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐸 (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦)))))
Theorem	lmhmlem 21045	Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾)))
Theorem	lmhmsca 21046	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 21047	A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	lmhmlmod2 21048	A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod)
Theorem	lmhmlmod1 21049	A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod)
Theorem	lmhmf 21050	A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝐵⟶𝐶)
Theorem	lmhmlin 21051	A homomorphism of left modules is 𝐾-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐸 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌)))
Theorem	lmodvsinv 21052	Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝑀 = (invg‘𝐹)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑅) · 𝑋) = (𝑁‘(𝑅 · 𝑋)))
Theorem	lmodvsinv2 21053	Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → (𝑅 · (𝑁‘𝑋)) = (𝑁‘(𝑅 · 𝑋)))
Theorem	islmhm2 21054*	A one-equation proof of linearity of a left module homomorphism, similar to df-lss 20947. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    &   ⊢ 𝐸 = (Base‘𝐾)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    ⇒   ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐹‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 × (𝐹‘𝑦)) ⨣ (𝐹‘𝑧)))))
Theorem	islmhmd 21055*	Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    &   ⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐽 = (Scalar‘𝑇)    &   ⊢ 𝑁 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ LMod)    &   ⊢ (𝜑 → 𝐽 = 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))
Theorem	0lmhm 21056	The constant zero linear function between two modules. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 0 = (0g‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑇 = (Scalar‘𝑁)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇) → (𝐵 × { 0 }) ∈ (𝑀 LMHom 𝑁))
Theorem	idlmhm 21057	The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ LMod → ( I ↾ 𝐵) ∈ (𝑀 LMHom 𝑀))
Theorem	invlmhm 21058	The negative function on a module is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐼 = (invg‘𝑀)    ⇒   ⊢ (𝑀 ∈ LMod → 𝐼 ∈ (𝑀 LMHom 𝑀))
Theorem	lmhmco 21059	The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘ 𝐺) ∈ (𝑀 LMHom 𝑂))
Theorem	lmhmplusg 21060	The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ + = (+g‘𝑁)    ⇒   ⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘f + 𝐺) ∈ (𝑀 LMHom 𝑁))
Theorem	lmhmvsca 21061	The pointwise scalar product of a linear function and a constant is linear, over a commutative ring. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑉 = (Base‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑁)    &   ⊢ 𝐽 = (Scalar‘𝑁)    &   ⊢ 𝐾 = (Base‘𝐽)    ⇒   ⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘f · 𝐹) ∈ (𝑀 LMHom 𝑁))
Theorem	lmhmf1o 21062	A bijective module homomorphism is also converse homomorphic. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 LMHom 𝑆)))
Theorem	lmhmima 21063	The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑋 = (LSubSp‘𝑆)    &   ⊢ 𝑌 = (LSubSp‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (𝐹 “ 𝑈) ∈ 𝑌)
Theorem	lmhmpreima 21064	The inverse image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑋 = (LSubSp‘𝑆)    &   ⊢ 𝑌 = (LSubSp‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ 𝑋)
Theorem	lmhmlsp 21065	Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐾 = (LSpan‘𝑆)    &   ⊢ 𝐿 = (LSpan‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) = (𝐿‘(𝐹 “ 𝑈)))
Theorem	lmhmrnlss 21066	The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ (LSubSp‘𝑇))
Theorem	lmhmkerlss 21067	The kernel of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝑈 = (LSubSp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ 𝑈)
Theorem	reslmhm 21068	Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑈 = (LSubSp‘𝑆)    &   ⊢ 𝑅 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝐹 ↾ 𝑋) ∈ (𝑅 LMHom 𝑇))
Theorem	reslmhm2 21069	Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    &   ⊢ 𝐿 = (LSubSp‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑈) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿) → 𝐹 ∈ (𝑆 LMHom 𝑇))
Theorem	reslmhm2b 21070	Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    &   ⊢ 𝐿 = (LSubSp‘𝑇)    ⇒   ⊢ ((𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ 𝐹 ∈ (𝑆 LMHom 𝑈)))
Theorem	lmhmeql 21071	The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝑈 = (LSubSp‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ 𝑈)
Theorem	lspextmo 21072*	A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by NM, 17-Jun-2017.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐾 = (LSpan‘𝑆)    ⇒   ⊢ ((𝑋 ⊆ 𝐵 ∧ (𝐾‘𝑋) = 𝐵) → ∃*𝑔 ∈ (𝑆 LMHom 𝑇)(𝑔 ↾ 𝑋) = 𝐹)
Theorem	pwsdiaglmhm 21073*	Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 LMHom 𝑌))
Theorem	pwssplit0 21074*	Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s 𝑈)    &   ⊢ 𝑍 = (𝑊 ↑s 𝑉)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐶 = (Base‘𝑍)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉))    ⇒   ⊢ ((𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵⟶𝐶)
Theorem	pwssplit1 21075*	Splitting for structure powers, part 1: restriction is an onto function. The only actual monoid law we need here is that the base set is nonempty. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s 𝑈)    &   ⊢ 𝑍 = (𝑊 ↑s 𝑉)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐶 = (Base‘𝑍)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉))    ⇒   ⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵–onto→𝐶)
Theorem	pwssplit2 21076*	Splitting for structure powers, part 2: restriction is a group homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s 𝑈)    &   ⊢ 𝑍 = (𝑊 ↑s 𝑉)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐶 = (Base‘𝑍)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉))    ⇒   ⊢ ((𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹 ∈ (𝑌 GrpHom 𝑍))
Theorem	pwssplit3 21077*	Splitting for structure powers, part 3: restriction is a module homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s 𝑈)    &   ⊢ 𝑍 = (𝑊 ↑s 𝑉)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐶 = (Base‘𝑍)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉))    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹 ∈ (𝑌 LMHom 𝑍))
Theorem	islmim 21078	An isomorphism of left modules is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) ↔ (𝐹 ∈ (𝑅 LMHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	lmimf1o 21079	An isomorphism of left modules is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	lmimlmhm 21080	An isomorphism of modules is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹 ∈ (𝑅 LMHom 𝑆))
Theorem	lmimgim 21081	An isomorphism of modules is an isomorphism of groups. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹 ∈ (𝑅 GrpIso 𝑆))
Theorem	islmim2 21082	An isomorphism of left modules is a homomorphism whose converse is a homomorphism. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) ↔ (𝐹 ∈ (𝑅 LMHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 LMHom 𝑅)))
Theorem	lmimcnv 21083	The converse of a bijective module homomorphism is a bijective module homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ (𝐹 ∈ (𝑆 LMIso 𝑇) → ◡𝐹 ∈ (𝑇 LMIso 𝑆))
Theorem	brlmic 21084	The relation "is isomorphic to" for modules. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑚 𝑆 ↔ (𝑅 LMIso 𝑆) ≠ ∅)
Theorem	brlmici 21085	Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝑅 ≃𝑚 𝑆)
Theorem	lmiclcl 21086	Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑚 𝑆 → 𝑅 ∈ LMod)
Theorem	lmicrcl 21087	Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ∈ LMod)
Theorem	lmicsym 21088	Module isomorphism is symmetric. (Contributed by Stefan O'Rear, 26-Feb-2015.)
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ≃𝑚 𝑅)
Theorem	lmhmpropd 21089*	Module homomorphism depends only on the module attributes of structures. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐽))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐽))    &   ⊢ (𝜑 → 𝐺 = (Scalar‘𝐾))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐿))    &   ⊢ (𝜑 → 𝐺 = (Scalar‘𝑀))    &   ⊢ 𝑃 = (Base‘𝐹)    &   ⊢ 𝑄 = (Base‘𝐺)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐽)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝐶)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝑀)𝑦))    ⇒   ⊢ (𝜑 → (𝐽 LMHom 𝐾) = (𝐿 LMHom 𝑀))
10.5.4  Subspace sum; bases for a left module
Syntax	clbs 21090	Extend class notation with the set of bases for a vector space.
class LBasis
Definition	df-lbs 21091*	Define the set of bases to a left module or left vector space. (Contributed by Mario Carneiro, 24-Jun-2014.)
⊢ LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
Theorem	islbs 21092*	The predicate "𝐵 is a basis for the left module or vector space 𝑊". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014.) (Revised by Mario Carneiro, 14-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝐹)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
Theorem	lbsss 21093	A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉)
Theorem	lbsel 21094	An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ ((𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵) → 𝐸 ∈ 𝑉)
Theorem	lbssp 21095	The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝐵 ∈ 𝐽 → (𝑁‘𝐵) = 𝑉)
Theorem	lbsind 21096	A basis is linearly independent; that is, every element has a span which trivially intersects the span of the remainder of the basis. (Contributed by Mario Carneiro, 12-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    ⇒   ⊢ (((𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → ¬ (𝐴 · 𝐸) ∈ (𝑁‘(𝐵 ∖ {𝐸})))
Theorem	lbsind2 21097	A basis is linearly independent; that is, every element is not in the span of the remainder of the basis. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 12-Jan-2015.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵) → ¬ 𝐸 ∈ (𝑁‘(𝐵 ∖ {𝐸})))
Theorem	lbspss 21098	No proper subset of a basis spans the space. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵) → (𝑁‘𝐶) ≠ 𝑉)
Theorem	lsmcl 21099	The sum of two subspaces is a subspace. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ⊕ 𝑈) ∈ 𝑆)
Theorem	lsmspsn 21100*	Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑈 ∈ ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ↔ ∃𝑗 ∈ 𝐾 ∃𝑘 ∈ 𝐾 𝑈 = ((𝑗 · 𝑋) + (𝑘 · 𝑌))))