P. 350 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34901-35000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lsat0cv 34901	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 ` W )   &    |- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   =>    |- ( ph -> ( U e. A <-> { .0. } C U ) )
Theorem	lcvexchlem1 34902	Lemma for lcvexch 34907. (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   =>    |- ( ph -> ( T C. ( T .(+) U ) <-> ( T i^i U ) C. U ) )
Theorem	lcvexchlem2 34903	Lemma for lcvexch 34907. (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> R e. S )   &    |- ( ph -> ( T i^i U ) C_ R )   &    |- ( ph -> R C_ U )   =>    |- ( ph -> ( ( R .(+) T ) i^i U ) = R )
Theorem	lcvexchlem3 34904	Lemma for lcvexch 34907. (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> R e. S )   &    |- ( ph -> T C_ R )   &    |- ( ph -> R C_ ( T .(+) U ) )   =>    |- ( ph -> ( ( R i^i U ) .(+) T ) = R )
Theorem	lcvexchlem4 34905	Lemma for lcvexch 34907. (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> T C ( T .(+) U ) )   =>    |- ( ph -> ( T i^i U ) C U )
Theorem	lcvexchlem5 34906	Lemma for lcvexch 34907. (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> ( T i^i U ) C U )   =>    |- ( ph -> T C ( T .(+) U ) )
Theorem	lcvexch 34907	Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 27415 analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   =>    |- ( ph -> ( ( T i^i U ) C U <-> T C ( T .(+) U ) ) )
Theorem	lcvp 34908	Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 27421 analog.) (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( ( U i^i Q ) = { .0. } <-> U C ( U .(+) Q ) ) )
Theorem	lcv1 34909	Covering property of a subspace plus an atom. (chcv1 27401 analog.) (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( -. Q C_ U <-> U C ( U .(+) Q ) ) )
Theorem	lcv2 34910	Covering property of a subspace plus an atom. (chcv2 27402 analog.) (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( U C. ( U .(+) Q ) <-> U C ( U .(+) Q ) ) )
Theorem	lsatexch 34911	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 27427 analog.) (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   &    |- ( ph -> Q C_ ( U .(+) R ) )   &    |- ( ph -> ( U i^i Q ) = { .0. } )   =>    |- ( ph -> R C_ ( U .(+) Q ) )
Theorem	lsatnle 34912	The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 27422 analog.) (Contributed by NM, 10-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( -. Q C_ U <-> ( U i^i Q ) = { .0. } ) )
Theorem	lsatnem0 34913	The meet of distinct atoms is the zero subspace. (atnemeq0 27423 analog.) (Contributed by NM, 10-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   =>    |- ( ph -> ( Q =/= R <-> ( Q i^i R ) = { .0. } ) )
Theorem	lsatexch1 34914	The atom exch1ange property. (hlatexch1 35262 analog.) (Contributed by NM, 14-Jan-2015.)
|- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   &    |- ( ph -> S e. A )   &    |- ( ph -> Q C_ ( S .(+) R ) )   &    |- ( ph -> Q =/= S )   =>    |- ( ph -> R C_ ( S .(+) Q ) )
Theorem	lsatcv0eq 34915	If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 27425 analog.) (Contributed by NM, 10-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   =>    |- ( ph -> ( { .0. } C ( Q .(+) R ) <-> Q = R ) )
Theorem	lsatcv1 34916	Two atoms covering the zero subspace are equal. (atcv1 27426 analog.) (Contributed by NM, 10-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   &    |- ( ph -> U C ( Q .(+) R ) )   =>    |- ( ph -> ( U = { .0. } <-> Q = R ) )
Theorem	lsatcvatlem 34917	Lemma for lsatcvat 34918. (Contributed by NM, 10-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   &    |- ( ph -> U =/= { .0. } )   &    |- ( ph -> U C. ( Q .(+) R ) )   &    |- ( ph -> -. Q C_ U )   =>    |- ( ph -> U e. A )
Theorem	lsatcvat 34918	A nonzero subspace less than the sum of two atoms is an atom. (atcvati 27432 analog.) (Contributed by NM, 10-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   &    |- ( ph -> U =/= { .0. } )   &    |- ( ph -> U C. ( Q .(+) R ) )   =>    |- ( ph -> U e. A )
Theorem	lsatcvat2 34919	A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 27433 analog.) (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   &    |- ( ph -> Q =/= R )   &    |- ( ph -> U C ( Q .(+) R ) )   =>    |- ( ph -> U e. A )
Theorem	lsatcvat3 34920	A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 27442 analog.) (Contributed by NM, 11-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   &    |- ( ph -> Q =/= R )   &    |- ( ph -> -. R C_ U )   &    |- ( ph -> Q C_ ( U .(+) R ) )   =>    |- ( ph -> ( U i^i ( Q .(+) R ) ) e. A )
Theorem	islshpcv 34921	Hyperplane properties expressed with covers relation. (Contributed by NM, 11-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   =>    |- ( ph -> ( U e. H <-> ( U e. S /\ U C V ) ) )
Theorem	l1cvpat 34922	A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. (1cvrjat 35342 analog.) (Contributed by NM, 11-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   &    |- ( ph -> U C V )   &    |- ( ph -> -. Q C_ U )   =>    |- ( ph -> ( U .(+) Q ) = V )
Theorem	l1cvat 34923	Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (1cvrat 35343 analog.) (Contributed by NM, 11-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   &    |- ( ph -> Q =/= R )   &    |- ( ph -> U C V )   &    |- ( ph -> -. Q C_ U )   =>    |- ( ph -> ( ( Q .(+) R ) i^i U ) e. A )
Theorem	lshpat 34924	Create an atom under a hyperplane. Part of proof of Lemma B in [Crawley] p. 112. (lhpat 35910 analog.) TODO: This changes U C V in l1cvpat 34922 and l1cvat 34923 to U e. H, which in turn change U e. H in islshpcv 34921 to U C V, with a couple of conversions of span to atom. Seems convoluted. Would a direct proof be better? (Contributed by NM, 11-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Q e. A )   &    |- ( ph -> R e. A )   &    |- ( ph -> Q =/= R )   &    |- ( ph -> -. Q C_ U )   =>    |- ( ph -> ( ( Q .(+) R ) i^i U ) e. A )
21.30.4  Functionals and kernels of a left vector space (or module)
Syntax	clfn 34925	Extend class notation with all linear functionals of a left module or left vector space.
class LFnl
Definition	df-lfl 34926*	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 = ( w e. _V |-> { f e. ( ( Base ` (Scalar ` w ) ) ^m ( Base ` w ) ) | A. r e. ( Base ` (Scalar ` w ) ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) ) } )
Theorem	lflset 34927*	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.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- D = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` D )   &    |- .+^ = ( +g ` D )   &    |- .X. = ( .r ` D )   &    |- F = (LFnl ` W )   =>    |- ( W e. X -> F = { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } )
Theorem	islfl 34928*	The predicate "is a linear functional". (Contributed by NM, 15-Apr-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- D = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` D )   &    |- .+^ = ( +g ` D )   &    |- .X. = ( .r ` D )   &    |- F = (LFnl ` W )   =>    |- ( W e. X -> ( G e. F <-> ( G : V --> K /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) ) )
Theorem	lfli 34929	Property of a linear functional. (lnfnli 27086 analog.) (Contributed by NM, 16-Apr-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- D = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` D )   &    |- .+^ = ( +g ` D )   &    |- .X. = ( .r ` D )   &    |- F = (LFnl ` W )   =>    |- ( ( W e. Z /\ G e. F /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( G ` ( ( R .x. X ) .+ Y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) )
Theorem	islfld 34930*	Properties that determine a linear functional. TODO: use this in place of islfl 34928 when it shortens the proof. (Contributed by NM, 19-Oct-2014.)
|- ( ph -> V = ( Base ` W ) )   &    |- ( ph -> .+ = ( +g ` W ) )   &    |- ( ph -> D = (Scalar ` W ) )   &    |- ( ph -> .x. = ( .s ` W ) )   &    |- ( ph -> K = ( Base ` D ) )   &    |- ( ph -> .+^ = ( +g ` D ) )   &    |- ( ph -> .X. = ( .r ` D ) )   &    |- ( ph -> F = (LFnl ` W ) )   &    |- ( ph -> G : V --> K )   &    |- ( ( ph /\ ( r e. K /\ x e. V /\ y e. V ) ) -> ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> G e. F )
Theorem	lflf 34931	A linear functional is a function from vectors to scalars. (lnfnfi 27087 analog.) (Contributed by NM, 15-Apr-2014.)
|- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   =>    |- ( ( W e. X /\ G e. F ) -> G : V --> K )
Theorem	lflcl 34932	A linear functional value is a scalar. (Contributed by NM, 15-Apr-2014.)
|- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   =>    |- ( ( W e. Y /\ G e. F /\ X e. V ) -> ( G ` X ) e. K )
Theorem	lfl0 34933	A linear functional is zero at the zero vector. (lnfn0i 27088 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- Z = ( 0g ` W )   &    |- F = (LFnl ` W )   =>    |- ( ( W e. LMod /\ G e. F ) -> ( G ` Z ) = .0. )
Theorem	lfladd 34934	Property of a linear functional. (lnfnaddi 27089 analog.) (Contributed by NM, 18-Apr-2014.)
|- D = (Scalar ` W )   &    |- .+^ = ( +g ` D )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- F = (LFnl ` W )   =>    |- ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( X .+ Y ) ) = ( ( G ` X ) .+^ ( G ` Y ) ) )
Theorem	lflsub 34935	Property of a linear functional. (lnfnaddi 27089 analog.) (Contributed by NM, 18-Apr-2014.)
|- D = (Scalar ` W )   &    |- M = ( -g ` D )   &    |- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- F = (LFnl ` W )   =>    |- ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( X .- Y ) ) = ( ( G ` X ) M ( G ` Y ) ) )
Theorem	lflmul 34936	Property of a linear functional. (lnfnmuli 27090 analog.) (Contributed by NM, 16-Apr-2014.)
|- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .X. = ( .r ` D )   &    |- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- F = (LFnl ` W )   =>    |- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( R .x. X ) ) = ( R .X. ( G ` X ) ) )
Theorem	lfl0f 34937	The zero function is a functional. (Contributed by NM, 16-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   =>    |- ( W e. LMod -> ( V X. { .0. } ) e. F )
Theorem	lfl1 34938*	A non-zero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- .1. = ( 1r ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   =>    |- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> E. x e. V ( G ` x ) = .1. )
Theorem	lfladdcl 34939	Closure of addition of two functionals. (Contributed by NM, 19-Oct-2014.)
|- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( G oF .+ H ) e. F )
Theorem	lfladdcom 34940	Commutativity of functional addition. (Contributed by NM, 19-Oct-2014.)
|- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( G oF .+ H ) = ( H oF .+ G ) )
Theorem	lfladdass 34941	Associativity of functional addition. (Contributed by NM, 19-Oct-2014.)
|- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   &    |- ( ph -> I e. F )   =>    |- ( ph -> ( ( G oF .+ H ) oF .+ I ) = ( G oF .+ ( H oF .+ I ) ) )
Theorem	lfladd0l 34942	Functional addition with the zero functional. (Contributed by NM, 21-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- .0. = ( 0g ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( V X. { .0. } ) oF .+ G ) = G )
Theorem	lflnegcl 34943*	Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp 35014, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- I = ( invg ` R )   &    |- N = ( x e. V |-> ( I ` ( G ` x ) ) )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> N e. F )
Theorem	lflnegl 34944*	A functional plus its negative is the zero functional. (This is specialized for the purpose of proving ldualgrp 35014, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- I = ( invg ` R )   &    |- N = ( x e. V |-> ( I ` ( G ` x ) ) )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- .+ = ( +g ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ph -> ( N oF .+ G ) = ( V X. { .0. } ) )
Theorem	lflvscl 34945	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.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> R e. K )   =>    |- ( ph -> ( G oF .x. ( V X. { R } ) ) e. F )
Theorem	lflvsdi1 34946	Distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( ( G oF .+ H ) oF .x. ( V X. { X } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( H oF .x. ( V X. { X } ) ) ) )
Theorem	lflvsdi2 34947	Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( ( V X. { X } ) oF .+ ( V X. { Y } ) ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )
Theorem	lflvsdi2a 34948	Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 21-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( V X. { ( X .+ Y ) } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )
Theorem	lflvsass 34949	Associative law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( V X. { ( X .x. Y ) } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .x. ( V X. { Y } ) ) )
Theorem	lfl0sc 34950	The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of ( V X. { .0. } ) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- F = (LFnl ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( V X. { .0. } ) ) = ( V X. { .0. } ) )
Theorem	lflsc0N 34951	The scalar product with the zero functional is the zero functional. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   =>    |- ( ph -> ( ( V X. { .0. } ) oF .x. ( V X. { X } ) ) = ( V X. { .0. } ) )
Theorem	lfl1sc 34952	The (right vector space) scalar product of a functional with one is the functional. (Contributed by NM, 21-Oct-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- F = (LFnl ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- .1. = ( 1r ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( V X. { .1. } ) ) = G )
Syntax	clk 34953	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 34954*	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 = ( w e. _V |-> ( f e. (LFnl ` w ) |-> ( `' f " { ( 0g ` (Scalar ` w ) ) } ) ) )
Theorem	lkrfval 34955*	The kernel of a functional. (Contributed by NM, 15-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( W e. X -> K = ( f e. F |-> ( `' f " { .0. } ) ) )
Theorem	lkrval 34956	Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. X /\ G e. F ) -> ( K ` G ) = ( `' G " { .0. } ) )
Theorem	ellkr 34957	Membership in the kernel of a functional. (elnlfn 26974 analog.) (Contributed by NM, 16-Apr-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. Y /\ G e. F ) -> ( X e. ( K ` G ) <-> ( X e. V /\ ( G ` X ) = .0. ) ) )
Theorem	lkrval2 34958*	Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. X /\ G e. F ) -> ( K ` G ) = { x e. V | ( G ` x ) = .0. } )
Theorem	ellkr2 34959	Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. Y )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( X e. ( K ` G ) <-> ( G ` X ) = .0. ) )
Theorem	lkrcl 34960	A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014.)
|- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. Y /\ G e. F /\ X e. ( K ` G ) ) -> X e. V )
Theorem	lkrf0 34961	The value of a functional at a member of its kernel is zero. (Contributed by NM, 16-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. Y /\ G e. F /\ X e. ( K ` G ) ) -> ( G ` X ) = .0. )
Theorem	lkr0f 34962	The kernel of the zero functional is the set of all vectors. (Contributed by NM, 17-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V <-> G = ( V X. { .0. } ) ) )
Theorem	lkrlss 34963	The kernel of a linear functional is a subspace. (nlelshi 27106 analog.) (Contributed by NM, 16-Apr-2014.)
|- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ G e. F ) -> ( K ` G ) e. S )
Theorem	lkrssv 34964	The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015.)
|- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( K ` G ) C_ V )
Theorem	lkrsc 34965	The kernel of a non-zero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 9-Oct-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   &    |- ( ph -> R e. K )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> R =/= .0. )   =>    |- ( ph -> ( L ` ( G oF .x. ( V X. { R } ) ) ) = ( L ` G ) )
Theorem	lkrscss 34966	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.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   &    |- ( ph -> R e. K )   =>    |- ( ph -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { R } ) ) ) )
Theorem	eqlkr 34967*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 18-Apr-2014.)
|- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) )
Theorem	eqlkr2 34968*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 10-Oct-2014.)
|- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) -> E. r e. K H = ( G oF .x. ( V X. { r } ) ) )
Theorem	eqlkr3 34969	Two functionals with the same kernel are equal if they are equal at any nonzero value. (Contributed by NM, 2-Jan-2015.)
|- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` S )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   &    |- ( ph -> ( K ` G ) = ( K ` H ) )   &    |- ( ph -> ( G ` X ) = ( H ` X ) )   &    |- ( ph -> ( G ` X ) =/= .0. )   =>    |- ( ph -> G = H )
Theorem	lkrlsp 34970	The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr 34957) is the whole vector space. (Contributed by NM, 19-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )
Theorem	lkrlsp2 34971	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.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )
Theorem	lkrlsp3 34972	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.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( N ` ( ( K ` G ) u. { X } ) ) = V )
Theorem	lkrshp 34973	The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( K ` G ) e. H )
Theorem	lkrshp3 34974	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) e. H <-> G =/= ( V X. { .0. } ) ) )
Theorem	lkrshpor 34975	The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014.)
|- V = ( Base ` W )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) e. H \/ ( K ` G ) = V ) )
Theorem	lkrshp4 34976	A kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.)
|- V = ( Base ` W )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) =/= V <-> ( K ` G ) e. H ) )
Theorem	lshpsmreu 34977*	Lemma for lshpkrex 34986. Show uniqueness of ring multiplier k when a vector X is broken down into components, one in a hyperplane and the other outside of it . TODO: do we need the cbvrexv 3085 for a to c? (Contributed by NM, 4-Jan-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   =>    |- ( ph -> E! k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) )
Theorem	lshpkrlem1 34978*	Lemma for lshpkrex 34986. The value of tentative functional G is zero iff its argument belongs to hyperplane U. (Contributed by NM, 14-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ph -> ( X e. U <-> ( G ` X ) = .0. ) )
Theorem	lshpkrlem2 34979*	Lemma for lshpkrex 34986. The value of tentative functional G is a scalar. (Contributed by NM, 16-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ph -> ( G ` X ) e. K )
Theorem	lshpkrlem3 34980*	Lemma for lshpkrex 34986. Defining property of G ` X. (Contributed by NM, 15-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ph -> E. z e. U X = ( z .+ ( ( G ` X ) .x. Z ) ) )
Theorem	lshpkrlem4 34981*	Lemma for lshpkrex 34986. Part of showing linearity of G. (Contributed by NM, 16-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) ) ) -> ( ( l .x. u ) .+ v ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) )
Theorem	lshpkrlem5 34982*	Lemma for lshpkrex 34986. Part of showing linearity of G. (Contributed by NM, 16-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) )
Theorem	lshpkrlem6 34983*	Lemma for lshpkrex 34986. Show linearlity of G. (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) )
Theorem	lshpkrcl 34984*	The set G defined by hyperplane U is a linear functional. (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   &    |- F = (LFnl ` W )   =>    |- ( ph -> G e. F )
Theorem	lshpkr 34985*	The kernel of functional G is the hyperplane defining it. (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   &    |- L = (LKer ` W )   =>    |- ( ph -> ( L ` G ) = U )
Theorem	lshpkrex 34986*	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.)
|- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ U e. H ) -> E. g e. F ( K ` g ) = U )
Theorem	lshpset2N 34987*	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.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( W e. LVec -> H = { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } )
Theorem	islshpkrN 34988*	The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be U = ( K ` g ) or ( K ` g ) = U as in lshpkrex 34986? 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.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( W e. LVec -> ( U e. H <-> E. g e. F ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) ) )
Theorem	lfl1dim 34989*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } )
Theorem	lfl1dim2N 34990*	Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 34989 may be more compatible with lspsn 17775. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g e. F | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } )
21.30.5  Opposite rings and dual vector spaces
Syntax	cld 34991	Extend class notation with left dualvector space.
class LDual
Definition	df-ldual 34992*	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 us to reuse our existing collection of left vector space theorems. The restriction on oF ( +g ` v ) allows it to be a set; see ofmres 6795. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppr ring, for convenience. (Contributed by NM, 18-Oct-2014.)
|- LDual = ( v e. _V |-> ( { <. ( Base ` ndx ) , (LFnl ` v ) >. , <. ( +g ` ndx ) , ( oF ( +g ` (Scalar ` v ) ) |` ( (LFnl ` v ) X. (LFnl ` v ) ) ) >. , <. (Scalar ` ndx ) , (oppr ` (Scalar ` v ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` (Scalar ` v ) ) , f e. (LFnl ` v ) |-> ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) ) ) >. } ) )
Theorem	ldualset 34993*	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 us to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppr ring, for convenience. (Contributed by NM, 18-Oct-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` R )   &    |- .+b = ( oF .+ |` ( F X. F ) )   &    |- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .xb = ( k e. K , f e. F |-> ( f oF .x. ( V X. { k } ) ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. (Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )
Theorem	ldualvbase 34994	The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- V = ( Base ` D )   &    |- ( ph -> W e. X )   =>    |- ( ph -> V = F )
Theorem	ldualelvbase 34995	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.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- V = ( Base ` D )   &    |- ( ph -> W e. X )   &    |- ( ph -> G e. F )   =>    |- ( ph -> G e. V )
Theorem	ldualfvadd 34996	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- D = (LDual ` W )   &    |- .+b = ( +g ` D )   &    |- ( ph -> W e. X )   &    |- .+^ = ( oF .+ |` ( F X. F ) )   =>    |- ( ph -> .+b = .+^ )
Theorem	ldualvadd 34997	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- D = (LDual ` W )   &    |- .+b = ( +g ` D )   &    |- ( ph -> W e. X )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( G .+b H ) = ( G oF .+ H ) )
Theorem	ldualvaddcl 34998	The value of vector addition in the dual of a vector space is a functional. (Contributed by NM, 21-Oct-2014.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .+ = ( +g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( G .+ H ) e. F )
Theorem	ldualvaddval 34999	The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .+b = ( +g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( G .+b H ) ` X ) = ( ( G ` X ) .+ ( H ` X ) ) )
Theorem	ldualsca 35000	The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
|- F = (Scalar ` W )   &    |- O = (oppr ` F )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` D )   &    |- ( ph -> W e. X )   =>    |- ( ph -> R = O )