P. 403 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40201-40300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lflmul 40201	Property of a linear functional. (lnfnmuli 32647 analog.) (Contributed by NM, 16-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ × = (.r‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (𝐺‘(𝑅 · 𝑋)) = (𝑅 × (𝐺‘𝑋)))
Theorem	lfl0f 40202	The zero function is a functional. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑉 × { 0 }) ∈ 𝐹)
Theorem	lfl1 40203*	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 40204	Closure of addition of two functionals. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f + 𝐻) ∈ 𝐹)
Theorem	lfladdcom 40205	Commutativity of functional addition. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f + 𝐻) = (𝐻 ∘f + 𝐺))
Theorem	lfladdass 40206	Associativity of functional addition. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐺 ∘f + 𝐻) ∘f + 𝐼) = (𝐺 ∘f + (𝐻 ∘f + 𝐼)))
Theorem	lfladd0l 40207	Functional addition with the zero functional. (Contributed by NM, 21-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑉 × { 0 }) ∘f + 𝐺) = 𝐺)
Theorem	lflnegcl 40208*	Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp 40279, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ 𝑁 = (𝑥 ∈ 𝑉 ↦ (𝐼‘(𝐺‘𝑥)))    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝐹)
Theorem	lflnegl 40209*	A functional plus its negative is the zero functional. (This is specialized for the purpose of proving ldualgrp 40279, 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 40210	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 40211	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 40212	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 40213	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 40214	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 · (𝑉 × {𝑌})))
Theorem	lfl0sc 40215	The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of (𝑉 × { 0 }) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · (𝑉 × { 0 })) = (𝑉 × { 0 }))
Theorem	lflsc0N 40216	The scalar product with the zero functional is the zero functional. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑉 × { 0 }) ∘f · (𝑉 × {𝑋})) = (𝑉 × { 0 }))
Theorem	lfl1sc 40217	The (right vector space) scalar product of a functional with one is the functional. (Contributed by NM, 21-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 1 = (1r‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · (𝑉 × { 1 })) = 𝐺)
Syntax	clk 40218	Extend class notation with the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space.
class LKer
Definition	df-lkr 40219*	Define the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. (Contributed by NM, 15-Apr-2014.)
⊢ LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))})))
Theorem	lkrfval 40220*	The kernel of a functional. (Contributed by NM, 15-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝐾 = (𝑓 ∈ 𝐹 ↦ (◡𝑓 “ { 0 })))
Theorem	lkrval 40221	Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = (◡𝐺 “ { 0 }))
Theorem	ellkr 40222	Membership in the kernel of a functional. (elnlfn 32531 analog.) (Contributed by NM, 16-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹) → (𝑋 ∈ (𝐾‘𝐺) ↔ (𝑋 ∈ 𝑉 ∧ (𝐺‘𝑋) = 0 )))
Theorem	lkrval2 40223*	Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = {𝑥 ∈ 𝑉 ∣ (𝐺‘𝑥) = 0 })
Theorem	ellkr2 40224	Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐾‘𝐺) ↔ (𝐺‘𝑋) = 0 ))
Theorem	lkrcl 40225	A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ (𝐾‘𝐺)) → 𝑋 ∈ 𝑉)
Theorem	lkrf0 40226	The value of a functional at a member of its kernel is zero. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ (𝐾‘𝐺)) → (𝐺‘𝑋) = 0 )
Theorem	lkr0f 40227	The kernel of the zero functional is the set of all vectors. (Contributed by NM, 17-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐾‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × { 0 })))
Theorem	lkrlss 40228	The kernel of a linear functional is a subspace. (nlelshi 32663 analog.) (Contributed by NM, 16-Apr-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ∈ 𝑆)
Theorem	lkrssv 40229	The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐾‘𝐺) ⊆ 𝑉)
Theorem	lkrsc 40230	The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 9-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑅 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐿‘(𝐺 ∘f · (𝑉 × {𝑅}))) = (𝐿‘𝐺))
Theorem	lkrscss 40231	The kernel of a scalar product of a functional includes the kernel of the functional. (The inclusion is proper for the zero product and equality otherwise.) (Contributed by NM, 9-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝐺 ∘f · (𝑉 × {𝑅}))))
Theorem	eqlkr 40232*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 18-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
Theorem	eqlkr2 40233*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 10-Oct-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 𝐻 = (𝐺 ∘f · (𝑉 × {𝑟})))
Theorem	eqlkr3 40234	Two functionals with the same kernel are equal if they are equal at any nonzero value. (Contributed by NM, 2-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻))    &   ⊢ (𝜑 → (𝐺‘𝑋) = (𝐻‘𝑋))    &   ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 )    ⇒   ⊢ (𝜑 → 𝐺 = 𝐻)
Theorem	lkrlsp 40235	The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr 40222) is the whole vector space. (Contributed by NM, 19-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ (𝐺‘𝑋) ≠ 0 ) → ((𝐾‘𝐺) ⊕ (𝑁‘{𝑋})) = 𝑉)
Theorem	lkrlsp2 40236	The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 12-May-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ ¬ 𝑋 ∈ (𝐾‘𝐺)) → ((𝐾‘𝐺) ⊕ (𝑁‘{𝑋})) = 𝑉)
Theorem	lkrlsp3 40237	The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 29-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ ¬ 𝑋 ∈ (𝐾‘𝐺)) → (𝑁‘((𝐾‘𝐺) ∪ {𝑋})) = 𝑉)
Theorem	lkrshp 40238	The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × { 0 })) → (𝐾‘𝐺) ∈ 𝐻)
Theorem	lkrshp3 40239	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ (𝑉 × { 0 })))
Theorem	lkrshpor 40240	The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ∨ (𝐾‘𝐺) = 𝑉))
Theorem	lkrshp4 40241	A kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ≠ 𝑉 ↔ (𝐾‘𝐺) ∈ 𝐻))
Theorem	lshpsmreu 40242*	Lemma for lshpkrex 40251. Show uniqueness of ring multiplier 𝑘 when a vector 𝑋 is broken down into components, one in a hyperplane and the other outside of it . TODO: do we need the cbvrexv 3350 for 𝑎 to 𝑐? (Contributed by NM, 4-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ (𝜑 → ∃!𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍)))
Theorem	lshpkrlem1 40243*	Lemma for lshpkrex 40251. The value of tentative functional 𝐺 is zero iff its argument belongs to hyperplane 𝑈. (Contributed by NM, 14-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝐺‘𝑋) = 0 ))
Theorem	lshpkrlem2 40244*	Lemma for lshpkrex 40251. The value of tentative functional 𝐺 is a scalar. (Contributed by NM, 16-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐾)
Theorem	lshpkrlem3 40245*	Lemma for lshpkrex 40251. Defining property of 𝐺‘𝑋. (Contributed by NM, 15-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑈 𝑋 = (𝑧 + ((𝐺‘𝑋) · 𝑍)))
Theorem	lshpkrlem4 40246*	Lemma for lshpkrex 40251. Part of showing linearity of 𝐺. (Contributed by NM, 16-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑉 ∧ 𝑠 ∈ 𝑉) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) = (((𝑙 · 𝑟) + 𝑠) + (((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣)) · 𝑍)))
Theorem	lshpkrlem5 40247*	Lemma for lshpkrex 40251. Part of showing linearity of 𝐺. (Contributed by NM, 16-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣)))
Theorem	lshpkrlem6 40248*	Lemma for lshpkrex 40251. Show linearlity of 𝐺. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ ((𝜑 ∧ (𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉)) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣)))
Theorem	lshpkrcl 40249*	The set 𝐺 defined by hyperplane 𝑈 is a linear functional. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐹)
Theorem	lshpkr 40250*	The kernel of functional 𝐺 is the hyperplane defining it. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    &   ⊢ 𝐿 = (LKer‘𝑊)    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) = 𝑈)
Theorem	lshpkrex 40251*	There exists a functional whose kernel equals a given hyperplane. Part of Th. 1.27 of Barbu and Precupanu, Convexity and Optimization in Banach Spaces. (Contributed by NM, 17-Jul-2014.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻) → ∃𝑔 ∈ 𝐹 (𝐾‘𝑔) = 𝑈)
Theorem	lshpset2N 40252*	The set of all hyperplanes of a left module or left vector space equals the set of all kernels of nonzero functionals. (Contributed by NM, 17-Jul-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐻 = {𝑠 ∣ ∃𝑔 ∈ 𝐹 (𝑔 ≠ (𝑉 × { 0 }) ∧ 𝑠 = (𝐾‘𝑔))})
Theorem	islshpkrN 40253*	The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be 𝑈 = (𝐾‘𝑔) or (𝐾‘𝑔) = 𝑈 as in lshpkrex 40251? Both standards seem to be used randomly throughout set.mm; we should decide on a preferred one. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝑈 ∈ 𝐻 ↔ ∃𝑔 ∈ 𝐹 (𝑔 ≠ (𝑉 × { 0 }) ∧ 𝑈 = (𝐾‘𝑔))))
Theorem	lfl1dim 40254*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘f · (𝑉 × {𝑘}))})
Theorem	lfl1dim2N 40255*	Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 40254 may be more compatible with lspsn 21278. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∈ 𝐹 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘f · (𝑉 × {𝑘}))})
21.30.8  Opposite rings and dual vector spaces
Syntax	cld 40256	Extend class notation with left dualvector space.
class LDual
Definition	df-ldual 40257*	Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in [Holland95] p. 218. This allows to reuse our existing collection of left vector space theorems. The restriction on ∘f (+g‘𝑣) allows it to be a set; see ofmres 7996. Note the operation reversal in the scalar product to allow to use the original scalar ring instead of the oppr ring, for convenience. (Contributed by NM, 18-Oct-2014.)
⊢ LDual = (𝑣 ∈ V ↦ ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}))
Theorem	ldualset 40258*	Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in [Holland95] p. 218. This allows to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow to use the original scalar ring instead of the oppr ring, for convenience. (Contributed by NM, 18-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ + = ( ∘f + ↾ (𝐹 × 𝐹))    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘})))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))
Theorem	ldualvbase 40259	The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑉 = 𝐹)
Theorem	ldualelvbase 40260	Utility theorem for converting a functional to a vector of the dual space in order to use standard vector theorems. (Contributed by NM, 6-Jan-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝑉)
Theorem	ldualfvadd 40261	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ ⨣ = ( ∘f + ↾ (𝐹 × 𝐹))    ⇒   ⊢ (𝜑 → + = ⨣ )
Theorem	ldualvadd 40262	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 + 𝐻) = (𝐺 ∘f + 𝐻))
Theorem	ldualvaddcl 40263	The value of vector addition in the dual of a vector space is a functional. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 + 𝐻) ∈ 𝐹)
Theorem	ldualvaddval 40264	The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐺 + 𝐻)‘𝑋) = ((𝐺‘𝑋) + (𝐻‘𝑋)))
Theorem	ldualsca 40265	The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝑂 = (oppr‘𝐹)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑅 = 𝑂)
Theorem	ldualsbase 40266	Base set of scalar ring for the dual of a vector space. (Contributed by NM, 24-Oct-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐿 = (Base‘𝐹)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝐷)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐾 = 𝐿)
Theorem	ldualsaddN 40267	Scalar addition for the dual of a vector space. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝐹)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝐷)    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    ⇒   ⊢ (𝜑 → + = + )
Theorem	ldualsmul 40268	Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = (.r‘𝐹)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝐷)    &   ⊢ ∙ = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝑋 ∙ 𝑌) = (𝑌 · 𝑋))
Theorem	ldualfvs 40269*	Scalar product operation for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑌)    &   ⊢ · = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f × (𝑉 × {𝑘})))    ⇒   ⊢ (𝜑 → ∙ = · )
Theorem	ldualvs 40270	Scalar product operation value (which is a functional) for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 ∙ 𝐺) = (𝐺 ∘f × (𝑉 × {𝑋})))
Theorem	ldualvsval 40271	Value of scalar product operation value for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑋 ∙ 𝐺)‘𝐴) = ((𝐺‘𝐴) × 𝑋))
Theorem	ldualvscl 40272	The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐹)
Theorem	ldualvaddcom 40273	Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	ldualvsass 40274	Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑌 × 𝑋) · 𝐺) = (𝑋 · (𝑌 · 𝐺)))
Theorem	ldualvsass2 40275	Associative law for scalar product operation, using operations from the dual space. (Contributed by NM, 20-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑄 = (Scalar‘𝐷)    &   ⊢ × = (.r‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑋 × 𝑌) · 𝐺) = (𝑋 · (𝑌 · 𝐺)))
Theorem	ldualvsdi1 40276	Distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 · (𝐺 + 𝐻)) = ((𝑋 · 𝐺) + (𝑋 · 𝐻)))
Theorem	ldualvsdi2 40277	Reverse distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) · 𝐺) = ((𝑋 · 𝐺) + (𝑌 · 𝐺)))
Theorem	ldualgrplem 40278	Lemma for ldualgrp 40279. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = ∘f (+g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ Grp)
Theorem	ldualgrp 40279	The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐷 ∈ Grp)
Theorem	ldual0 40280	The zero scalar of the dual of a vector space. (Contributed by NM, 28-Dec-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐷)    &   ⊢ 𝑂 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑂 = 0 )
Theorem	ldual1 40281	The unit scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐷)    &   ⊢ 𝐼 = (1r‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐼 = 1 )
Theorem	ldualneg 40282	The negative of a scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑀 = (invg‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐷)    &   ⊢ 𝑁 = (invg‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑁 = 𝑀)
Theorem	ldual0v 40283	The zero vector of the dual of a vector space. (Contributed by NM, 24-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑂 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑂 = (𝑉 × { 0 }))
Theorem	ldual0vcl 40284	The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 0 ∈ 𝐹)
Theorem	lduallmodlem 40285	Lemma for lduallmod 40286. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = ∘f (+g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LMod)
Theorem	lduallmod 40286	The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LMod)
Theorem	lduallvec 40287	The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 20568; otherwise, the dual would be a right vector space as is sometimes the case in the literature. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LVec)
Theorem	ldualvsub 40288	The value of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 − 𝐻) = (𝐺 + ((𝑁‘ 1 ) · 𝐻)))
Theorem	ldualvsubcl 40289	Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 − 𝐻) ∈ 𝐹)
Theorem	ldualvsubval 40290	The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 40288? (Requires 𝐷 to oppr conversion.) (Contributed by NM, 26-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑆 = (-g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋)))
Theorem	ldualssvscl 40291	Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑈)
Theorem	ldualssvsubcl 40292	Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑈)
Theorem	ldual0vs 40293	Scalar zero times a functional is the zero functional. (Contributed by NM, 17-Feb-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝑂 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ( 0 · 𝐺) = 𝑂)
Theorem	lkr0f2 40294	The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) = 𝑉 ↔ 𝐺 = 0 ))
Theorem	lduallkr3 40295	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ 0 ))
Theorem	lkrpssN 40296	Proper subset relation between kernels. (Contributed by NM, 16-Feb-2015.) (New usage is discouraged.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ⊊ (𝐾‘𝐻) ↔ (𝐺 ≠ 0 ∧ 𝐻 = 0 )))
Theorem	lkrin 40297	Intersection of the kernels of 2 functionals is included in the kernel of their sum. (Contributed by NM, 7-Jan-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∩ (𝐾‘𝐻)) ⊆ (𝐾‘(𝐺 + 𝐻)))
Theorem	eqlkr4 40298*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 4-Feb-2015.)
⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝑅 𝐻 = (𝑟 · 𝐺))
Theorem	ldual1dim 40299*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑁‘{𝐺}) = {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)})
Theorem	ldualkrsc 40300	The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 28-Dec-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐿‘(𝑋 · 𝐺)) = (𝐿‘𝐺))