P. 204 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20301-20400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lmhmsca 20301	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 20302	A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	lmhmlmod2 20303	A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod)
Theorem	lmhmlmod1 20304	A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod)
Theorem	lmhmf 20305	A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝐵⟶𝐶)
Theorem	lmhmlin 20306	A homomorphism of left modules is 𝐾-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐸 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌)))
Theorem	lmodvsinv 20307	Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝑀 = (invg‘𝐹)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑅) · 𝑋) = (𝑁‘(𝑅 · 𝑋)))
Theorem	lmodvsinv2 20308	Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → (𝑅 · (𝑁‘𝑋)) = (𝑁‘(𝑅 · 𝑋)))
Theorem	islmhm2 20309*	A one-equation proof of linearity of a left module homomorphism, similar to df-lss 20203. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐿 = (Scalar‘𝑇)    &   ⊢ 𝐸 = (Base‘𝐾)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    ⇒   ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐹‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 × (𝐹‘𝑦)) ⨣ (𝐹‘𝑧)))))
Theorem	islmhmd 20310*	Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ × = ( ·𝑠 ‘𝑇)    &   ⊢ 𝐾 = (Scalar‘𝑆)    &   ⊢ 𝐽 = (Scalar‘𝑇)    &   ⊢ 𝑁 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ LMod)    &   ⊢ (𝜑 → 𝐽 = 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))
Theorem	0lmhm 20311	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 20312	The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ LMod → ( I ↾ 𝐵) ∈ (𝑀 LMHom 𝑀))
Theorem	invlmhm 20313	The negative function on a module is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐼 = (invg‘𝑀)    ⇒   ⊢ (𝑀 ∈ LMod → 𝐼 ∈ (𝑀 LMHom 𝑀))
Theorem	lmhmco 20314	The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘ 𝐺) ∈ (𝑀 LMHom 𝑂))
Theorem	lmhmplusg 20315	The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ + = (+g‘𝑁)    ⇒   ⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘f + 𝐺) ∈ (𝑀 LMHom 𝑁))
Theorem	lmhmvsca 20316	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 20317	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 20318	The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑋 = (LSubSp‘𝑆)    &   ⊢ 𝑌 = (LSubSp‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (𝐹 “ 𝑈) ∈ 𝑌)
Theorem	lmhmpreima 20319	The inverse image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑋 = (LSubSp‘𝑆)    &   ⊢ 𝑌 = (LSubSp‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ 𝑋)
Theorem	lmhmlsp 20320	Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐾 = (LSpan‘𝑆)    &   ⊢ 𝐿 = (LSpan‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) = (𝐿‘(𝐹 “ 𝑈)))
Theorem	lmhmrnlss 20321	The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ (LSubSp‘𝑇))
Theorem	lmhmkerlss 20322	The kernel of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝑈 = (LSubSp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ 𝑈)
Theorem	reslmhm 20323	Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑈 = (LSubSp‘𝑆)    &   ⊢ 𝑅 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝐹 ↾ 𝑋) ∈ (𝑅 LMHom 𝑇))
Theorem	reslmhm2 20324	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 20325	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 20326	The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝑈 = (LSubSp‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ 𝑈)
Theorem	lspextmo 20327*	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 20328*	Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 LMHom 𝑌))
Theorem	pwssplit0 20329*	Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s 𝑈)    &   ⊢ 𝑍 = (𝑊 ↑s 𝑉)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐶 = (Base‘𝑍)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉))    ⇒   ⊢ ((𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵⟶𝐶)
Theorem	pwssplit1 20330*	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 20331*	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 20332*	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 20333	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 20334	An isomorphism of left modules is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	lmimlmhm 20335	An isomorphism of modules is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹 ∈ (𝑅 LMHom 𝑆))
Theorem	lmimgim 20336	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 20337	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 20338	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 20339	The relation "is isomorphic to" for modules. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑚 𝑆 ↔ (𝑅 LMIso 𝑆) ≠ ∅)
Theorem	brlmici 20340	Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝑅 ≃𝑚 𝑆)
Theorem	lmiclcl 20341	Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑚 𝑆 → 𝑅 ∈ LMod)
Theorem	lmicrcl 20342	Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ∈ LMod)
Theorem	lmicsym 20343	Module isomorphism is symmetric. (Contributed by Stefan O'Rear, 26-Feb-2015.)
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ≃𝑚 𝑅)
Theorem	lmhmpropd 20344*	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 20345	Extend class notation with the set of bases for a vector space.
class LBasis
Definition	df-lbs 20346*	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 20347*	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 20348	A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉)
Theorem	lbsel 20349	An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ ((𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵) → 𝐸 ∈ 𝑉)
Theorem	lbssp 20350	The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝐵 ∈ 𝐽 → (𝑁‘𝐵) = 𝑉)
Theorem	lbsind 20351	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 20352	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 20353	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 20354	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 20355*	Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑈 ∈ ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ↔ ∃𝑗 ∈ 𝐾 ∃𝑘 ∈ 𝐾 𝑈 = ((𝑗 · 𝑋) + (𝑘 · 𝑌))))
Theorem	lsmelval2 20356*	Subspace sum membership in terms of a sum of 1-dim subspaces (atoms), which can be useful for treating subspaces as projective lattice elements. (Contributed by NM, 9-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})))))
Theorem	lsmsp 20357	Subspace sum in terms of span. (Contributed by NM, 6-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ⊕ 𝑈) = (𝑁‘(𝑇 ∪ 𝑈)))
Theorem	lsmsp2 20358	Subspace sum of spans of subsets is the span of their union. (spanuni 29915 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉) → ((𝑁‘𝑇) ⊕ (𝑁‘𝑈)) = (𝑁‘(𝑇 ∪ 𝑈)))
Theorem	lsmssspx 20359	Subspace sum (in its extended domain) is a subset of the span of the union of its arguments. (Contributed by NM, 6-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → (𝑇 ⊕ 𝑈) ⊆ (𝑁‘(𝑇 ∪ 𝑈)))
Theorem	lsmpr 20360	The span of a pair of vectors equals the sum of the spans of their singletons. (Contributed by NM, 13-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})))
Theorem	lsppreli 20361	A vector expressed as a sum belongs to the span of its components. (Contributed by NM, 9-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	lsmelpr 20362	Two ways to say that a vector belongs to the span of a pair of vectors. (Contributed by NM, 14-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍}))))
Theorem	lsppr0 20363	The span of a vector paired with zero equals the span of the singleton of the vector. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 0 }) = (𝑁‘{𝑋}))
Theorem	lsppr 20364*	Span of a pair of vectors. (Contributed by NM, 22-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = {𝑣 ∣ ∃𝑘 ∈ 𝐾 ∃𝑙 ∈ 𝐾 𝑣 = ((𝑘 · 𝑋) + (𝑙 · 𝑌))})
Theorem	lspprel 20365*	Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑁‘{𝑋, 𝑌}) ↔ ∃𝑘 ∈ 𝐾 ∃𝑙 ∈ 𝐾 𝑍 = ((𝑘 · 𝑋) + (𝑙 · 𝑌))))
Theorem	lspprabs 20366	Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, (𝑋 + 𝑌)}) = (𝑁‘{𝑋, 𝑌}))
Theorem	lspvadd 20367	The span of a vector sum is included in the span of its arguments. (Contributed by NM, 22-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑁‘{(𝑋 + 𝑌)}) ⊆ (𝑁‘{𝑋, 𝑌}))
Theorem	lspsntri 20368	Triangle-type inequality for span of a singleton. (Contributed by NM, 24-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑁‘{(𝑋 + 𝑌)}) ⊆ ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})))
Theorem	lspsntrim 20369	Triangle-type inequality for span of a singleton of vector difference. (Contributed by NM, 25-Apr-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑁‘{(𝑋 − 𝑌)}) ⊆ ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})))
Theorem	lbspropd 20370*	If two structures have the same components (properties), they have the same set of bases. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 24-Apr-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    &   ⊢ 𝐹 = (Scalar‘𝐾)    &   ⊢ 𝐺 = (Scalar‘𝐿)    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐹))    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐺))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (LBasis‘𝐾) = (LBasis‘𝐿))
Theorem	pj1lmhm 20371	The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑃 = (proj1‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐿)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    ⇒   ⊢ (𝜑 → (𝑇𝑃𝑈) ∈ ((𝑊 ↾s (𝑇 ⊕ 𝑈)) LMHom 𝑊))
Theorem	pj1lmhm2 20372	The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑃 = (proj1‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐿)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    ⇒   ⊢ (𝜑 → (𝑇𝑃𝑈) ∈ ((𝑊 ↾s (𝑇 ⊕ 𝑈)) LMHom (𝑊 ↾s 𝑇)))
10.6  Vector spaces
10.6.1  Definition and basic properties
Syntax	clvec 20373	Extend class notation with class of all left vector spaces.
class LVec
Definition	df-lvec 20374	Define the class of all left vector spaces. A left vector space over a division ring is an Abelian group (vectors) together with a division ring (scalars) and a left scalar product connecting them. Some authors call this a "left module over a division ring", reserving "vector space" for those where the division ring is commutative, i.e., is a field. (Contributed by NM, 11-Nov-2013.)
⊢ LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing}
Theorem	islvec 20375	The predicate "is a left vector space". (Contributed by NM, 11-Nov-2013.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
Theorem	lvecdrng 20376	The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing)
Theorem	lveclmod 20377	A left vector space is a left module. (Contributed by NM, 9-Dec-2013.)
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
Theorem	lsslvec 20378	A vector subspace is a vector space. (Contributed by NM, 14-Mar-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LVec)
Theorem	lvecvs0or 20379	If a scalar product is zero, one of its factors must be zero. (hvmul0or 29396 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑂 = (0g‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) = 0 ↔ (𝐴 = 𝑂 ∨ 𝑋 = 0 )))
Theorem	lvecvsn0 20380	A scalar product is nonzero iff both of its factors are nonzero. (Contributed by NM, 3-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑂 = (0g‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) ≠ 0 ↔ (𝐴 ≠ 𝑂 ∧ 𝑋 ≠ 0 )))
Theorem	lssvs0or 20381	If a scalar product belongs to a subspace, either the scalar component is zero or the vector component also belongs to the subspace. (Contributed by NM, 5-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) ∈ 𝑈 ↔ (𝐴 = 0 ∨ 𝑋 ∈ 𝑈)))
Theorem	lvecvscan 20382	Cancellation law for scalar multiplication. (hvmulcan 29443 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) = (𝐴 · 𝑌) ↔ 𝑋 = 𝑌))
Theorem	lvecvscan2 20383	Cancellation law for scalar multiplication. (hvmulcan2 29444 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) = (𝐵 · 𝑋) ↔ 𝐴 = 𝐵))
Theorem	lvecinv 20384	Invert coefficient of scalar product. (Contributed by NM, 11-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ 𝐼 = (invr‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 = (𝐴 · 𝑌) ↔ 𝑌 = ((𝐼‘𝐴) · 𝑋)))
Theorem	lspsnvs 20385	A nonzero scalar product does not change the span of a singleton. (spansncol 29939 analog.) (Contributed by NM, 23-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉) → (𝑁‘{(𝑅 · 𝑋)}) = (𝑁‘{𝑋}))
Theorem	lspsneleq 20386	Membership relation that implies equality of spans. (spansneleq 29941 analog.) (Contributed by NM, 4-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋}))    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑋}))
Theorem	lspsncmp 20387	Comparable spans of nonzero singletons are equal. (Contributed by NM, 27-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}) ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌})))
Theorem	lspsnne1 20388	Two ways to express that vectors have different spans. (Contributed by NM, 28-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))
Theorem	lspsnne2 20389	Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
Theorem	lspsnnecom 20390	Swap two vectors with different spans. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋}))
Theorem	lspabs2 20391	Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))
Theorem	lspabs3 20392	Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 )    &   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)}))
Theorem	lspsneq 20393*	Equal spans of singletons must have proportional vectors. See lspsnss2 20276 for comparable span version. TODO: can proof be shortened? (Contributed by NM, 21-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑘 · 𝑌)))
Theorem	lspsneu 20394*	Nonzero vectors with equal singleton spans have a unique proportionality constant. (Contributed by NM, 31-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑂 = (0g‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃!𝑘 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑘 · 𝑌)))
Theorem	lspsnel4 20395	A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn4 29944 analog.) (Contributed by NM, 4-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋}))    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈))
Theorem	lspdisj 20396	The span of a vector not in a subspace is disjoint with the subspace. (Contributed by NM, 6-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ 𝑈) = { 0 })
Theorem	lspdisjb 20397	A nonzero vector is not in a subspace iff its span is disjoint with the subspace. (Contributed by NM, 23-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (¬ 𝑋 ∈ 𝑈 ↔ ((𝑁‘{𝑋}) ∩ 𝑈) = { 0 }))
Theorem	lspdisj2 20398	Unequal spans are disjoint (share only the zero vector). (Contributed by NM, 22-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ (𝑁‘{𝑌})) = { 0 })
Theorem	lspfixed 20399*	Show membership in the span of the sum of two vectors, one of which (𝑌) is fixed in advance. (Contributed by NM, 27-May-2015.) (Revised by AV, 12-Jul-2022.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}))
Theorem	lspexch 20400	Exchange property for span of a pair. TODO: see if a version with Y,Z and X,Z reversed will shorten proofs (analogous to lspexchn1 20401 versus lspexchn2 20402); look for lspexch 20400 and prcom 4669 in same proof. TODO: would a hypothesis of ¬ 𝑋 ∈ (𝑁‘{𝑍}) instead of (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}) be better overall? This would be shorter and also satisfy the 𝑋 ≠ 0 condition. Here and also lspindp* and all proofs affected by them (all in NM's mathbox); there are 58 hypotheses with the ≠ pattern as of 24-May-2015. (Contributed by NM, 11-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑍}))