P. 377 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dochkrsm 37601	The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 37557 can be used to convert sum to join.) (Contributed by NM, 29-Jan-2015.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoH ` K ) ` W )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ran I )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( X .(+) ( ._|_ ` ( L ` G ) ) ) e. ran I )
Theorem	dochexmidat 37602	Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( ( ._|_ ` { X } ) .(+) ( N ` { X } ) ) = V )
Theorem	dochexmidlem1 37603	Lemma for dochexmid 37611. Holland's proof implicitly requires q =/= r, which we prove here. (Contributed by NM, 14-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> p e. A )   &    |- ( ph -> q e. A )   &    |- ( ph -> r e. A )   &    |- ( ph -> q C_ ( ._|_ ` X ) )   &    |- ( ph -> r C_ X )   =>    |- ( ph -> q =/= r )
Theorem	dochexmidlem2 37604	Lemma for dochexmid 37611. (Contributed by NM, 14-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> p e. A )   &    |- ( ph -> q e. A )   &    |- ( ph -> r e. A )   &    |- ( ph -> q C_ ( ._|_ ` X ) )   &    |- ( ph -> r C_ X )   &    |- ( ph -> p C_ ( r .(+) q ) )   =>    |- ( ph -> p C_ ( X .(+) ( ._|_ ` X ) ) )
Theorem	dochexmidlem3 37605	Lemma for dochexmid 37611. Use atom exchange lsatexch1 35187 to swap p and q. (Contributed by NM, 14-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> p e. A )   &    |- ( ph -> q e. A )   &    |- ( ph -> r e. A )   &    |- ( ph -> q C_ ( ._|_ ` X ) )   &    |- ( ph -> r C_ X )   &    |- ( ph -> q C_ ( r .(+) p ) )   =>    |- ( ph -> p C_ ( X .(+) ( ._|_ ` X ) ) )
Theorem	dochexmidlem4 37606	Lemma for dochexmid 37611. (Contributed by NM, 15-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> p e. A )   &    |- ( ph -> q e. A )   &    |- .0. = ( 0g ` U )   &    |- M = ( X .(+) p )   &    |- ( ph -> X =/= { .0. } )   &    |- ( ph -> q C_ ( ( ._|_ ` X ) i^i M ) )   =>    |- ( ph -> p C_ ( X .(+) ( ._|_ ` X ) ) )
Theorem	dochexmidlem5 37607	Lemma for dochexmid 37611. (Contributed by NM, 15-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> p e. A )   &    |- .0. = ( 0g ` U )   &    |- M = ( X .(+) p )   &    |- ( ph -> X =/= { .0. } )   &    |- ( ph -> -. p C_ ( X .(+) ( ._|_ ` X ) ) )   =>    |- ( ph -> ( ( ._|_ ` X ) i^i M ) = { .0. } )
Theorem	dochexmidlem6 37608	Lemma for dochexmid 37611. (Contributed by NM, 15-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> p e. A )   &    |- .0. = ( 0g ` U )   &    |- M = ( X .(+) p )   &    |- ( ph -> X =/= { .0. } )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )   &    |- ( ph -> -. p C_ ( X .(+) ( ._|_ ` X ) ) )   =>    |- ( ph -> M = X )
Theorem	dochexmidlem7 37609	Lemma for dochexmid 37611. Contradict dochexmidlem6 37608. (Contributed by NM, 15-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> p e. A )   &    |- .0. = ( 0g ` U )   &    |- M = ( X .(+) p )   &    |- ( ph -> X =/= { .0. } )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )   &    |- ( ph -> -. p C_ ( X .(+) ( ._|_ ` X ) ) )   =>    |- ( ph -> M =/= X )
Theorem	dochexmidlem8 37610	Lemma for dochexmid 37611. The contradiction of dochexmidlem6 37608 and dochexmidlem7 37609 shows that there can be no atom p that is not in X + ( ._|_ ` X ), which is therefore the whole atom space. (Contributed by NM, 15-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X =/= { .0. } )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )   =>    |- ( ph -> ( X .(+) ( ._|_ ` X ) ) = V )
Theorem	dochexmid 37611	Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 37520. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables X, M, p, q, r in place of Hollands' l, m, P, Q, L respectively. (pexmidALTN 36118 analog.) (Contributed by NM, 15-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( LSubSp ` U )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )   =>    |- ( ph -> ( X .(+) ( ._|_ ` X ) ) = V )
Theorem	dochsnkrlem1 37612	Lemma for dochsnkr 37615. (Contributed by NM, 1-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
Theorem	dochsnkrlem2 37613	Lemma for dochsnkr 37615. (Contributed by NM, 1-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )   &    |- A = (LSAtoms ` U )   =>    |- ( ph -> ( ._|_ ` ( L ` G ) ) e. A )
Theorem	dochsnkrlem3 37614	Lemma for dochsnkr 37615. (Contributed by NM, 2-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
Theorem	dochsnkr 37615	A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems) (Contributed by NM, 2-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )   =>    |- ( ph -> ( L ` G ) = ( ._|_ ` { X } ) )
Theorem	dochsnkr2 37616*	Kernel of the explicit functional G determined by a nonzero vector X. Compare the more general lshpkr 35258. (Contributed by NM, 27-Oct-2014.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- L = (LKer ` U )   &    |- D = (Scalar ` U )   &    |- R = ( Base ` D )   &    |- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( L ` G ) = ( ._|_ ` { X } ) )
Theorem	dochsnkr2cl 37617*	The X determining functional G belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- L = (LKer ` U )   &    |- D = (Scalar ` U )   &    |- R = ( Base ` D )   &    |- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
Theorem	dochflcl 37618*	Closure of the explicit functional G determined by a nonzero vector X. Compare the more general lshpkrcl 35257. (Contributed by NM, 27-Oct-2014.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- F = (LFnl ` U )   &    |- D = (Scalar ` U )   &    |- R = ( Base ` D )   &    |- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> G e. F )
Theorem	dochfl1 37619*	The value of the explicit functional G is 1 at the X that determines it. (Contributed by NM, 27-Oct-2014.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- D = (Scalar ` U )   &    |- R = ( Base ` D )   &    |- .1. = ( 1r ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )   =>    |- ( ph -> ( G ` X ) = .1. )
Theorem	dochfln0 37620	The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- N = ( 0g ` R )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )   =>    |- ( ph -> ( G ` X ) =/= N )
Theorem	dochkr1 37621*	A non-zero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 35211. (Contributed by NM, 2-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` U )   &    |- .1. = ( 1r ` R )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )   =>    |- ( ph -> E. x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) ( G ` x ) = .1. )
Theorem	dochkr1OLDN 37622*	A non-zero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 35211. (Contributed by NM, 2-Jan-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )   =>    |- ( ph -> E. x e. ( ._|_ ` ( L ` G ) ) ( G ` x ) = .1. )
21.29.11  Construction of involution and inner product from a Hilbert lattice
Syntax	clpoN 37623	Extend class notation with all polarities of a left module or left vector space.
class LPol
Definition	df-lpolN 37624*	Define the set of all polarities of a left module or left vector space. A polarity is a kind of complementation operation on a subspace. The double polarity of a subspace is a closure operation. Based on Definition 3.2 of [Holland95] p. 214 for projective geometry polarities. For convenience, we open up the domain to include all vector subsets and not just subspaces, but any more restricted polarity can be converted to this one by taking the span of its argument. (Contributed by NM, 24-Nov-2014.)
|- LPol = ( w e. _V |-> { o e. ( ( LSubSp ` w ) ^m ~P ( Base ` w ) ) | ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } /\ A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. (LSAtoms ` w ) ( ( o ` x ) e. (LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) ) } )
Theorem	lpolsetN 37625*	The set of polarities of a left module or left vector space. (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- H = (LSHyp ` W )   &    |- P = (LPol ` W )   =>    |- ( W e. X -> P = { o e. ( S ^m ~P V ) | ( ( o ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. A ( ( o ` x ) e. H /\ ( o ` ( o ` x ) ) = x ) ) } )
Theorem	islpolN 37626*	The predicate "is a polarity". (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- H = (LSHyp ` W )   &    |- P = (LPol ` W )   =>    |- ( W e. X -> ( ._|_ e. P <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
Theorem	islpoldN 37627*	Properties that determine a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- .0. = ( 0g ` W )   &    |- A = (LSAtoms ` W )   &    |- H = (LSHyp ` W )   &    |- P = (LPol ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> ._|_ : ~P V --> S )   &    |- ( ph -> ( ._|_ ` V ) = { .0. } )   &    |- ( ( ph /\ ( x C_ V /\ y C_ V /\ x C_ y ) ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) )   &    |- ( ( ph /\ x e. A ) -> ( ._|_ ` x ) e. H )   &    |- ( ( ph /\ x e. A ) -> ( ._|_ ` ( ._|_ ` x ) ) = x )   =>    |- ( ph -> ._|_ e. P )
Theorem	lpolfN 37628	Functionality of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- P = (LPol ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> ._|_ e. P )   =>    |- ( ph -> ._|_ : ~P V --> S )
Theorem	lpolvN 37629	The polarity of the whole space is the zero subspace. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- P = (LPol ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> ._|_ e. P )   =>    |- ( ph -> ( ._|_ ` V ) = { .0. } )
Theorem	lpolconN 37630	Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- P = (LPol ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> ._|_ e. P )   &    |- ( ph -> X C_ V )   &    |- ( ph -> Y C_ V )   &    |- ( ph -> X C_ Y )   =>    |- ( ph -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) )
Theorem	lpolsatN 37631	The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
|- A = (LSAtoms ` W )   &    |- H = (LSHyp ` W )   &    |- P = (LPol ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> ._|_ e. P )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( ._|_ ` Q ) e. H )
Theorem	lpolpolsatN 37632	Property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
|- A = (LSAtoms ` W )   &    |- P = (LPol ` W )   &    |- ( ph -> W e. X )   &    |- ( ph -> ._|_ e. P )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` Q ) ) = Q )
Theorem	dochpolN 37633	The subspace orthocomplement for the DVecH vector space is a polarity. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- P = (LPol ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ._|_ e. P )
Theorem	lcfl1lem 37634*	Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.)
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   =>    |- ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
Theorem	lcfl1 37635*	Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.)
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
Theorem	lcfl2 37636*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) ) )
Theorem	lcfl3 37637*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- A = (LSAtoms ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( ( ._|_ ` ( L ` G ) ) e. A \/ ( L ` G ) = V ) ) )
Theorem	lcfl4N 37638*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- Y = (LSHyp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y \/ ( L ` G ) = V ) ) )
Theorem	lcfl5 37639*	Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoH ` K ) ` W )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( L ` G ) e. ran I ) )
Theorem	lcfl5a 37640	Property of a functional with a closed kernel. TODO: Make lcfl5 37639 etc. obsolete and rewrite w/out C hypothesis? (Contributed by NM, 29-Jan-2015.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoH ` K ) ` W )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) <-> ( L ` G ) e. ran I ) )
Theorem	lcfl6lem 37641*	Lemma for lcfl6 37643. A functional G (whose kernel is closed by dochsnkr 37615) is comletely determined by a vector X in the orthocomplement in its kernel at which the functional value is 1. Note that the \ { .0. } in the X hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .1. = ( 1r ` S )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )   &    |- ( ph -> ( G ` X ) = .1. )   =>    |- ( ph -> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) )
Theorem	lcfl7lem 37642*	Lemma for lcfl7N 37644. If two functionals G and J are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )   &    |- J = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { Y } ) v = ( w .+ ( k .x. Y ) ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G = J )   =>    |- ( ph -> X = Y )
Theorem	lcfl6 37643*	Property of a functional with a closed kernel. Note that ( L ` G ) = V means the functional is zero by lkr0f 35235. (Contributed by NM, 3-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( ( L ` G ) = V \/ E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) )
Theorem	lcfl7N 37644*	Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that ( L ` G ) = V means the functional is zero by lkr0f 35235. (Contributed by NM, 4-Jan-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( ( L ` G ) = V \/ E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) )
Theorem	lcfl8 37645*	Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )
Theorem	lcfl8a 37646*	Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) <-> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )
Theorem	lcfl8b 37647*	Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Y = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. ( C \ { Y } ) )   =>    |- ( ph -> E. x e. ( V \ { .0. } ) ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) )
Theorem	lcfl9a 37648	Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( ._|_ ` { X } ) C_ ( L ` G ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
Theorem	lclkrlem1 37649*	The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .s ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> G e. C )   =>    |- ( ph -> ( X .x. G ) e. C )
Theorem	lclkrlem2a 37650	Lemma for lclkr 37676. Use lshpat 35197 to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )   &    |- ( ph -> -. X e. ( ._|_ ` { B } ) )   =>    |- ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )
Theorem	lclkrlem2b 37651	Lemma for lclkr 37676. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   =>    |- ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )
Theorem	lclkrlem2c 37652	Lemma for lclkr 37676. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- J = (LSHyp ` U )   =>    |- ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) e. J )
Theorem	lclkrlem2d 37653	Lemma for lclkr 37676. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- I = ( ( DIsoH ` K ) ` W )   =>    |- ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) e. ran I )
Theorem	lclkrlem2e 37654	Lemma for lclkr 37676. The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` E ) = ( L ` G ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2f 37655	Lemma for lclkr 37676. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( L ` E ) =/= ( L ` G ) )   &    |- ( ph -> ( L ` ( E .+ G ) ) e. J )   =>    |- ( ph -> ( ( ( L ` E ) i^i ( L ` G ) ) .(+) ( N ` { B } ) ) C_ ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2g 37656	Lemma for lclkr 37676. Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( L ` E ) =/= ( L ` G ) )   &    |- ( ph -> ( L ` ( E .+ G ) ) e. J )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2h 37657	Lemma for lclkr 37676. Eliminate the ( L ` ( E .+ G ) ) e. J hypothesis. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( L ` E ) =/= ( L ` G ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2i 37658	Lemma for lclkr 37676. Eliminate the ( L ` E ) =/= ( L ` G ) hypothesis. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2j 37659	Lemma for lclkr 37676. Kernel closure when Y is zero. (Contributed by NM, 18-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y = .0. )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2k 37660	Lemma for lclkr 37676. Kernel closure when X is zero. (Contributed by NM, 18-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X = .0. )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2l 37661	Lemma for lclkr 37676. Eliminate the X =/= .0., Y =/= .0. hypotheses. (Contributed by NM, 18-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2m 37662	Lemma for lclkr 37676. Construct a vector B that makes the sum of functionals zero. Combine with B e. V to shorten overall proof. (Contributed by NM, 17-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> U e. LVec )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   =>    |- ( ph -> ( B e. V /\ ( ( E .+ G ) ` B ) = .0. ) )
Theorem	lclkrlem2n 37663	Lemma for lclkr 37676. (Contributed by NM, 12-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> U e. LVec )   &    |- ( ph -> ( ( E .+ G ) ` X ) = .0. )   &    |- ( ph -> ( ( E .+ G ) ` Y ) = .0. )   =>    |- ( ph -> ( N ` { X , Y } ) C_ ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2o 37664	Lemma for lclkr 37676. When B is nonzero, the vectors X and Y can't both belong to the hyperplane generated by B. (Contributed by NM, 17-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B =/= ( 0g ` U ) )   =>    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )
Theorem	lclkrlem2p 37665	Lemma for lclkr 37676. When B is zero, X and Y must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B = ( 0g ` U ) )   =>    |- ( ph -> ( ._|_ ` { Y } ) C_ ( ._|_ ` { X } ) )
Theorem	lclkrlem2q 37666	Lemma for lclkr 37676. The sum has a closed kernel when B is nonzero. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B =/= ( 0g ` U ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2r 37667	Lemma for lclkr 37676. When B is zero, i.e. when X and Y are colinear, the intersection of the kernels of E and G equal the kernel of G, so the kernels of G and the sum are comparable. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B = ( 0g ` U ) )   =>    |- ( ph -> ( L ` G ) C_ ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2s 37668	Lemma for lclkr 37676. Thus, the sum has a closed kernel when B is zero. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B = ( 0g ` U ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2t 37669	Lemma for lclkr 37676. We eliminate all hypotheses with B here. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2u 37670	Lemma for lclkr 37676. lclkrlem2t 37669 with X and Y swapped. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` X ) =/= .0. )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2v 37671	Lemma for lclkr 37676. When the hypotheses of lclkrlem2u 37670 and lclkrlem2u 37670 are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid 37611, which requires the orthomodular law dihoml4 37520 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` X ) = .0. )   &    |- ( ph -> ( ( E .+ G ) ` Y ) = .0. )   =>    |- ( ph -> ( L ` ( E .+ G ) ) = V )
Theorem	lclkrlem2w 37672	Lemma for lclkr 37676. This is the same as lclkrlem2u 37670 and lclkrlem2u 37670 with the inequality hypotheses negated. When the sum of two functionals is zero at each generating vector, the kernel is the vector space and therefore closed. (Contributed by NM, 16-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` X ) = .0. )   &    |- ( ph -> ( ( E .+ G ) ` Y ) = .0. )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2x 37673	Lemma for lclkr 37676. Eliminate by cases the hypotheses of lclkrlem2u 37670, lclkrlem2u 37670 and lclkrlem2w 37672. (Contributed by NM, 18-Jan-2015.)
|- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2y 37674	Lemma for lclkr 37676. Restate the hypotheses for E and G to say their kernels are closed, in order to eliminate the generating vectors X and Y. (Contributed by NM, 18-Jan-2015.)
|- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2 37675*	The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 37650 through lclkrlem2y 37674 are used for the proof. Here we express lclkrlem2y 37674 in terms of membership in the set C of functionals with closed kernels. (Contributed by NM, 18-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> E e. C )   &    |- ( ph -> G e. C )   =>    |- ( ph -> ( E .+ G ) e. C )
Theorem	lclkr 37676*	The set of functionals with closed kernels is a subspace. Part of proof of Theorem 3.6 of [Holland95] p. 218, line 20, stating "The fM that arise this way generate a subspace F of E'". Our proof was suggested by Mario Carneiro, 5-Jan-2015. (Contributed by NM, 18-Jan-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- S = ( LSubSp ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> C e. S )
Theorem	lcfls1lem 37677*	Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.)
|- C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }   =>    |- ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
Theorem	lcfls1N 37678*	Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.)
|- C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) ) )
Theorem	lcfls1c 37679*	Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.)
|- C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }   &    |- D = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   =>    |- ( G e. C <-> ( G e. D /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
Theorem	lclkrslem1 37680*	The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. (Contributed by NM, 27-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .s ` D )   &    |- C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> Q e. S )   &    |- ( ph -> G e. C )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X .x. G ) e. C )
Theorem	lclkrslem2 37681*	The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. (Contributed by NM, 28-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .s ` D )   &    |- C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> Q e. S )   &    |- ( ph -> G e. C )   &    |- .+ = ( +g ` D )   &    |- ( ph -> E e. C )   =>    |- ( ph -> ( E .+ G ) e. C )
Theorem	lclkrs 37682*	The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace R is a subspace of the dual space. TODO: This proof repeats large parts of the lclkr 37676 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 37676 a special case of this? (Contributed by NM, 29-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ R ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> R e. S )   =>    |- ( ph -> C e. T )
Theorem	lclkrs2 37683*	The set of functionals with closed kernels and majorizing the orthocomplement of a given subspace Q is a subspace of the dual space containing functionals with closed kernels. Note that R is the value given by mapdval 37771. (Contributed by NM, 12-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- R = { g e. F | ( ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) /\ ( ._|_ ` ( L ` g ) ) C_ Q ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> Q e. S )   =>    |- ( ph -> ( R e. T /\ R C_ C ) )
Theorem	lcfrvalsnN 37684*	Reconstruction from the dual space span of a singleton. (Contributed by NM, 19-Feb-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- N = ( LSpan ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- Q = U_ f e. R ( ._|_ ` ( L ` f ) )   &    |- R = ( N ` { G } )   =>    |- ( ph -> Q = ( ._|_ ` ( L ` G ) ) )
Theorem	lcfrlem1 37685	Lemma for lcfr 37728. Note that X is z in Mario's notes. (Contributed by NM, 27-Feb-2015.)
|- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .x. = ( .s ` D )   &    |- .- = ( -g ` D )   &    |- ( ph -> U e. LVec )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( G ` X ) =/= .0. )   &    |- H = ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) )   =>    |- ( ph -> ( H ` X ) = .0. )
Theorem	lcfrlem2 37686	Lemma for lcfr 37728. (Contributed by NM, 27-Feb-2015.)
|- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .x. = ( .s ` D )   &    |- .- = ( -g ` D )   &    |- ( ph -> U e. LVec )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( G ` X ) =/= .0. )   &    |- H = ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) )   &    |- L = (LKer ` U )   =>    |- ( ph -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( L ` H ) )
Theorem	lcfrlem3 37687	Lemma for lcfr 37728. (Contributed by NM, 27-Feb-2015.)
|- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .x. = ( .s ` D )   &    |- .- = ( -g ` D )   &    |- ( ph -> U e. LVec )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( G ` X )