P. 327 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32601-32700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lcv1 32601	Covering property of a subspace plus an atom. (chcv1 28001 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 32602	Covering property of a subspace plus an atom. (chcv2 28002 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 32603	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 28027 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 32604	The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 28022 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 32605	The meet of distinct atoms is the zero subspace. (atnemeq0 28023 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 32606	The atom exch1ange property. (hlatexch1 32954 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 32607	If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 28025 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 32608	Two atoms covering the zero subspace are equal. (atcv1 28026 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 32609	Lemma for lsatcvat 32610. (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 32610	A nonzero subspace less than the sum of two atoms is an atom. (atcvati 28032 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 32611	A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 28033 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 32612	A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 28042 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 32613	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 32614	A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. (1cvrjat 33034 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 32615	Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (1cvrat 33035 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 32616	Create an atom under a hyperplane. Part of proof of Lemma B in [Crawley] p. 112. (lhpat 33602 analog.) TODO: This changes U C V in l1cvpat 32614 and l1cvat 32615 to U e. H, which in turn change U e. H in islshpcv 32613 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.21.7  Functionals and kernels of a left vector space (or module)
Syntax	clfn 32617	Extend class notation with all linear functionals of a left module or left vector space.
class LFnl
Definition	df-lfl 32618*	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 32619*	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 32620*	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 32621	Property of a linear functional. (lnfnli 27686 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 32622*	Properties that determine a linear functional. TODO: use this in place of islfl 32620 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 32623	A linear functional is a function from vectors to scalars. (lnfnfi 27687 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 32624	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 32625	A linear functional is zero at the zero vector. (lnfn0i 27688 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 32626	Property of a linear functional. (lnfnaddi 27689 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 32627	Property of a linear functional. (lnfnaddi 27689 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 32628	Property of a linear functional. (lnfnmuli 27690 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 32629	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 32630*	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 32631	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 32632	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 32633	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 32634	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 32635*	Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp 32706, 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 32636*	A functional plus its negative is the zero functional. (This is specialized for the purpose of proving ldualgrp 32706, 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 32637	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 32638	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 32639	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 32640	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 32641	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 32642	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 32643	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 32644	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 32645	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 32646*	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 32647*	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 32648	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 32649	Membership in the kernel of a functional. (elnlfn 27574 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 32650*	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 32651	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 32652	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 32653	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 32654	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 32655	The kernel of a linear functional is a subspace. (nlelshi 27706 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 32656	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 32657	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 32658	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 32659*	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 32660*	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 32661	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 32662	The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr 32649) 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 32663	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 32664	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 32665	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 32666	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 32667	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 32668	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 32669*	Lemma for lshpkrex 32678. 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 3019 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 32670*	Lemma for lshpkrex 32678. 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 32671*	Lemma for lshpkrex 32678. 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 32672*	Lemma for lshpkrex 32678. 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 32673*	Lemma for lshpkrex 32678. 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 32674*	Lemma for lshpkrex 32678. 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 32675*	Lemma for lshpkrex 32678. 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 32676*	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 32677*	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 32678*	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 32679*	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 32680*	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 32678? 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 32681*	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 32682*	Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 32681 may be more compatible with lspsn 18218. (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.21.8  Opposite rings and dual vector spaces
Syntax	cld 32683	Extend class notation with left dualvector space.
class LDual
Definition	df-ldual 32684*	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 6786. 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 32685*	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 32686	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 32687	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 32688	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 32689	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 32690	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 32691	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 32692	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 )
Theorem	ldualsbase 32693	Base set of scalar ring for the dual of a vector space. (Contributed by NM, 24-Oct-2014.)
|- F = (Scalar ` W )   &    |- L = ( Base ` F )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` D )   &    |- K = ( Base ` R )   &    |- ( ph -> W e. V )   =>    |- ( ph -> K = L )
Theorem	ldualsaddN 32694	Scalar addition for the dual of a vector space. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.)
|- F = (Scalar ` W )   &    |- .+ = ( +g ` F )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` D )   &    |- .+b = ( +g ` R )   &    |- ( ph -> W e. V )   =>    |- ( ph -> .+b = .+ )
Theorem	ldualsmul 32695	Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .r ` F )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` D )   &    |- .xb = ( .r ` R )   &    |- ( ph -> W e. V )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   =>    |- ( ph -> ( X .xb Y ) = ( Y .x. X ) )
Theorem	ldualfvs 32696*	Scalar product operation for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- D = (LDual ` W )   &    |- .xb = ( .s ` D )   &    |- ( ph -> W e. Y )   &    |- .x. = ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) )   =>    |- ( ph -> .xb = .x. )
Theorem	ldualvs 32697	Scalar product operation value (which is a functional) for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- D = (LDual ` W )   &    |- .xb = ( .s ` D )   &    |- ( ph -> W e. Y )   &    |- ( ph -> X e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( X .xb G ) = ( G oF .X. ( V X. { X } ) ) )
Theorem	ldualvsval 32698	Value of scalar product operation value for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- D = (LDual ` W )   &    |- .xb = ( .s ` D )   &    |- ( ph -> W e. Y )   &    |- ( ph -> X e. K )   &    |- ( ph -> G e. F )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( ( X .xb G ) ` A ) = ( ( G ` A ) .X. X ) )
Theorem	ldualvscl 32699	The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( X .x. G ) e. F )
Theorem	ldualvaddcom 32700	Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .+ = ( +g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. F )   &    |- ( ph -> Y e. F )   =>    |- ( ph -> ( X .+ Y ) = ( Y .+ X ) )