P. 398 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39701-39800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lfl1 39701*	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 39702	Closure of addition of two functionals. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f + 𝐻) ∈ 𝐹)
Theorem	lfladdcom 39703	Commutativity of functional addition. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ∘f + 𝐻) = (𝐻 ∘f + 𝐺))
Theorem	lfladdass 39704	Associativity of functional addition. (Contributed by NM, 19-Oct-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐺 ∘f + 𝐻) ∘f + 𝐼) = (𝐺 ∘f + (𝐻 ∘f + 𝐼)))
Theorem	lfladd0l 39705	Functional addition with the zero functional. (Contributed by NM, 21-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑉 × { 0 }) ∘f + 𝐺) = 𝐺)
Theorem	lflnegcl 39706*	Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp 39777, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ 𝑁 = (𝑥 ∈ 𝑉 ↦ (𝐼‘(𝐺‘𝑥)))    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝐹)
Theorem	lflnegl 39707*	A functional plus its negative is the zero functional. (This is specialized for the purpose of proving ldualgrp 39777, 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 39708	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 39709	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 39710	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 39711	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 39712	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 39713	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 39714	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 39715	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 39716	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 39717*	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 39718*	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 39719	Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = (◡𝐺 “ { 0 }))
Theorem	ellkr 39720	Membership in the kernel of a functional. (elnlfn 32185 analog.) (Contributed by NM, 16-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹) → (𝑋 ∈ (𝐾‘𝐺) ↔ (𝑋 ∈ 𝑉 ∧ (𝐺‘𝑋) = 0 )))
Theorem	lkrval2 39721*	Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = {𝑥 ∈ 𝑉 ∣ (𝐺‘𝑥) = 0 })
Theorem	ellkr2 39722	Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐾‘𝐺) ↔ (𝐺‘𝑋) = 0 ))
Theorem	lkrcl 39723	A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ (𝐾‘𝐺)) → 𝑋 ∈ 𝑉)
Theorem	lkrf0 39724	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 39725	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 39726	The kernel of a linear functional is a subspace. (nlelshi 32317 analog.) (Contributed by NM, 16-Apr-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ∈ 𝑆)
Theorem	lkrssv 39727	The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐾‘𝐺) ⊆ 𝑉)
Theorem	lkrsc 39728	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 39729	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 39730*	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 39731*	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 39732	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 39733	The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr 39720) is the whole vector space. (Contributed by NM, 19-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ (𝐺‘𝑋) ≠ 0 ) → ((𝐾‘𝐺) ⊕ (𝑁‘{𝑋})) = 𝑉)
Theorem	lkrlsp2 39734	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 39735	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 39736	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 39737	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ (𝑉 × { 0 })))
Theorem	lkrshpor 39738	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 39739	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 39740*	Lemma for lshpkrex 39749. 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 3355 for 𝑎 to 𝑐? (Contributed by NM, 4-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ (𝜑 → ∃!𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍)))
Theorem	lshpkrlem1 39741*	Lemma for lshpkrex 39749. 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 39742*	Lemma for lshpkrex 39749. 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 39743*	Lemma for lshpkrex 39749. Defining property of 𝐺‘𝑋. (Contributed by NM, 15-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑈 𝑋 = (𝑧 + ((𝐺‘𝑋) · 𝑍)))
Theorem	lshpkrlem4 39744*	Lemma for lshpkrex 39749. 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 39745*	Lemma for lshpkrex 39749. 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 39746*	Lemma for lshpkrex 39749. Show linearlity of 𝐺. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ ((𝜑 ∧ (𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉)) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣)))
Theorem	lshpkrcl 39747*	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 39748*	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 39749*	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 39750*	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 39751*	The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be 𝑈 = (𝐾‘𝑔) or (𝐾‘𝑔) = 𝑈 as in lshpkrex 39749? 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 39752*	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 39753*	Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 39752 may be more compatible with lspsn 21089. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∈ 𝐹 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘f · (𝑉 × {𝑘}))})
21.28.8  Opposite rings and dual vector spaces
Syntax	cld 39754	Extend class notation with left dualvector space.
class LDual
Definition	df-ldual 39755*	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 7969. 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 39756*	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 39757	The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑉 = 𝐹)
Theorem	ldualelvbase 39758	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 39759	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ✚ = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ ⨣ = ( ∘f + ↾ (𝐹 × 𝐹))    ⇒   ⊢ (𝜑 → ✚ = ⨣ )
Theorem	ldualvadd 39760	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ✚ = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ✚ 𝐻) = (𝐺 ∘f + 𝐻))
Theorem	ldualvaddcl 39761	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 39762	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 39763	The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝑂 = (oppr‘𝐹)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑅 = 𝑂)
Theorem	ldualsbase 39764	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 39765	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 39766	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 39767*	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 39768	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 39769	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 39770	The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐹)
Theorem	ldualvaddcom 39771	Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	ldualvsass 39772	Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑌 × 𝑋) · 𝐺) = (𝑋 · (𝑌 · 𝐺)))
Theorem	ldualvsass2 39773	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 39774	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 39775	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 39776	Lemma for ldualgrp 39777. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = ∘f (+g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ Grp)
Theorem	ldualgrp 39777	The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐷 ∈ Grp)
Theorem	ldual0 39778	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 39779	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 39780	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 39781	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 39782	The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 0 ∈ 𝐹)
Theorem	lduallmodlem 39783	Lemma for lduallmod 39784. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = ∘f (+g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LMod)
Theorem	lduallmod 39784	The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LMod)
Theorem	lduallvec 39785	The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 20407; 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 39786	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 39787	Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 − 𝐻) ∈ 𝐹)
Theorem	ldualvsubval 39788	The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 39786? (Requires 𝐷 to oppr conversion.) (Contributed by NM, 26-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑆 = (-g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋)))
Theorem	ldualssvscl 39789	Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑈)
Theorem	ldualssvsubcl 39790	Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑈)
Theorem	ldual0vs 39791	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 39792	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 39793	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ 0 ))
Theorem	lkrpssN 39794	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 39795	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 39796*	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 39797*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑁‘{𝐺}) = {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)})
Theorem	ldualkrsc 39798	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 )    ⇒   ⊢ (𝜑 → (𝐿‘(𝑋 · 𝐺)) = (𝐿‘𝐺))
Theorem	lkrss 39799	The kernel of a scalar product of a functional includes the kernel of the functional. (Contributed by NM, 27-Jan-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝑋 · 𝐺)))
Theorem	lkrss2N 39800*	Two functionals with kernels in a subset relationship. (Contributed by NM, 17-Feb-2015.) (New usage is discouraged.)
⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ⊆ (𝐾‘𝐻) ↔ ∃𝑟 ∈ 𝑅 𝐻 = (𝑟 · 𝐺)))