P. 208 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20701-20800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lsppreli 20701	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 20702	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 20703	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 20704*	Span of a pair of vectors. (Contributed by NM, 22-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = {𝑣 ∣ ∃𝑘 ∈ 𝐾 ∃𝑙 ∈ 𝐾 𝑣 = ((𝑘 · 𝑋) + (𝑙 · 𝑌))})
Theorem	lspprel 20705*	Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑁‘{𝑋, 𝑌}) ↔ ∃𝑘 ∈ 𝐾 ∃𝑙 ∈ 𝐾 𝑍 = ((𝑘 · 𝑋) + (𝑙 · 𝑌))))
Theorem	lspprabs 20706	Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, (𝑋 + 𝑌)}) = (𝑁‘{𝑋, 𝑌}))
Theorem	lspvadd 20707	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 20708	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 20709	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 20710*	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 20711	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 20712	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 20713	Extend class notation with class of all left vector spaces.
class LVec
Definition	df-lvec 20714	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 20715	The predicate "is a left vector space". (Contributed by NM, 11-Nov-2013.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
Theorem	lvecdrng 20716	The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing)
Theorem	lveclmod 20717	A left vector space is a left module. (Contributed by NM, 9-Dec-2013.)
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
Theorem	lveclmodd 20718	A vector space is a left module. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑊 ∈ LVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ LMod)
Theorem	lsslvec 20719	A vector subspace is a vector space. (Contributed by NM, 14-Mar-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LVec)
Theorem	lmhmlvec 20720	The property for modules to be vector spaces is invariant under module isomorphism. (Contributed by Steven Nguyen, 15-Aug-2023.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑆 ∈ LVec ↔ 𝑇 ∈ LVec))
Theorem	lvecvs0or 20721	If a scalar product is zero, one of its factors must be zero. (hvmul0or 30278 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑂 = (0g‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) = 0 ↔ (𝐴 = 𝑂 ∨ 𝑋 = 0 )))
Theorem	lvecvsn0 20722	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 20723	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 20724	Cancellation law for scalar multiplication. (hvmulcan 30325 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) = (𝐴 · 𝑌) ↔ 𝑋 = 𝑌))
Theorem	lvecvscan2 20725	Cancellation law for scalar multiplication. (hvmulcan2 30326 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) = (𝐵 · 𝑋) ↔ 𝐴 = 𝐵))
Theorem	lvecinv 20726	Invert coefficient of scalar product. (Contributed by NM, 11-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ 𝐼 = (invr‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 = (𝐴 · 𝑌) ↔ 𝑌 = ((𝐼‘𝐴) · 𝑋)))
Theorem	lspsnvs 20727	A nonzero scalar product does not change the span of a singleton. (spansncol 30821 analog.) (Contributed by NM, 23-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉) → (𝑁‘{(𝑅 · 𝑋)}) = (𝑁‘{𝑋}))
Theorem	lspsneleq 20728	Membership relation that implies equality of spans. (spansneleq 30823 analog.) (Contributed by NM, 4-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋}))    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑋}))
Theorem	lspsncmp 20729	Comparable spans of nonzero singletons are equal. (Contributed by NM, 27-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}) ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌})))
Theorem	lspsnne1 20730	Two ways to express that vectors have different spans. (Contributed by NM, 28-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))
Theorem	lspsnne2 20731	Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
Theorem	lspsnnecom 20732	Swap two vectors with different spans. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋}))
Theorem	lspabs2 20733	Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))
Theorem	lspabs3 20734	Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 )    &   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)}))
Theorem	lspsneq 20735*	Equal spans of singletons must have proportional vectors. See lspsnss2 20616 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 20736*	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 20737	A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn4 30826 analog.) (Contributed by NM, 4-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋}))    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈))
Theorem	lspdisj 20738	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 20739	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 20740	Unequal spans are disjoint (share only the zero vector). (Contributed by NM, 22-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ (𝑁‘{𝑌})) = { 0 })
Theorem	lspfixed 20741*	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 20742	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 20743 versus lspexchn2 20744); look for lspexch 20742 and prcom 4737 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 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑍}))
Theorem	lspexchn1 20743	Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch 20742 to see if this will shorten proofs. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋, 𝑍}))
Theorem	lspexchn2 20744	Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch 20742 to see if this will shorten proofs. (Contributed by NM, 24-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍, 𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑋}))
Theorem	lspindpi 20745	Partial independence property. (Contributed by NM, 23-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))
Theorem	lspindp1 20746	Alternate way to say 3 vectors are mutually independent (swap 1st and 2nd). (Contributed by NM, 11-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑍}) ≠ (𝑁‘{𝑌}) ∧ ¬ 𝑋 ∈ (𝑁‘{𝑍, 𝑌})))
Theorem	lspindp2l 20747	Alternate way to say 3 vectors are mutually independent (rotate left). (Contributed by NM, 10-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}) ∧ ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
Theorem	lspindp2 20748	Alternate way to say 3 vectors are mutually independent (rotate right). (Contributed by NM, 12-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑍}) ≠ (𝑁‘{𝑋}) ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑋})))
Theorem	lspindp3 20749	Independence of 2 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑋 + 𝑌)}))
Theorem	lspindp4 20750	(Partial) independence of 3 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑋 + 𝑌)}))
Theorem	lvecindp 20751	Compute the 𝑋 coefficient in a sum with an independent vector 𝑋 (first conjunct), which can then be removed to continue with the remaining vectors summed in expressions 𝑌 and 𝑍 (second conjunct). Typically, 𝑈 is the span of the remaining vectors. (Contributed by NM, 5-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 19-Jul-2022.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝑌) = ((𝐵 · 𝑋) + 𝑍))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ∧ 𝑌 = 𝑍))
Theorem	lvecindp2 20752	Sums of independent vectors must have equal coefficients. (Contributed by NM, 22-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐾)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐶 · 𝑋) + (𝐷 · 𝑌)))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	lspsnsubn0 20753	Unequal singleton spans imply nonzero vector subtraction. (Contributed by NM, 19-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ≠ 0 )
Theorem	lsmcv 20754	Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 30905 analog.) TODO: ugly proof; can it be shortened? (Contributed by NM, 2-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇 ⊕ (𝑁‘{𝑋}))) → 𝑈 = (𝑇 ⊕ (𝑁‘{𝑋})))
Theorem	lspsolvlem 20755*	Lemma for lspsolv 20756. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑄 = {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)}    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌})))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
Theorem	lspsolv 20756	If 𝑋 is in the span of 𝐴 ∪ {𝑌} but not 𝐴, then 𝑌 is in the span of 𝐴 ∪ {𝑋}. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → 𝑌 ∈ (𝑁‘(𝐴 ∪ {𝑋})))
Theorem	lssacsex 20757*	In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 20578 by lspsolv 20756. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝑋 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝐴 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))))
Theorem	lspsnat 20758	There is no subspace strictly between the zero subspace and the span of a vector (i.e. a 1-dimensional subspace is an atom). (h1datomi 30834 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 22-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (𝑈 = (𝑁‘{𝑋}) ∨ 𝑈 = { 0 }))
Theorem	lspsncv0 20759*	The span of a singleton covers the zero subspace, using Definition 3.2.18 of [PtakPulmannova] p. 68 for "covers".) (Contributed by NM, 12-Aug-2014.) (Revised by AV, 13-Jul-2022.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ¬ ∃𝑦 ∈ 𝑆 ({ 0 } ⊊ 𝑦 ∧ 𝑦 ⊊ (𝑁‘{𝑋})))
Theorem	lsppratlem1 20760	Lemma for lspprat 20766. Let 𝑥 ∈ (𝑈 ∖ {0}) (if there is no such 𝑥 then 𝑈 is the zero subspace), and let 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})) (assuming the conclusion is false). The goal is to write 𝑋, 𝑌 in terms of 𝑥, 𝑦, which would normally be done by solving the system of linear equations. The span equivalent of this process is lspsolv 20756 (hence the name), which we use extensively below. In this lemma, we show that since 𝑥 ∈ (𝑁‘{𝑋, 𝑌}), either 𝑥 ∈ (𝑁‘{𝑌}) or 𝑋 ∈ (𝑁‘{𝑥, 𝑌}). (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝑁‘{𝑌}) ∨ 𝑋 ∈ (𝑁‘{𝑥, 𝑌})))
Theorem	lsppratlem2 20761	Lemma for lspprat 20766. Show that if 𝑋 and 𝑌 are both in (𝑁‘{𝑥, 𝑦}) (which will be our goal for each of the two cases above), then (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈, contradicting the hypothesis for 𝑈. (Contributed by NM, 29-Aug-2014.) (Revised by Mario Carneiro, 5-Sep-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑦}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑥, 𝑦}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈)
Theorem	lsppratlem3 20762	Lemma for lspprat 20766. In the first case of lsppratlem1 20760, since 𝑥 ∉ (𝑁‘∅), also 𝑌 ∈ (𝑁‘{𝑥}), and since 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑋, 𝑥}) and 𝑦 ∉ (𝑁‘{𝑥}), we have 𝑋 ∈ (𝑁‘{𝑥, 𝑦}) as desired. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    &   ⊢ (𝜑 → 𝑥 ∈ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦})))
Theorem	lsppratlem4 20763	Lemma for lspprat 20766. In the second case of lsppratlem1 20760, 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑌}) and 𝑦 ∉ (𝑁‘{𝑥}) implies 𝑌 ∈ (𝑁‘{𝑥, 𝑦}) and thus 𝑋 ∈ (𝑁‘{𝑥, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑦}) as well. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦})))
Theorem	lsppratlem5 20764	Lemma for lspprat 20766. Combine the two cases and show a contradiction to 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}) under the assumptions on 𝑥 and 𝑦. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈)
Theorem	lsppratlem6 20765	Lemma for lspprat 20766. Negating the assumption on 𝑦, we arrive close to the desired conclusion. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝑈 ∖ { 0 }) → 𝑈 = (𝑁‘{𝑥})))
Theorem	lspprat 20766*	A proper subspace of the span of a pair of vectors is the span of a singleton (an atom) or the zero subspace (if 𝑧 is zero). Proof suggested by Mario Carneiro, 28-Aug-2014. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 𝑈 = (𝑁‘{𝑧}))
Theorem	islbs2 20767*	An equivalent formulation of the basis predicate in a vector space: a subset is a basis iff no element is in the span of the rest of the set. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
Theorem	islbs3 20768*	An equivalent formulation of the basis predicate: a subset is a basis iff it is a minimal spanning set. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑠(𝑠 ⊊ 𝐵 → (𝑁‘𝑠) ⊊ 𝑉))))
Theorem	lbsacsbs 20769	Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 20767. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝐼 ∧ (𝑁‘𝑆) = 𝑋)))
Theorem	lvecdim 20770	The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 20757 and lbsacsbs 20769 to show that being a basis for a vector space is equivalent to being a basis for the associated algebraic closure system, and then using acsexdimd 18512. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽) → 𝑆 ≈ 𝑇)
Theorem	lbsextlem1 20771*	Lemma for lbsext 20776. The set 𝑆 is the set of all linearly independent sets containing 𝐶; we show here that it is nonempty. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))    &   ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}    ⇒   ⊢ (𝜑 → 𝑆 ≠ ∅)
Theorem	lbsextlem2 20772*	Lemma for lbsext 20776. Since 𝐴 is a chain (actually, we only need it to be closed under binary union), the union 𝑇 of the spans of each individual element of 𝐴 is a subspace, and it contains all of ∪ 𝐴 (except for our target vector 𝑥- we are trying to make 𝑥 a linear combination of all the other vectors in some set from 𝐴). (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))    &   ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}    &   ⊢ 𝑃 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝐴)    &   ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))    ⇒   ⊢ (𝜑 → (𝑇 ∈ 𝑃 ∧ (∪ 𝐴 ∖ {𝑥}) ⊆ 𝑇))
Theorem	lbsextlem3 20773*	Lemma for lbsext 20776. A chain in 𝑆 has an upper bound in 𝑆. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))    &   ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}    &   ⊢ 𝑃 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝐴)    &   ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑆)
Theorem	lbsextlem4 20774*	Lemma for lbsext 20776. lbsextlem3 20773 satisfies the conditions for the application of Zorn's lemma zorn 10502 (thus invoking AC), and so there is a maximal linearly independent set extending 𝐶. Here we prove that such a set is a basis. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))    &   ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}    &   ⊢ (𝜑 → 𝒫 𝑉 ∈ dom card)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠)
Theorem	lbsextg 20775*	For any linearly independent subset 𝐶 of 𝑉, there is a basis containing the vectors in 𝐶. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card) ∧ 𝐶 ⊆ 𝑉 ∧ ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠)
Theorem	lbsext 20776*	For any linearly independent subset 𝐶 of 𝑉, there is a basis containing the vectors in 𝐶. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐶 ⊆ 𝑉 ∧ ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠)
Theorem	lbsexg 20777	Every vector space has a basis. This theorem is an AC equivalent; this is the forward implication. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ ((CHOICE ∧ 𝑊 ∈ LVec) → 𝐽 ≠ ∅)
Theorem	lbsex 20778	Every vector space has a basis. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐽 ≠ ∅)
Theorem	lvecprop2d 20779*	If two structures have the same components (properties), one is a left vector space iff the other one is. This version of lvecpropd 20780 also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ 𝐹 = (Scalar‘𝐾)    &   ⊢ 𝐺 = (Scalar‘𝐿)    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐹))    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐺))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(.r‘𝐹)𝑦) = (𝑥(.r‘𝐺)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ LVec ↔ 𝐿 ∈ LVec))
Theorem	lvecpropd 20780*	If two structures have the same components (properties), one is a left vector space iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐾))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐿))    &   ⊢ 𝑃 = (Base‘𝐹)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ LVec ↔ 𝐿 ∈ LVec))
10.7  Ideals
10.7.1  The subring algebra; ideals
Syntax	csra 20781	Extend class notation with the subring algebra generator.
class subringAlg
Syntax	crglmod 20782	Extend class notation with the left module induced by a ring over itself.
class ringLMod
Syntax	clidl 20783	Ring left-ideal function.
class LIdeal
Syntax	crsp 20784	Ring span function.
class RSpan
Definition	df-sra 20785*	Any ring can be regarded as a left algebra over any of its subrings. The function subringAlg associates with any ring and any of its subrings the left algebra consisting in the ring itself regarded as a left algebra over the subring. It has an inner product which is simply the ring product. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ subringAlg = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩)))
Definition	df-rgmod 20786	Any ring can be regarded as a left algebra over itself. The function ringLMod associates with any ring the left algebra consisting in the ring itself regarded as a left algebra over itself. It has an inner product which is simply the ring product. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ ringLMod = (𝑤 ∈ V ↦ ((subringAlg ‘𝑤)‘(Base‘𝑤)))
Definition	df-lidl 20787	Define the class of left ideals of a given ring. An ideal is a submodule of the ring viewed as a module over itself. For the usual textbook definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring, see dflidl2 20843. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ LIdeal = (LSubSp ∘ ringLMod)
Definition	df-rsp 20788	Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ RSpan = (LSpan ∘ ringLMod)
Theorem	sraval 20789	Lemma for srabase 20792 through sravsca 20800. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet ⟨(Scalar‘ndx), (𝑊 ↾s 𝑆)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑊)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑊)⟩))
Theorem	sralem 20790	Lemma for srabase 20792 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (Scalar‘ndx) ≠ (𝐸‘ndx)    &   ⊢ ( ·𝑠 ‘ndx) ≠ (𝐸‘ndx)    &   ⊢ (·𝑖‘ndx) ≠ (𝐸‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘𝐴))
Theorem	sralemOLD 20791	Obsolete version of sralem 20790 as of 29-Oct-2024. Lemma for srabase 20792 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ (𝑁 < 5 ∨ 8 < 𝑁)    ⇒   ⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘𝐴))
Theorem	srabase 20792	Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (Base‘𝑊) = (Base‘𝐴))
Theorem	srabaseOLD 20793	Obsolete proof of srabase 20792 as of 29-Oct-2024. Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (Base‘𝑊) = (Base‘𝐴))
Theorem	sraaddg 20794	Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (+g‘𝑊) = (+g‘𝐴))
Theorem	sraaddgOLD 20795	Obsolete proof of sraaddg 20794 as of 29-Oct-2024. Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (+g‘𝑊) = (+g‘𝐴))
Theorem	sramulr 20796	Multiplicative operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = (.r‘𝐴))
Theorem	sramulrOLD 20797	Obsolete proof of sramulr 20796 as of 29-Oct-2024. Multiplicative operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = (.r‘𝐴))
Theorem	srasca 20798	The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (𝑊 ↾s 𝑆) = (Scalar‘𝐴))
Theorem	srascaOLD 20799	Obsolete proof of srasca 20798 as of 12-Nov-2024. The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 12-Nov-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (𝑊 ↾s 𝑆) = (Scalar‘𝐴))
Theorem	sravsca 20800	The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = ( ·𝑠 ‘𝐴))