P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	riotasv 32501*	Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4630). Special case of riota2f 6289. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
|- A e. _V   &    |- D = ( iota_ x e. A A. y e. B ( ph -> x = C ) )   =>    |- ( ( D e. A /\ y e. B /\ ph ) -> D = C )
Theorem	riotasv3d 32502*	A property ch holding for a representative of a single-valued class expression C ( y ) (see e.g. reusv2 4630) also holds for its description binder D (in the form of property th). (Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ y th )   &    |- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )   &    |- ( ( ph /\ C = D ) -> ( ch <-> th ) )   &    |- ( ph -> ( ( y e. B /\ ps ) -> ch ) )   &    |- ( ph -> D e. A )   &    |- ( ph -> E. y e. B ps )   =>    |- ( ( ph /\ A e. V ) -> th )
21.21.4  Experiments with weak deduction theorem
Theorem	elimhyps 32503	A version of elimhyp 3969 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
|- [. B / x ]. ph   =>    |- [. if ( ph , x , B ) / x ]. ph
Theorem	dedths 32504	A version of weak deduction theorem dedth 3962 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
|- [. if ( ph , x , B ) / x ]. ps   =>    |- ( ph -> ps )
Theorem	renegclALT 32505	Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 9945. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. RR -> -u A e. RR )
Theorem	elimhyps2 32506	Generalization of elimhyps 32503 that is not useful unless we can separately prove |- A e. _V. (Contributed by NM, 13-Jun-2019.)
|- [. B / x ]. ph   =>    |- [. if ( [. A / x ]. ph , A , B ) / x ]. ph
Theorem	dedths2 32507	Generalization of dedths 32504 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 )
21.21.5  Miscellanea
Theorem	cnaddcom 32508	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 32509*	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 32510	Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space.
class LSAtoms
Syntax	clsh 32511	Extend class notation with all subspaces of a left module or left vector space that are hyperplanes.
class LSHyp
Definition	df-lsatoms 32512*	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 32513*	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 32514*	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 32515*	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 32516*	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 32517	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 32518	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 32519	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 32520	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 32521	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 32522	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 32523	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 32524	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 32525	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 32526*	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 32527*	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 32528	The span of a non-zero singleton is an atom. TODO: make this obsolete and use lsatlspsn 32529 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 32529	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 32530*	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 32531*	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 32532	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 32533	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 32534	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 32535	A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 27997 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 32536	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 32537	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 32538	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 32539	If two atoms are comparable, they are equal. (atsseq 27999 analog.) TODO: can lspsncmp 18339 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 32540	If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 32539. TODO: can lspsncmp 18339 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 32541	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 32542	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 32543	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 32544*	Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 33340 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 32545*	Show equality with the span of the sum of two vectors, one of which ( X) is fixed in advance. Compare lspfixed 18351. (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 32546	Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 27304 analog.) Explicit atom version of lsmcv 18364. (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 32547*	The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 28010 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 32548*	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 28013 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 32549*	Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 28015 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 32550*	Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 28016 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 32551*	The ordering of two subspaces is determined by the atoms under them. (chrelat3 28023 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 32552*	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 28015 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 32553*	Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 32516. (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 32554	Extend class notation with the covering relation for a left module or left vector space.
class <oLL
Definition	df-lcv 32555*	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 32557 for binary relation. (df-cv 27931 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 32556*	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 32557*	The covers relation for a left vector space (or a left module). (cvbr 27934 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 32558*	The covers relation for a left vector space (or a left module). (cvbr2 27935 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 32559*	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 32560	The covers relation implies proper subset. (cvpss 27937 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 32561	The covers relation implies no in-betweenness. (cvnbtwn 27938 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 32562	The covers relation is not transitive. (cvntr 27944 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 32563	The covers relation implies no in-betweenness. (cvnbtwn2 27939 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 32564	The covers relation implies no in-betweenness. (cvnbtwn3 27940 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 32565	Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 27945 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 32566*	If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 28018 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 32567	An atom covers the zero subspace. (atcv0 27994 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 32568	A subspace covered by an atom must be the zero subspace. (atcveq0 28000 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 32569	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 32570	Lemma for lcvexch 32575. (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 32571	Lemma for lcvexch 32575. (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 32572	Lemma for lcvexch 32575. (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 32573	Lemma for lcvexch 32575. (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 32574	Lemma for lcvexch 32575. (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 32575	Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 28021 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 32576	Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 28027 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 32577	Covering property of a subspace plus an atom. (chcv1 28007 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 32578	Covering property of a subspace plus an atom. (chcv2 28008 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 32579	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 28033 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 32580	The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 28028 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 32581	The meet of distinct atoms is the zero subspace. (atnemeq0 28029 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 32582	The atom exch1ange property. (hlatexch1 32930 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 32583	If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 28031 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 32584	Two atoms covering the zero subspace are equal. (atcv1 28032 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 32585	Lemma for lsatcvat 32586. (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 32586	A nonzero subspace less than the sum of two atoms is an atom. (atcvati 28038 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 32587	A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 28039 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 32588	A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 28048 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 32589	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 32590	A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. (1cvrjat 33010 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 32591	Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (1cvrat 33011 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 32592	Create an atom under a hyperplane. Part of proof of Lemma B in [Crawley] p. 112. (lhpat 33578 analog.) TODO: This changes U C V in l1cvpat 32590 and l1cvat 32591 to U e. H, which in turn change U e. H in islshpcv 32589 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 32593	Extend class notation with all linear functionals of a left module or left vector space.
class LFnl
Definition	df-lfl 32594*	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 32595*	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 32596*	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 32597	Property of a linear functional. (lnfnli 27692 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 32598*	Properties that determine a linear functional. TODO: use this in place of islfl 32596 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 32599	A linear functional is a function from vectors to scalars. (lnfnfi 27693 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 32600	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 )