P. 344 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34301-34400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lrelat 34301*	Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 29223 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 34302*	The ordering of two subspaces is determined by the atoms under them. (chrelat3 29230 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 34303*	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 29222 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 34304*	Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 34267. (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 34305	Extend class notation with the covering relation for a left module or left vector space.
class <oLL
Definition	df-lcv 34306*	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 34308 for binary relation. (df-cv 29138 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 34307*	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 34308*	The covers relation for a left vector space (or a left module). (cvbr 29141 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 34309*	The covers relation for a left vector space (or a left module). (cvbr2 29142 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 34310*	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 34311	The covers relation implies proper subset. (cvpss 29144 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 34312	The covers relation implies no in-betweenness. (cvnbtwn 29145 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 34313	The covers relation is not transitive. (cvntr 29151 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 34314	The covers relation implies no in-betweenness. (cvnbtwn2 29146 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 34315	The covers relation implies no in-betweenness. (cvnbtwn3 29147 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 34316	Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 29152 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 34317*	If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 29225 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 34318	An atom covers the zero subspace. (atcv0 29201 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 34319	A subspace covered by an atom must be the zero subspace. (atcveq0 29207 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 34320	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 34321	Lemma for lcvexch 34326. (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 34322	Lemma for lcvexch 34326. (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 34323	Lemma for lcvexch 34326. (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 34324	Lemma for lcvexch 34326. (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 34325	Lemma for lcvexch 34326. (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 34326	Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 29228 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 34327	Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 29234 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 34328	Covering property of a subspace plus an atom. (chcv1 29214 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 34329	Covering property of a subspace plus an atom. (chcv2 29215 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 34330	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 29240 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 34331	The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 29235 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 34332	The meet of distinct atoms is the zero subspace. (atnemeq0 29236 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 34333	The atom exch1ange property. (hlatexch1 34681 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 34334	If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 29238 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 34335	Two atoms covering the zero subspace are equal. (atcv1 29239 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 34336	Lemma for lsatcvat 34337. (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 34337	A nonzero subspace less than the sum of two atoms is an atom. (atcvati 29245 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 34338	A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 29246 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 34339	A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 29255 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 34340	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 34341	A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. (1cvrjat 34761 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 34342	Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (1cvrat 34762 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 34343	Create an atom under a hyperplane. Part of proof of Lemma B in [Crawley] p. 112. (lhpat 35329 analog.) TODO: This changes U C V in l1cvpat 34341 and l1cvat 34342 to U e. H, which in turn change U e. H in islshpcv 34340 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 )
20.23.7  Functionals and kernels of a left vector space (or module)
Syntax	clfn 34344	Extend class notation with all linear functionals of a left module or left vector space.
class LFnl
Definition	df-lfl 34345*	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 34346*	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 34347*	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 34348	Property of a linear functional. (lnfnli 28899 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 34349*	Properties that determine a linear functional. TODO: use this in place of islfl 34347 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 34350	A linear functional is a function from vectors to scalars. (lnfnfi 28900 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 34351	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 34352	A linear functional is zero at the zero vector. (lnfn0i 28901 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 34353	Property of a linear functional. (lnfnaddi 28902 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 34354	Property of a linear functional. (lnfnaddi 28902 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 34355	Property of a linear functional. (lnfnmuli 28903 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 34356	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 34357*	A nonzero 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 34358	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 34359	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 34360	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 34361	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 34362*	Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp 34433, 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 34363*	A functional plus its negative is the zero functional. (This is specialized for the purpose of proving ldualgrp 34433, 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 34364	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 34365	Distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( ( G oF .+ H ) oF .x. ( V X. { X } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( H oF .x. ( V X. { X } ) ) ) )
Theorem	lflvsdi2 34366	Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( ( V X. { X } ) oF .+ ( V X. { Y } ) ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )
Theorem	lflvsdi2a 34367	Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 21-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( V X. { ( X .+ Y ) } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )
Theorem	lflvsass 34368	Associative law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- F = (LFnl ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( V X. { ( X .x. Y ) } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .x. ( V X. { Y } ) ) )
Theorem	lfl0sc 34369	The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of ( V X. { .0. } ) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- F = (LFnl ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( V X. { .0. } ) ) = ( V X. { .0. } ) )
Theorem	lflsc0N 34370	The scalar product with the zero functional is the zero functional. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   =>    |- ( ph -> ( ( V X. { .0. } ) oF .x. ( V X. { X } ) ) = ( V X. { .0. } ) )
Theorem	lfl1sc 34371	The (right vector space) scalar product of a functional with one is the functional. (Contributed by NM, 21-Oct-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- F = (LFnl ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- .1. = ( 1r ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G oF .x. ( V X. { .1. } ) ) = G )
Syntax	clk 34372	Extend class notation with the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space.
class LKer
Definition	df-lkr 34373*	Define the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. (Contributed by NM, 15-Apr-2014.)
|- LKer = ( w e. _V |-> ( f e. (LFnl ` w ) |-> ( `' f " { ( 0g ` (Scalar ` w ) ) } ) ) )
Theorem	lkrfval 34374*	The kernel of a functional. (Contributed by NM, 15-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( W e. X -> K = ( f e. F |-> ( `' f " { .0. } ) ) )
Theorem	lkrval 34375	Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. X /\ G e. F ) -> ( K ` G ) = ( `' G " { .0. } ) )
Theorem	ellkr 34376	Membership in the kernel of a functional. (elnlfn 28787 analog.) (Contributed by NM, 16-Apr-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. Y /\ G e. F ) -> ( X e. ( K ` G ) <-> ( X e. V /\ ( G ` X ) = .0. ) ) )
Theorem	lkrval2 34377*	Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. X /\ G e. F ) -> ( K ` G ) = { x e. V | ( G ` x ) = .0. } )
Theorem	ellkr2 34378	Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. Y )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( X e. ( K ` G ) <-> ( G ` X ) = .0. ) )
Theorem	lkrcl 34379	A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014.)
|- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. Y /\ G e. F /\ X e. ( K ` G ) ) -> X e. V )
Theorem	lkrf0 34380	The value of a functional at a member of its kernel is zero. (Contributed by NM, 16-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. Y /\ G e. F /\ X e. ( K ` G ) ) -> ( G ` X ) = .0. )
Theorem	lkr0f 34381	The kernel of the zero functional is the set of all vectors. (Contributed by NM, 17-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V <-> G = ( V X. { .0. } ) ) )
Theorem	lkrlss 34382	The kernel of a linear functional is a subspace. (nlelshi 28919 analog.) (Contributed by NM, 16-Apr-2014.)
|- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ G e. F ) -> ( K ` G ) e. S )
Theorem	lkrssv 34383	The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015.)
|- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( K ` G ) C_ V )
Theorem	lkrsc 34384	The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 9-Oct-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   &    |- ( ph -> R e. K )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> R =/= .0. )   =>    |- ( ph -> ( L ` ( G oF .x. ( V X. { R } ) ) ) = ( L ` G ) )
Theorem	lkrscss 34385	The kernel of a scalar product of a functional includes the kernel of the functional. (The inclusion is proper for the zero product and equality otherwise.) (Contributed by NM, 9-Oct-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   &    |- ( ph -> R e. K )   =>    |- ( ph -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { R } ) ) ) )
Theorem	eqlkr 34386*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 18-Apr-2014.)
|- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) )
Theorem	eqlkr2 34387*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 10-Oct-2014.)
|- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) -> E. r e. K H = ( G oF .x. ( V X. { r } ) ) )
Theorem	eqlkr3 34388	Two functionals with the same kernel are equal if they are equal at any nonzero value. (Contributed by NM, 2-Jan-2015.)
|- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` S )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   &    |- ( ph -> ( K ` G ) = ( K ` H ) )   &    |- ( ph -> ( G ` X ) = ( H ` X ) )   &    |- ( ph -> ( G ` X ) =/= .0. )   =>    |- ( ph -> G = H )
Theorem	lkrlsp 34389	The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr 34376) is the whole vector space. (Contributed by NM, 19-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )
Theorem	lkrlsp2 34390	The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 12-May-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )
Theorem	lkrlsp3 34391	The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( N ` ( ( K ` G ) u. { X } ) ) = V )
Theorem	lkrshp 34392	The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( K ` G ) e. H )
Theorem	lkrshp3 34393	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) e. H <-> G =/= ( V X. { .0. } ) ) )
Theorem	lkrshpor 34394	The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014.)
|- V = ( Base ` W )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) e. H \/ ( K ` G ) = V ) )
Theorem	lkrshp4 34395	A kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.)
|- V = ( Base ` W )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) =/= V <-> ( K ` G ) e. H ) )
Theorem	lshpsmreu 34396*	Lemma for lshpkrex 34405. Show uniqueness of ring multiplier k when a vector X is broken down into components, one in a hyperplane and the other outside of it . TODO: do we need the cbvrexv 3172 for a to c? (Contributed by NM, 4-Jan-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   =>    |- ( ph -> E! k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) )
Theorem	lshpkrlem1 34397*	Lemma for lshpkrex 34405. The value of tentative functional G is zero iff its argument belongs to hyperplane U. (Contributed by NM, 14-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ph -> ( X e. U <-> ( G ` X ) = .0. ) )
Theorem	lshpkrlem2 34398*	Lemma for lshpkrex 34405. The value of tentative functional G is a scalar. (Contributed by NM, 16-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ph -> ( G ` X ) e. K )
Theorem	lshpkrlem3 34399*	Lemma for lshpkrex 34405. Defining property of G ` X. (Contributed by NM, 15-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ph -> E. z e. U X = ( z .+ ( ( G ` X ) .x. Z ) ) )
Theorem	lshpkrlem4 34400*	Lemma for lshpkrex 34405. Part of showing linearity of G. (Contributed by NM, 16-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) ) ) -> ( ( l .x. u ) .+ v ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) )