P. 215 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21401-21500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lspsnne1 21401	Two ways to express that vectors have different spans. (Contributed by NM, 28-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))
Theorem	lspsnne2 21402	Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
Theorem	lspsnnecom 21403	Swap two vectors with different spans. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋}))
Theorem	lspabs2 21404	Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))
Theorem	lspabs3 21405	Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 )    &   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)}))
Theorem	lspsneq 21406*	Equal spans of singletons must have proportional vectors. See lspsnss2 21286 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 21407*	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	ellspsn4 21408	A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn4 32181 analog.) (Contributed by NM, 4-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋}))    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈))
Theorem	lspdisj 21409	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 21410	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 21411	Unequal spans are disjoint (share only the zero vector). (Contributed by NM, 22-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ (𝑁‘{𝑌})) = { 0 })
Theorem	lspfixed 21412*	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 21413	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 21414 versus lspexchn2 21415); look for lspexch 21413 and prcom 4689 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 21414	Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch 21413 to see if this will shorten proofs. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋, 𝑍}))
Theorem	lspexchn2 21415	Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch 21413 to see if this will shorten proofs. (Contributed by NM, 24-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍, 𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑋}))
Theorem	lspindpi 21416	Partial independence property. (Contributed by NM, 23-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))
Theorem	lspindp1 21417	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 21418	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 21419	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 21420	Independence of 2 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑋 + 𝑌)}))
Theorem	lspindp4 21421	(Partial) independence of 3 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑋 + 𝑌)}))
Theorem	lvecindp 21422	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 21423	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 21424	Unequal singleton spans imply nonzero vector subtraction. (Contributed by NM, 19-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ≠ 0 )
Theorem	lsmcv 21425	Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 32260 analog.) TODO: ugly proof; can it be shortened? (Contributed by NM, 2-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇 ⊕ (𝑁‘{𝑋}))) → 𝑈 = (𝑇 ⊕ (𝑁‘{𝑋})))
Theorem	lspsolvlem 21426*	Lemma for lspsolv 21427. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑄 = {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)}    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌})))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
Theorem	lspsolv 21427	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 21428*	In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 21248 by lspsolv 21427. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝑋 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝐴 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))))
Theorem	lspsnat 21429	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 32189 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 22-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (𝑈 = (𝑁‘{𝑋}) ∨ 𝑈 = { 0 }))
Theorem	lspsncv0 21430*	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 21431	Lemma for lspprat 21437. 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 21427 (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 21432	Lemma for lspprat 21437. 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 21433	Lemma for lspprat 21437. In the first case of lsppratlem1 21431, since 𝑥 ∉ (𝑁‘∅), also 𝑌 ∈ (𝑁‘{𝑥}), and since 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑋, 𝑥}) and 𝑦 ∉ (𝑁‘{𝑥}), we have 𝑋 ∈ (𝑁‘{𝑥, 𝑦}) as desired. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    &   ⊢ (𝜑 → 𝑥 ∈ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦})))
Theorem	lsppratlem4 21434	Lemma for lspprat 21437. In the second case of lsppratlem1 21431, 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑌}) and 𝑦 ∉ (𝑁‘{𝑥}) implies 𝑌 ∈ (𝑁‘{𝑥, 𝑦}) and thus 𝑋 ∈ (𝑁‘{𝑥, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑦}) as well. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦})))
Theorem	lsppratlem5 21435	Lemma for lspprat 21437. 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 21436	Lemma for lspprat 21437. 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 21437*	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 21438*	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 21439*	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 21440	Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 21438. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝐼 ∧ (𝑁‘𝑆) = 𝑋)))
Theorem	lvecdim 21441	The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 21428 and lbsacsbs 21440 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 18739. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽) → 𝑆 ≈ 𝑇)
Theorem	lbsextlem1 21442*	Lemma for lbsext 21447. 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 21443*	Lemma for lbsext 21447. 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 21444*	Lemma for lbsext 21447. A chain in 𝑆 has an upper bound in 𝑆. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))    &   ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}    &   ⊢ 𝑃 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝐴)    &   ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑆)
Theorem	lbsextlem4 21445*	Lemma for lbsext 21447. lbsextlem3 21444 satisfies the conditions for the application of Zorn's lemma zorn 10589 (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 21446*	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 21447*	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 21448	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 21449	Every vector space has a basis. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐽 ≠ ∅)
Theorem	lvecprop2d 21450*	If two structures have the same components (properties), one is a left vector space iff the other one is. This version of lvecpropd 21451 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 21451*	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  Subring algebras and ideals
10.7.1  Subring algebras
Syntax	csra 21452	Extend class notation with the subring algebra generator.
class subringAlg
Syntax	crglmod 21453	Extend class notation with the left module induced by a ring over itself.
class ringLMod
Definition	df-sra 21454*	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 21455	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‘𝑤)))
Theorem	sraval 21456	Lemma for srabase 21458 through sravsca 21462. (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 21457	Lemma for srabase 21458 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	srabase 21458	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	sraaddg 21459	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	sramulr 21460	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	srasca 21461	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	sravsca 21462	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‘𝑊) = ( ·𝑠 ‘𝐴))
Theorem	sraip 21463	The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = (·𝑖‘𝐴))
Theorem	sratset 21464	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (TopSet‘𝑊) = (TopSet‘𝐴))
Theorem	sratopn 21465	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (TopOpen‘𝑊) = (TopOpen‘𝐴))
Theorem	srads 21466	Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (dist‘𝑊) = (dist‘𝐴))
Theorem	sraring 21467	Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ Ring)
Theorem	sralmod 21468	The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆)    ⇒   ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod)
Theorem	sralmod0 21469	The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 0 = (0g‘𝑊))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → 0 = (0g‘𝐴))
Theorem	issubrgd 21470*	Prove a subring by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷))    &   ⊢ (𝜑 → 0 = (0g‘𝐼))    &   ⊢ (𝜑 → + = (+g‘𝐼))    &   ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼))    &   ⊢ (𝜑 → 0 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷)    &   ⊢ (𝜑 → 1 = (1r‘𝐼))    &   ⊢ (𝜑 → · = (.r‘𝐼))    &   ⊢ (𝜑 → 1 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 · 𝑦) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (SubRing‘𝐼))
Theorem	rlmfn 21471	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ ringLMod Fn V
Theorem	rlmval 21472	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊))
Theorem	rlmval2 21473	Value of the ring module extended. (Contributed by AV, 2-Dec-2018.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝑊 ∈ 𝑋 → (ringLMod‘𝑊) = (((𝑊 sSet ⟨(Scalar‘ndx), 𝑊⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑊)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑊)⟩))
Theorem	rlmbas 21474	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (Base‘𝑅) = (Base‘(ringLMod‘𝑅))
Theorem	rlmplusg 21475	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (+g‘𝑅) = (+g‘(ringLMod‘𝑅))
Theorem	rlm0 21476	Zero vector in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ (0g‘𝑅) = (0g‘(ringLMod‘𝑅))
Theorem	rlmsub 21477	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ (-g‘𝑅) = (-g‘(ringLMod‘𝑅))
Theorem	rlmmulr 21478	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (.r‘𝑅) = (.r‘(ringLMod‘𝑅))
Theorem	rlmsca 21479	Scalars in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ (𝑅 ∈ 𝑋 → 𝑅 = (Scalar‘(ringLMod‘𝑅)))
Theorem	rlmsca2 21480	Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ ( I ‘𝑅) = (Scalar‘(ringLMod‘𝑅))
Theorem	rlmvsca 21481	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (.r‘𝑅) = ( ·𝑠 ‘(ringLMod‘𝑅))
Theorem	rlmtopn 21482	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅))
Theorem	rlmds 21483	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (dist‘𝑅) = (dist‘(ringLMod‘𝑅))
Theorem	rlmlmod 21484	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ (𝑅 ∈ Ring → (ringLMod‘𝑅) ∈ LMod)
Theorem	rlmlvec 21485	The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ DivRing → (ringLMod‘𝑅) ∈ LVec)
Theorem	rlmlsm 21486	Subgroup sum of the ring module. (Contributed by Thierry Arnoux, 9-Apr-2024.)
⊢ (𝑅 ∈ 𝑉 → (LSSum‘𝑅) = (LSSum‘(ringLMod‘𝑅)))
Theorem	rlmvneg 21487	Vector negation in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 5-Jun-2015.)
⊢ (invg‘𝑅) = (invg‘(ringLMod‘𝑅))
Theorem	rlmscaf 21488	Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (+𝑓‘(mulGrp‘𝑅)) = ( ·sf ‘(ringLMod‘𝑅))
Theorem	ixpsnbasval 21489*	The value of an infinite Cartesian product of the base of a left module over a ring with a singleton. (Contributed by AV, 3-Dec-2018.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅))})
10.7.2  Left ideals and spans Remark: Usually, (left) ideals are defined as a subset of a (unital or non-unital) ring that is a subgroup of the additive group of the ring that "absorbs multiplication from the left by elements of the ring", see Wikipedia https://en.wikipedia.org/wiki/Ideal_(ring_theory) (19.02.2025), or the definition 4 in [BourbakiAlg1] p. 103 and the definition in [Lang] p.86, although a ring is to be considered unital (and commutative!) here, see definition 1 in [BourbakiAlg1] p. 96 resp. the definition in [Lang] p. 83, or definition in [Roman] p. 20. In contrast, the definition of (LIdeal‘𝑅), does not require the subset to be a subgroup of the additive group, as can be seen by islidl 21500. If 𝑅 is a unital ring, however, it can be proven that each ideal in (LIdeal‘𝑅) is a subgroup of the additive group of the ring, see lidlsubg 21508. This is not possible for arbitrary non-unital rings, because the proof uses the existence of the ring unity.
Syntax	clidl 21490	Ring left-ideal function.
class LIdeal
Syntax	crsp 21491	Ring span function.
class RSpan
Definition	df-lidl 21492	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 dflidl2rng 21503 and dflidl2 21513. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ LIdeal = (LSubSp ∘ ringLMod)
Definition	df-rsp 21493	Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ RSpan = (LSpan ∘ ringLMod)
Theorem	lidlval 21494	Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊))
Theorem	rspval 21495	Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊))
Theorem	lidlss 21496	An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (LIdeal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵)
Theorem	lidlbasel 21497	An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by AV, 27-Jun-2026.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (LIdeal‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝐼 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ 𝐵)
Theorem	lidlssbas 21498	The base set of the restriction of the ring to a (left) ideal is a subset of the base set of the ring. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅))
Theorem	lidlbas 21499	A (left) ideal of a ring is the base set of the restriction of the ring to this ideal. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) = 𝑈)
Theorem	islidl 21500*	Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝐼 ∈ 𝑈 ↔ (𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐼 ((𝑥 · 𝑎) + 𝑏) ∈ 𝐼))