P. 352 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	dochexmidlem3 35101	Lemma for dochexmid 35107. Use atom exchange lsatexch1 32683 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 35102	Lemma for dochexmid 35107. (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 35103	Lemma for dochexmid 35107. (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 35104	Lemma for dochexmid 35107. (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 35105	Lemma for dochexmid 35107. Contradict dochexmidlem6 35104. (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 35106	Lemma for dochexmid 35107. The contradiction of dochexmidlem6 35104 and dochexmidlem7 35105 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 35107	Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 35016. 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 33614 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 35108	Lemma for dochsnkr 35111. (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 35109	Lemma for dochsnkr 35111. (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 35110	Lemma for dochsnkr 35111. (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 35111	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 35112*	Kernel of the explicit functional G determined by a nonzero vector X. Compare the more general lshpkr 32754. (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 35113*	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 35114*	Closure of the explicit functional G determined by a nonzero vector X. Compare the more general lshpkrcl 32753. (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 35115*	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 35116	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 35117*	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 32707. (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 35118*	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 32707. (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.21.14  Construction of involution and inner product from a Hilbert lattice
Syntax	clpoN 35119	Extend class notation with all polarities of a left module or left vector space.
class LPol
Definition	df-lpolN 35120*	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 35121*	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 35122*	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 35123*	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 35124	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 35125	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 35126	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 35127	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 35128	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 35129	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 35130*	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 35131*	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 35132*	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 35133*	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 35134*	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 35135*	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 35136	Property of a functional with a closed kernel. TODO: Make lcfl5 35135 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 35137*	Lemma for lcfl6 35139. A functional G (whose kernel is closed by dochsnkr 35111) 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 35138*	Lemma for lcfl7N 35140. 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 35139*	Property of a functional with a closed kernel. Note that ( L ` G ) = V means the functional is zero by lkr0f 32731. (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 35140*	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 32731. (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 35141*	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 35142*	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 35143*	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 35144	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 35145*	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 35146	Lemma for lclkr 35172. Use lshpat 32693 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 35147	Lemma for lclkr 35172. (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 35148	Lemma for lclkr 35172. (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 35149	Lemma for lclkr 35172. (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 35150	Lemma for lclkr 35172. 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 35151	Lemma for lclkr 35172. 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 35152	Lemma for lclkr 35172. 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 35153	Lemma for lclkr 35172. 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 35154	Lemma for lclkr 35172. 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 35155	Lemma for lclkr 35172. 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 35156	Lemma for lclkr 35172. 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 35157	Lemma for lclkr 35172. 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 35158	Lemma for lclkr 35172. 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 35159	Lemma for lclkr 35172. (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 35160	Lemma for lclkr 35172. 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 35161	Lemma for lclkr 35172. 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 35162	Lemma for lclkr 35172. 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 35163	Lemma for lclkr 35172. 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 35164	Lemma for lclkr 35172. 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 35165	Lemma for lclkr 35172. 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 35166	Lemma for lclkr 35172. lclkrlem2t 35165 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 35167	Lemma for lclkr 35172. When the hypotheses of lclkrlem2u 35166 and lclkrlem2u 35166 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 35107, which requires the orthomodular law dihoml4 35016 (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 35168	Lemma for lclkr 35172. This is the same as lclkrlem2u 35166 and lclkrlem2u 35166 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 35169	Lemma for lclkr 35172. Eliminate by cases the hypotheses of lclkrlem2u 35166, lclkrlem2u 35166 and lclkrlem2w 35168. (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 35170	Lemma for lclkr 35172. 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 35171*	The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 35146 through lclkrlem2y 35170 are used for the proof. Here we express lclkrlem2y 35170 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 35172*	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 35173*	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 35174*	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 35175*	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 35176*	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 35177*	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 35178*	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 35172 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 35172 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 35179*	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 35267. (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 35180*	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 35181	Lemma for lcfr 35224. 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 35182	Lemma for lcfr 35224. (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 35183	Lemma for lcfr 35224. (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 -> X e. ( L ` H ) )
Theorem	lcfrlem4 35184*	Lemma for lcfr 35224. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> X e. E )   =>    |- ( ph -> X e. V )
Theorem	lcfrlem5 35185*	Lemma for lcfr 35224. The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. TODO: share hypotheses with others. Use more consistent variable names here or elsewhere when possible. (Contributed by NM, 5-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- S = ( LSubSp ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> R e. S )   &    |- Q = U_ f e. R ( ._|_ ` ( L ` f ) )   &    |- ( ph -> X e. Q )   &    |- C = (Scalar ` U )   &    |- B = ( Base ` C )   &    |- .x. = ( .s ` U )   &    |- ( ph -> A e. B )   =>    |- ( ph -> ( A .x. X ) e. Q )
Theorem	lcfrlem6 35186*	Lemma for lcfr 35224. Closure of vector sum with colinear vectors. TODO: Move down N definition so top hypotheses can be shared. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   &    |- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem7 35187*	Lemma for lcfr 35224. Closure of vector sum when one vector is zero. TODO: share hypotheses with others. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &