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	dedths2 32601	Generalization of dedths 32598 that is not useful unless we can separately prove |- A e. _V. (Contributed by NM, 13-Jun-2019.)
|- [. if ( [. A / x ]. ph , A , B ) / x ]. ps   =>    |- ( [. A / x ]. ph -> [. A / x ]. ps )
Theorem	19.9alt 32602	Version of 19.9t 1989 for universal quantifier. (Contributed by NM, 9-Nov-2020.)
|- ( F/ x ph -> ( A. x ph <-> ph ) )
Theorem	nfcxfrdf 32603	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.)
|- F/ x ph   &    |- ( ph -> A = B )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x A )
Theorem	nfded 32604	A deduction theorem that converts a not-free inference directly to deduction form. The first hypothesis is the hypothesis of the deduction form. The second is an equality deduction (e.g. ( F/_ x A -> U. { y | A. x y e. A } = U. A )) that starts from abidnf 3195. The last is assigned to the inference form (e.g. F/_ x U. { y | A. x y e. A }) whose hypothesis is satisfied using nfaba1 2617. (Contributed by NM, 19-Nov-2020.)
|- ( ph -> F/_ x A )   &    |- ( F/_ x A -> B = C )   &    |- F/_ x B   =>    |- ( ph -> F/_ x C )
Theorem	nfded2 32605	A deduction theorem that converts a not-free inference directly to deduction form. The first 2 hypotheses are the hypotheses of the deduction form. The third is an equality deduction (e.g. ( ( F/_ x A /\ F/_ x B ) -> <. { y | A. x y e. A } , { y | A. x y e. B } >. = <. A , B >. ) for nfopd 4175) that starts from abidnf 3195. The last is assigned to the inference form (e.g. F/_ x <. { y | A. x y e. A } , { y | A. x y e. B } >. for nfop 4174) whose hypotheses are satisfied using nfaba1 2617. (Contributed by NM, 19-Nov-2020.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   &    |- ( ( F/_ x A /\ F/_ x B ) -> C = D )   &    |- F/_ x C   =>    |- ( ph -> F/_ x D )
Theorem	nfunidALT2 32606	Deduction version of nfuni 4196. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x U. A )
Theorem	nfunidALT 32607	Deduction version of nfuni 4196. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x U. A )
Theorem	nfopdALT 32608	Deduction version of bound-variable hypothesis builder nfop 4174. This shows how the deduction version of a not-free theorem such as nfop 4174 can be created from the corresponding not-free inference theorem. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x <. A , B >. )
21.21.5  Miscellanea
Theorem	cnaddcom 32609	Recover the commutative law of addition for complex numbers from the Abelian group structure. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Theorem	toycom 32610*	Show the commutative law for an operation O on a toy structure class C of commuatitive operations on CC. This illustrates how a structure class can be partially specialized. In practice, we would ordinarily define a new constant such as "CAbel" in place of C. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.)
|- C = { g e. Abel | ( Base ` g ) = CC }   &    |- .+ = ( +g ` K )   =>    |- ( ( K e. C /\ A e. CC /\ B e. CC ) -> ( A .+ B ) = ( B .+ A ) )
21.21.6  Atoms, hyperplanes, and covering in a left vector space (or module)
Syntax	clsa 32611	Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space.
class LSAtoms
Syntax	clsh 32612	Extend class notation with all subspaces of a left module or left vector space that are hyperplanes.
class LSHyp
Definition	df-lsatoms 32613*	Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.)
|- LSAtoms = ( w e. _V |-> ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) ) )
Definition	df-lshyp 32614*	Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less that the full space. (Contributed by NM, 29-Jun-2014.)
|- LSHyp = ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } )
Theorem	lshpset 32615*	The set of all hyperplanes of a left module or left vector space. The vector v is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   =>    |- ( W e. X -> H = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
Theorem	islshp 32616*	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 32617*	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 32618	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 32619	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 32620	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 32621	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 32622	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 32623	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 32624	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 32625	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 32626	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 32627*	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 32628*	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 32629	The span of a non-zero singleton is an atom. TODO: make this obsolete and use lsatlspsn 32630 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 32630	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 32631*	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 32632*	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 32633	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 32634	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 32635	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 32636	A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 28079 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 32637	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 32638	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 32639	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 32640	If two atoms are comparable, they are equal. (atsseq 28081 analog.) TODO: can lspsncmp 18417 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 32641	If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 32640. TODO: can lspsncmp 18417 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 32642	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 32643	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 32644	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 32645*	Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 33441 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 32646*	Show equality with the span of the sum of two vectors, one of which ( X) is fixed in advance. Compare lspfixed 18429. (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 32647	Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 27386 analog.) Explicit atom version of lsmcv 18442. (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 32648*	The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 28092 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 32649*	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 28095 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 32650*	Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 28097 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 32651*	Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 28098 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 32652*	The ordering of two subspaces is determined by the atoms under them. (chrelat3 28105 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 32653*	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 28097 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 32654*	Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 32617. (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 32655	Extend class notation with the covering relation for a left module or left vector space.
class <oLL
Definition	df-lcv 32656*	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 32658 for binary relation. (df-cv 28013 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 32657*	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 32658*	The covers relation for a left vector space (or a left module). (cvbr 28016 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 32659*	The covers relation for a left vector space (or a left module). (cvbr2 28017 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 32660*	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 32661	The covers relation implies proper subset. (cvpss 28019 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 32662	The covers relation implies no in-betweenness. (cvnbtwn 28020 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 32663	The covers relation is not transitive. (cvntr 28026 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 32664	The covers relation implies no in-betweenness. (cvnbtwn2 28021 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 32665	The covers relation implies no in-betweenness. (cvnbtwn3 28022 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 32666	Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 28027 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 32667*	If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 28100 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 32668	An atom covers the zero subspace. (atcv0 28076 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 32669	A subspace covered by an atom must be the zero subspace. (atcveq0 28082 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 32670	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 32671	Lemma for lcvexch 32676. (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 32672	Lemma for lcvexch 32676. (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 32673	Lemma for lcvexch 32676. (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 32674	Lemma for lcvexch 32676. (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 32675	Lemma for lcvexch 32676. (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 32676	Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 28103 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 32677	Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 28109 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 32678	Covering property of a subspace plus an atom. (chcv1 28089 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 32679	Covering property of a subspace plus an atom. (chcv2 28090 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 32680	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 28115 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 32681	The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 28110 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 32682	The meet of distinct atoms is the zero subspace. (atnemeq0 28111 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 32683	The atom exch1ange property. (hlatexch1 33031 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 32684	If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 28113 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 32685	Two atoms covering the zero subspace are equal. (atcv1 28114 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 32686	Lemma for lsatcvat 32687. (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 32687	A nonzero subspace less than the sum of two atoms is an atom. (atcvati 28120 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 32688	A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 28121 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 32689	A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 28130 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 32690	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 32691	A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. (1cvrjat 33111 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 32692	Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (1cvrat 33112 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 32693	Create an atom under a hyperplane. Part of proof of Lemma B in [Crawley] p. 112. (lhpat 33679 analog.) TODO: This changes U C V in l1cvpat 32691 and l1cvat 32692 to U e. H, which in turn change U e. H in islshpcv 32690 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 32694	Extend class notation with all linear functionals of a left module or left vector space.
class LFnl
Definition	df-lfl 32695*	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 32696*	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 32697*	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 32698	Property of a linear functional. (lnfnli 27774 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 32699*	Properties that determine a linear functional. TODO: use this in place of islfl 32697 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 32700	A linear functional is a function from vectors to scalars. (lnfnfi 27775 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 )