P. 352 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35101-35200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	islshp 35101*	The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   =>    |- ( W e. X -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
Theorem	islshpsm 35102*	Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) ) )
Theorem	lshplss 35103	A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.)
|- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   =>    |- ( ph -> U e. S )
Theorem	lshpne 35104	A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.)
|- V = ( Base ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   =>    |- ( ph -> U =/= V )
Theorem	lshpnel 35105	A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { X } ) ) = V )   =>    |- ( ph -> -. X e. U )
Theorem	lshpnelb 35106	The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( -. X e. U <-> ( U .(+) ( N ` { X } ) ) = V ) )
Theorem	lshpnel2N 35107	Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> U =/= V )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. U )   =>    |- ( ph -> ( U e. H <-> ( U .(+) ( N ` { X } ) ) = V ) )
Theorem	lshpne0 35108	The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- .0. = ( 0g ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { X } ) ) = V )   =>    |- ( ph -> X =/= .0. )
Theorem	lshpdisj 35109	A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { X } ) ) = V )   =>    |- ( ph -> ( U i^i ( N ` { X } ) ) = { .0. } )
Theorem	lshpcmp 35110	If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.)
|- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> T e. H )   &    |- ( ph -> U e. H )   =>    |- ( ph -> ( T C_ U <-> T = U ) )
Theorem	lshpinN 35111	The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.)
|- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> T e. H )   &    |- ( ph -> U e. H )   =>    |- ( ph -> ( ( T i^i U ) e. H <-> T = U ) )
Theorem	lsatset 35112*	The set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( W e. X -> A = ran ( v e. ( V \ { .0. } ) |-> ( N ` { v } ) ) )
Theorem	islsat 35113*	The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( W e. X -> ( U e. A <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) ) )
Theorem	lsatlspsn2 35114	The span of a non-zero singleton is an atom. TODO: make this obsolete and use lsatlspsn 35115 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) e. A )
Theorem	lsatlspsn 35115	The span of a non-zero singleton is an atom. (Contributed by NM, 16-Jan-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( N ` { X } ) e. A )
Theorem	islsati 35116*	A 1-dim subspace (atom) (of a left module or left vector space) equals the span of some vector. (Contributed by NM, 1-Oct-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( ( W e. X /\ U e. A ) -> E. v e. V U = ( N ` { v } ) )
Theorem	lsateln0 35117*	A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. A )   =>    |- ( ph -> E. v e. U v =/= .0. )
Theorem	lsatlss 35118	The set of 1-dim subspaces is a set of subspaces. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( W e. LMod -> A C_ S )
Theorem	lsatlssel 35119	An atom is a subspace. (Contributed by NM, 25-Aug-2014.)
|- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. A )   =>    |- ( ph -> U e. S )
Theorem	lsatssv 35120	An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.)
|- V = ( Base ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> Q C_ V )
Theorem	lsatn0 35121	A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 27462 analog.) (Contributed by NM, 25-Aug-2014.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. A )   =>    |- ( ph -> U =/= { .0. } )
Theorem	lsatspn0 35122	The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( N ` { X } ) e. A <-> X =/= .0. ) )
Theorem	lsator0sp 35123	The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( N ` { X } ) e. A \/ ( N ` { X } ) = { .0. } ) )
Theorem	lsatssn0 35124	A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> Q e. A )   &    |- ( ph -> Q C_ U )   =>    |- ( ph -> U =/= { .0. } )
Theorem	lsatcmp 35125	If two atoms are comparable, they are equal. (atsseq 27464 analog.) TODO: can lspsncmp 17957 shorten this? (Contributed by NM, 25-Aug-2014.)
|- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> T e. A )   &    |- ( ph -> U e. A )   =>    |- ( ph -> ( T C_ U <-> T = U ) )
Theorem	lsatcmp2 35126	If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 35125. TODO: can lspsncmp 17957 shorten this? (Contributed by NM, 3-Feb-2015.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> T e. A )   &    |- ( ph -> ( U e. A \/ U = { .0. } ) )   =>    |- ( ph -> ( T C_ U <-> T = U ) )
Theorem	lsatel 35127	A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.)
|- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. A )   &    |- ( ph -> X e. U )   &    |- ( ph -> X =/= .0. )   =>    |- ( ph -> U = ( N ` { X } ) )
Theorem	lsatelbN 35128	A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> U e. A )   =>    |- ( ph -> ( X e. U <-> U = ( N ` { X } ) ) )
Theorem	lsat2el 35129	Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> P e. A )   &    |- ( ph -> Q e. A )   &    |- ( ph -> X =/= .0. )   &    |- ( ph -> X e. P )   &    |- ( ph -> X e. Q )   =>    |- ( ph -> P = Q )
Theorem	lsmsat 35130*	Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 35926 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   &    |- ( ph -> T =/= { .0. } )   &    |- ( ph -> Q C_ ( T .(+) U ) )   =>    |- ( ph -> E. p e. A ( p C_ T /\ Q C_ ( p .(+) U ) ) )
Theorem	lsatfixedN 35131*	Show equality with the span of the sum of two vectors, one of which ( X) is fixed in advance. Compare lspfixed 17969. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> Q e. A )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Q =/= ( N ` { X } ) )   &    |- ( ph -> Q =/= ( N ` { Y } ) )   &    |- ( ph -> Q C_ ( N ` { X , Y } ) )   =>    |- ( ph -> E. z e. ( ( N ` { Y } ) \ { .0. } ) Q = ( N ` { ( X .+ z ) } ) )
Theorem	lsmsatcv 35132	Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 26768 analog.) Explicit atom version of lsmcv 17982. (Contributed by NM, 29-Oct-2014.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   =>    |- ( ( ph /\ T C. U /\ U C_ ( T .(+) Q ) ) -> U = ( T .(+) Q ) )
Theorem	lssatomic 35133*	The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 27475 analog.) (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> U =/= { .0. } )   =>    |- ( ph -> E. q e. A q C_ U )
Theorem	lssats 35134*	The lattice of subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. Hypothesis (shatomistici 27478 analog.) (Contributed by NM, 9-Apr-2014.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> U = ( N ` U. { x e. A | x C_ U } ) )
Theorem	lpssat 35135*	Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 27480 analog.) (Contributed by NM, 11-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> T C. U )   =>    |- ( ph -> E. q e. A ( q C_ U /\ -. q C_ T ) )
Theorem	lrelat 35136*	Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 27481 analog.) (Contributed by NM, 11-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> T C. U )   =>    |- ( ph -> E. q e. A ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) )
Theorem	lssatle 35137*	The ordering of two subspaces is determined by the atoms under them. (chrelat3 27488 analog.) (Contributed by NM, 29-Oct-2014.)
|- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   =>    |- ( ph -> ( T C_ U <-> A. p e. A ( p C_ T -> p C_ U ) ) )
Theorem	lssat 35138*	Two subspaces in a proper subset relationship imply the existence of a 1-dim subspace less than or equal to one but not the other. (chpssati 27480 analog.) (Contributed by NM, 9-Apr-2014.)
|- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   =>    |- ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ U C. V ) -> E. p e. A ( p C_ V /\ -. p C_ U ) )
Theorem	islshpat 35139*	Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 35102. (Contributed by NM, 11-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- A = (LSAtoms ` W )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. q e. A ( U .(+) q ) = V ) ) )
Syntax	clcv 35140	Extend class notation with the covering relation for a left module or left vector space.
class <oLL
Definition	df-lcv 35141*	Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of [PtakPulmannova] p. 68. Ptak/Pulmannova's notation A ( <oLL ` W ) B is read " B covers A " or " A is covered by B " , and it means that B is larger than A and there is nothing in between. See lcvbr 35143 for binary relation. (df-cv 27396 analog.) (Contributed by NM, 7-Jan-2015.)
|- <oLL = ( w e. _V |-> { <. t , u >. | ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) } )
Theorem	lcvfbr 35142*	The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. X )   =>    |- ( ph -> C = { <. t , u >. | ( ( t e. S /\ u e. S ) /\ ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } )
Theorem	lcvbr 35143*	The covers relation for a left vector space (or a left module). (cvbr 27399 analog.) (Contributed by NM, 9-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   =>    |- ( ph -> ( T C U <-> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) ) )
Theorem	lcvbr2 35144*	The covers relation for a left vector space (or a left module). (cvbr2 27400 analog.) (Contributed by NM, 9-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   =>    |- ( ph -> ( T C U <-> ( T C. U /\ A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) ) ) )
Theorem	lcvbr3 35145*	The covers relation for a left vector space (or a left module). (Contributed by NM, 9-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   =>    |- ( ph -> ( T C U <-> ( T C. U /\ A. s e. S ( ( T C_ s /\ s C_ U ) -> ( s = T \/ s = U ) ) ) ) )
Theorem	lcvpss 35146	The covers relation implies proper subset. (cvpss 27402 analog.) (Contributed by NM, 7-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> T C U )   =>    |- ( ph -> T C. U )
Theorem	lcvnbtwn 35147	The covers relation implies no in-betweenness. (cvnbtwn 27403 analog.) (Contributed by NM, 7-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> R e. S )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> R C T )   =>    |- ( ph -> -. ( R C. U /\ U C. T ) )
Theorem	lcvntr 35148	The covers relation is not transitive. (cvntr 27409 analog.) (Contributed by NM, 10-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> R e. S )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> R C T )   &    |- ( ph -> T C U )   =>    |- ( ph -> -. R C U )
Theorem	lcvnbtwn2 35149	The covers relation implies no in-betweenness. (cvnbtwn2 27404 analog.) (Contributed by NM, 7-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> R e. S )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> R C T )   &    |- ( ph -> R C. U )   &    |- ( ph -> U C_ T )   =>    |- ( ph -> U = T )
Theorem	lcvnbtwn3 35150	The covers relation implies no in-betweenness. (cvnbtwn3 27405 analog.) (Contributed by NM, 7-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> R e. S )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> R C T )   &    |- ( ph -> R C_ U )   &    |- ( ph -> U C. T )   =>    |- ( ph -> U = R )
Theorem	lsmcv2 35151	Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 27410 analog.) (Contributed by NM, 10-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. ( N ` { X } ) C_ U )   =>    |- ( ph -> U C ( U .(+) ( N ` { X } ) ) )
Theorem	lcvat 35152*	If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 27483 analog.) (Contributed by NM, 11-Jan-2015.)
|- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> T e. S )   &    |- ( ph -> U e. S )   &    |- ( ph -> T C U )   =>    |- ( ph -> E. q e. A ( T .(+) q ) = U )
Theorem	lsatcv0 35153	An atom covers the zero subspace. (atcv0 27459 analog.) (Contributed by NM, 7-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> { .0. } C Q )
Theorem	lsatcveq0 35154	A subspace covered by an atom must be the zero subspace. (atcveq0 27465 analog.) (Contributed by NM, 7-Jan-2015.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   &    |- A = (LSAtoms ` W )   &    |- C = ( <oLL ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( U C Q <-> U = { .0. } ) )
Theorem	lsat0cv 35155	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 35156	Lemma for lcvexch 35161. (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 35157	Lemma for lcvexch 35161. (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 35158	Lemma for lcvexch 35161. (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 35159	Lemma for lcvexch 35161. (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 35160	Lemma for lcvexch 35161. (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 35161	Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 27486 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 35162	Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 27492 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 35163	Covering property of a subspace plus an atom. (chcv1 27472 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 35164	Covering property of a subspace plus an atom. (chcv2 27473 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 35165	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 27498 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 35166	The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 27493 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 35167	The meet of distinct atoms is the zero subspace. (atnemeq0 27494 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 35168	The atom exch1ange property. (hlatexch1 35516 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 35169	If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 27496 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 35170	Two atoms covering the zero subspace are equal. (atcv1 27497 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 35171	Lemma for lsatcvat 35172. (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 35172	A nonzero subspace less than the sum of two atoms is an atom. (atcvati 27503 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 35173	A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 27504 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 35174	A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 27513 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 35175	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 35176	A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. (1cvrjat 35596 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 35177	Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (1cvrat 35597 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 35178	Create an atom under a hyperplane. Part of proof of Lemma B in [Crawley] p. 112. (lhpat 36164 analog.) TODO: This changes U C V in l1cvpat 35176 and l1cvat 35177 to U e. H, which in turn change U e. H in islshpcv 35175 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.29.4  Functionals and kernels of a left vector space (or module)
Syntax	clfn 35179	Extend class notation with all linear functionals of a left module or left vector space.
class LFnl
Definition	df-lfl 35180*	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 35181*	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 35182*	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 35183	Property of a linear functional. (lnfnli 27157 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 35184*	Properties that determine a linear functional. TODO: use this in place of islfl 35182 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 35185	A linear functional is a function from vectors to scalars. (lnfnfi 27158 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 35186	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 35187	A linear functional is zero at the zero vector. (lnfn0i 27159 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 35188	Property of a linear functional. (lnfnaddi 27160 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 35189	Property of a linear functional. (lnfnaddi 27160 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 35190	Property of a linear functional. (lnfnmuli 27161 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 35191	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 35192*	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 35193	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 35194	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 35195	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 35196	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 35197*	Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp 35268, 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 35198*	A functional plus its negative is the zero functional. (This is specialized for the purpose of proving ldualgrp 35268, 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 35199	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 35200	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 } ) ) ) )