P. 392 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39101-39200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lshpne 39101	A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → 𝑈 ≠ 𝑉)
Theorem	lshpnel 39102	A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
Theorem	lshpnelb 39103	The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (¬ 𝑋 ∈ 𝑈 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉))
Theorem	lshpnel2N 39104	Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉))
Theorem	lshpne0 39105	The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014.) (Proof shortened by AV, 19-Jul-2022.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 0 )
Theorem	lshpdisj 39106	A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)    ⇒   ⊢ (𝜑 → (𝑈 ∩ (𝑁‘{𝑋})) = { 0 })
Theorem	lshpcmp 39107	If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lshpinN 39108	The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → ((𝑇 ∩ 𝑈) ∈ 𝐻 ↔ 𝑇 = 𝑈))
Theorem	lsatset 39109*	The set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝐴 = ran (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})))
Theorem	islsat 39110*	The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑈 = (𝑁‘{𝑥})))
Theorem	lsatlspsn2 39111	The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 39112 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) ∈ 𝐴)
Theorem	lsatlspsn 39112	The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ 𝐴)
Theorem	islsati 39113*	A 1-dim subspace (atom) (of a left module or left vector space) equals the span of some vector. (Contributed by NM, 1-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑈 ∈ 𝐴) → ∃𝑣 ∈ 𝑉 𝑈 = (𝑁‘{𝑣}))
Theorem	lsateln0 39114*	A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ 𝑈 𝑣 ≠ 0 )
Theorem	lsatlss 39115	The set of 1-dim subspaces is a set of subspaces. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝐴 ⊆ 𝑆)
Theorem	lsatlssel 39116	An atom is a subspace. (Contributed by NM, 25-Aug-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	lsatssv 39117	An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑄 ⊆ 𝑉)
Theorem	lsatn0 39118	A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 32327 analog.) (Contributed by NM, 25-Aug-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑈 ≠ { 0 })
Theorem	lsatspn0 39119	The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∈ 𝐴 ↔ 𝑋 ≠ 0 ))
Theorem	lsator0sp 39120	The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∈ 𝐴 ∨ (𝑁‘{𝑋}) = { 0 }))
Theorem	lsatssn0 39121	A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑈 ≠ { 0 })
Theorem	lsatcmp 39122	If two atoms are comparable, they are equal. (atsseq 32329 analog.) TODO: can lspsncmp 21055 shorten this? (Contributed by NM, 25-Aug-2014.)
⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lsatcmp2 39123	If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 39122. TODO: can lspsncmp 21055 shorten this? (Contributed by NM, 3-Feb-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∨ 𝑈 = { 0 }))    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lsatel 39124	A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → 𝑈 = (𝑁‘{𝑋}))
Theorem	lsatelbN 39125	A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ 𝑈 = (𝑁‘{𝑋})))
Theorem	lsat2el 39126	Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑄)    ⇒   ⊢ (𝜑 → 𝑃 = 𝑄)
Theorem	lsmsat 39127*	Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 39924 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑇 ≠ { 0 })    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑇 ⊕ 𝑈))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈)))
Theorem	lsatfixedN 39128*	Show equality with the span of the sum of two vectors, one of which (𝑋) is fixed in advance. Compare lspfixed 21067. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑋}))    &   ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)}))
Theorem	lsmsatcv 39129	Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 31634 analog.) Explicit atom version of lsmcv 21080. (Contributed by NM, 29-Oct-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇 ⊕ 𝑄)) → 𝑈 = (𝑇 ⊕ 𝑄))
Theorem	lssatomic 39130*	The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 32340 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ≠ { 0 })    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈)
Theorem	lssats 39131*	The lattice of subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. Hypothesis (shatomistici 32343 analog.) (Contributed by NM, 9-Apr-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 = (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}))
Theorem	lpssat 39132*	Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 32345 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ⊊ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇))
Theorem	lrelat 39133*	Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 32346 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ⊊ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑇 ⊊ (𝑇 ⊕ 𝑞) ∧ (𝑇 ⊕ 𝑞) ⊆ 𝑈))
Theorem	lssatle 39134*	The ordering of two subspaces is determined by the atoms under them. (chrelat3 32353 analog.) (Contributed by NM, 29-Oct-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈)))
Theorem	lssat 39135*	Two subspaces in a proper subset relationship imply the existence of a 1-dim subspace less than or equal to one but not the other. (chpssati 32345 analog.) (Contributed by NM, 9-Apr-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆) ∧ 𝑈 ⊊ 𝑉) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈))
Theorem	islshpat 39136*	Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 39099. (Contributed by NM, 11-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑞 ∈ 𝐴 (𝑈 ⊕ 𝑞) = 𝑉)))
Syntax	clcv 39137	Extend class notation with the covering relation for a left module or left vector space.
class ⋖L
Definition	df-lcv 39138*	Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of [PtakPulmannova] p. 68. Ptak/Pulmannova's notation 𝐴( ⋖L ‘𝑊)𝐵 is read "𝐵 covers 𝐴 " or "𝐴 is covered by 𝐵 " , and it means that 𝐵 is larger than 𝐴 and there is nothing in between. See lcvbr 39140 for binary relation. (df-cv 32261 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ ⋖L = (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))})
Theorem	lcvfbr 39139*	The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐶 = {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))})
Theorem	lcvbr 39140*	The covers relation for a left vector space (or a left module). (cvbr 32264 analog.) (Contributed by NM, 9-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇𝐶𝑈 ↔ (𝑇 ⊊ 𝑈 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈))))
Theorem	lcvbr2 39141*	The covers relation for a left vector space (or a left module). (cvbr2 32265 analog.) (Contributed by NM, 9-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇𝐶𝑈 ↔ (𝑇 ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 ((𝑇 ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈))))
Theorem	lcvbr3 39142*	The covers relation for a left vector space (or a left module). (Contributed by NM, 9-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇𝐶𝑈 ↔ (𝑇 ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 ((𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈) → (𝑠 = 𝑇 ∨ 𝑠 = 𝑈)))))
Theorem	lcvpss 39143	The covers relation implies proper subset. (cvpss 32267 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇𝐶𝑈)    ⇒   ⊢ (𝜑 → 𝑇 ⊊ 𝑈)
Theorem	lcvnbtwn 39144	The covers relation implies no in-betweenness. (cvnbtwn 32268 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅𝐶𝑇)    ⇒   ⊢ (𝜑 → ¬ (𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇))
Theorem	lcvntr 39145	The covers relation is not transitive. (cvntr 32274 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅𝐶𝑇)    &   ⊢ (𝜑 → 𝑇𝐶𝑈)    ⇒   ⊢ (𝜑 → ¬ 𝑅𝐶𝑈)
Theorem	lcvnbtwn2 39146	The covers relation implies no in-betweenness. (cvnbtwn2 32269 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅𝐶𝑇)    &   ⊢ (𝜑 → 𝑅 ⊊ 𝑈)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑇)    ⇒   ⊢ (𝜑 → 𝑈 = 𝑇)
Theorem	lcvnbtwn3 39147	The covers relation implies no in-betweenness. (cvnbtwn3 32270 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅𝐶𝑇)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝑈 ⊊ 𝑇)    ⇒   ⊢ (𝜑 → 𝑈 = 𝑅)
Theorem	lsmcv2 39148	Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 32275 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ (𝑁‘{𝑋}) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑈𝐶(𝑈 ⊕ (𝑁‘{𝑋})))
Theorem	lcvat 39149*	If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 32348 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇𝐶𝑈)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑇 ⊕ 𝑞) = 𝑈)
Theorem	lsatcv0 39150	An atom covers the zero subspace. (atcv0 32324 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → { 0 }𝐶𝑄)
Theorem	lsatcveq0 39151	A subspace covered by an atom must be the zero subspace. (atcveq0 32330 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑈𝐶𝑄 ↔ 𝑈 = { 0 }))
Theorem	lsat0cv 39152	A subspace is an atom iff it covers the zero subspace. This could serve as an alternate definition of an atom. TODO: this is a quick-and-dirty proof that could probably be more efficient. (Contributed by NM, 14-Mar-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ↔ { 0 }𝐶𝑈))
Theorem	lcvexchlem1 39153	Lemma for lcvexch 39158. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇 ⊊ (𝑇 ⊕ 𝑈) ↔ (𝑇 ∩ 𝑈) ⊊ 𝑈))
Theorem	lcvexchlem2 39154	Lemma for lcvexch 39158. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑅 ⊕ 𝑇) ∩ 𝑈) = 𝑅)
Theorem	lcvexchlem3 39155	Lemma for lcvexch 39158. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝑇 ⊕ 𝑈))    ⇒   ⊢ (𝜑 → ((𝑅 ∩ 𝑈) ⊕ 𝑇) = 𝑅)
Theorem	lcvexchlem4 39156	Lemma for lcvexch 39158. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇𝐶(𝑇 ⊕ 𝑈))    ⇒   ⊢ (𝜑 → (𝑇 ∩ 𝑈)𝐶𝑈)
Theorem	lcvexchlem5 39157	Lemma for lcvexch 39158. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈)𝐶𝑈)    ⇒   ⊢ (𝜑 → 𝑇𝐶(𝑇 ⊕ 𝑈))
Theorem	lcvexch 39158	Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 32351 analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝑇 ∩ 𝑈)𝐶𝑈 ↔ 𝑇𝐶(𝑇 ⊕ 𝑈)))
Theorem	lcvp 39159	Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32357 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑈 ∩ 𝑄) = { 0 } ↔ 𝑈𝐶(𝑈 ⊕ 𝑄)))
Theorem	lcv1 39160	Covering property of a subspace plus an atom. (chcv1 32337 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈𝐶(𝑈 ⊕ 𝑄)))
Theorem	lcv2 39161	Covering property of a subspace plus an atom. (chcv2 32338 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑈 ⊊ (𝑈 ⊕ 𝑄) ↔ 𝑈𝐶(𝑈 ⊕ 𝑄)))
Theorem	lsatexch 39162	The atom exchange property. Proposition 1(i) of [Kalmbach] p. 140. A version of this theorem was originally proved by Hermann Grassmann in 1862. (atexch 32363 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑈 ⊕ 𝑅))    &   ⊢ (𝜑 → (𝑈 ∩ 𝑄) = { 0 })    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (𝑈 ⊕ 𝑄))
Theorem	lsatnle 39163	The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 32358 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ (𝑈 ∩ 𝑄) = { 0 }))
Theorem	lsatnem0 39164	The meet of distinct atoms is the zero subspace. (atnemeq0 32359 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑄 ≠ 𝑅 ↔ (𝑄 ∩ 𝑅) = { 0 }))
Theorem	lsatexch1 39165	The atom exch1ange property. (hlatexch1 39514 analog.) (Contributed by NM, 14-Jan-2015.)
⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑆 ⊕ 𝑅))    &   ⊢ (𝜑 → 𝑄 ≠ 𝑆)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (𝑆 ⊕ 𝑄))
Theorem	lsatcv0eq 39166	If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 32361 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ({ 0 }𝐶(𝑄 ⊕ 𝑅) ↔ 𝑄 = 𝑅))
Theorem	lsatcv1 39167	Two atoms covering the zero subspace are equal. (atcv1 32362 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈𝐶(𝑄 ⊕ 𝑅))    ⇒   ⊢ (𝜑 → (𝑈 = { 0 } ↔ 𝑄 = 𝑅))
Theorem	lsatcvatlem 39168	Lemma for lsatcvat 39169. (Contributed by NM, 10-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 ≠ { 0 })    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑄 ⊕ 𝑅))    &   ⊢ (𝜑 → ¬ 𝑄 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐴)
Theorem	lsatcvat 39169	A nonzero subspace less than the sum of two atoms is an atom. (atcvati 32368 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 ≠ { 0 })    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑄 ⊕ 𝑅))    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐴)
Theorem	lsatcvat2 39170	A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 32369 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑅)    &   ⊢ (𝜑 → 𝑈𝐶(𝑄 ⊕ 𝑅))    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐴)
Theorem	lsatcvat3 39171	A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 32378 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑅)    &   ⊢ (𝜑 → ¬ 𝑅 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑈 ⊕ 𝑅))    ⇒   ⊢ (𝜑 → (𝑈 ∩ (𝑄 ⊕ 𝑅)) ∈ 𝐴)
Theorem	islshpcv 39172	Hyperplane properties expressed with covers relation. (Contributed by NM, 11-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)))
Theorem	l1cvpat 39173	A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. (1cvrjat 39594 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈𝐶𝑉)    &   ⊢ (𝜑 → ¬ 𝑄 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → (𝑈 ⊕ 𝑄) = 𝑉)
Theorem	l1cvat 39174	Create an atom under an element covered by the lattice unity. Part of proof of Lemma B in [Crawley] p. 112. (1cvrat 39595 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑅)    &   ⊢ (𝜑 → 𝑈𝐶𝑉)    &   ⊢ (𝜑 → ¬ 𝑄 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑄 ⊕ 𝑅) ∩ 𝑈) ∈ 𝐴)
Theorem	lshpat 39175	Create an atom under a hyperplane. Part of proof of Lemma B in [Crawley] p. 112. (lhpat 40162 analog.) TODO: This changes 𝑈𝐶𝑉 in l1cvpat 39173 and l1cvat 39174 to 𝑈 ∈ 𝐻, which in turn change 𝑈 ∈ 𝐻 in islshpcv 39172 to 𝑈𝐶𝑉, with a couple of conversions of span to atom. Seems convoluted. Would a direct proof be better? (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑅)    &   ⊢ (𝜑 → ¬ 𝑄 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑄 ⊕ 𝑅) ∩ 𝑈) ∈ 𝐴)
21.28.7  Functionals and kernels of a left vector space (or module)
Syntax	clfn 39176	Extend class notation with all linear functionals of a left module or left vector space.
class LFnl
Definition	df-lfl 39177*	Define the set of all linear functionals (maps from vectors to the ring) of a left module or left vector space. (Contributed by NM, 15-Apr-2014.)
⊢ LFnl = (𝑤 ∈ V ↦ {𝑓 ∈ ((Base‘(Scalar‘𝑤)) ↑m (Base‘𝑤)) ∣ ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))})
Theorem	lflset 39178*	The set of linear functionals in a left module or left vector space. (Contributed by NM, 15-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ ⨣ = (+g‘𝐷)    &   ⊢ × = (.r‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝐹 = {𝑓 ∈ (𝐾 ↑m 𝑉) ∣ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑓‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝑓‘𝑥)) ⨣ (𝑓‘𝑦))})
Theorem	islfl 39179*	The predicate "is a linear functional". (Contributed by NM, 15-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ ⨣ = (+g‘𝐷)    &   ⊢ × = (.r‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝐺 ∈ 𝐹 ↔ (𝐺:𝑉⟶𝐾 ∧ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦)))))
Theorem	lfli 39180	Property of a linear functional. (lnfnli 32022 analog.) (Contributed by NM, 16-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ ⨣ = (+g‘𝐷)    &   ⊢ × = (.r‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐺‘((𝑅 · 𝑋) + 𝑌)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑌)))
Theorem	islfld 39181*	Properties that determine a linear functional. TODO: use this in place of islfl 39179 when it shortens the proof. (Contributed by NM, 19-Oct-2014.)
⊢ (𝜑 → 𝑉 = (Base‘𝑊))    &   ⊢ (𝜑 → + = (+g‘𝑊))    &   ⊢ (𝜑 → 𝐷 = (Scalar‘𝑊))    &   ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝐷))    &   ⊢ (𝜑 → ⨣ = (+g‘𝐷))    &   ⊢ (𝜑 → × = (.r‘𝐷))    &   ⊢ (𝜑 → 𝐹 = (LFnl‘𝑊))    &   ⊢ (𝜑 → 𝐺:𝑉⟶𝐾)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦)))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐹)
Theorem	lflf 39182	A linear functional is a function from vectors to scalars. (lnfnfi 32023 analog.) (Contributed by NM, 15-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → 𝐺:𝑉⟶𝐾)
Theorem	lflcl 39183	A linear functional value is a scalar. (Contributed by NM, 15-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → (𝐺‘𝑋) ∈ 𝐾)
Theorem	lfl0 39184	A linear functional is zero at the zero vector. (lnfn0i 32024 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝑍 = (0g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘𝑍) = 0 )
Theorem	lfladd 39185	Property of a linear functional. (lnfnaddi 32025 analog.) (Contributed by NM, 18-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ ⨣ = (+g‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐺‘(𝑋 + 𝑌)) = ((𝐺‘𝑋) ⨣ (𝐺‘𝑌)))
Theorem	lflsub 39186	Property of a linear functional. (lnfnaddi 32025 analog.) (Contributed by NM, 18-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝑀 = (-g‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐺‘(𝑋 − 𝑌)) = ((𝐺‘𝑋)𝑀(𝐺‘𝑌)))
Theorem	lflmul 39187	Property of a linear functional. (lnfnmuli 32026 analog.) (Contributed by NM, 16-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ × = (.r‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (𝐺‘(𝑅 · 𝑋)) = (𝑅 × (𝐺‘𝑋)))
Theorem	lfl0f 39188	The zero function is a functional. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑉 × { 0 }) ∈ 𝐹)
Theorem	lfl1 39189*	A nonzero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 1 = (1r‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × { 0 })) → ∃𝑥 ∈ 𝑉 (𝐺‘𝑥) = 1 )
Theorem	lfladdcl 39190	Closure of addition of two functionals. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f + 𝐻) ∈ 𝐹)
Theorem	lfladdcom 39191	Commutativity of functional addition. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f + 𝐻) = (𝐻 ∘f + 𝐺))
Theorem	lfladdass 39192	Associativity of functional addition. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐺 ∘f + 𝐻) ∘f + 𝐼) = (𝐺 ∘f + (𝐻 ∘f + 𝐼)))
Theorem	lfladd0l 39193	Functional addition with the zero functional. (Contributed by NM, 21-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑉 × { 0 }) ∘f + 𝐺) = 𝐺)
Theorem	lflnegcl 39194*	Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp 39265, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ 𝑁 = (𝑥 ∈ 𝑉 ↦ (𝐼‘(𝐺‘𝑥)))    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝐹)
Theorem	lflnegl 39195*	A functional plus its negative is the zero functional. (This is specialized for the purpose of proving ldualgrp 39265, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ 𝑁 = (𝑥 ∈ 𝑉 ↦ (𝐼‘(𝐺‘𝑥)))    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝜑 → (𝑁 ∘f + 𝐺) = (𝑉 × { 0 }))
Theorem	lflvscl 39196	Closure of a scalar product with a functional. Note that this is the scalar product for a right vector space with the scalar after the vector; reversing these fails closure. (Contributed by NM, 9-Oct-2014.) (Revised by Mario Carneiro, 22-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · (𝑉 × {𝑅})) ∈ 𝐹)
Theorem	lflvsdi1 39197	Distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐺 ∘f + 𝐻) ∘f · (𝑉 × {𝑋})) = ((𝐺 ∘f · (𝑉 × {𝑋})) ∘f + (𝐻 ∘f · (𝑉 × {𝑋}))))
Theorem	lflvsdi2 39198	Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · ((𝑉 × {𝑋}) ∘f + (𝑉 × {𝑌}))) = ((𝐺 ∘f · (𝑉 × {𝑋})) ∘f + (𝐺 ∘f · (𝑉 × {𝑌}))))
Theorem	lflvsdi2a 39199	Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 21-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · (𝑉 × {(𝑋 + 𝑌)})) = ((𝐺 ∘f · (𝑉 × {𝑋})) ∘f + (𝐺 ∘f · (𝑉 × {𝑌}))))
Theorem	lflvsass 39200	Associative law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · (𝑉 × {(𝑋 · 𝑌)})) = ((𝐺 ∘f · (𝑉 × {𝑋})) ∘f · (𝑉 × {𝑌})))