P. 355 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35401-35500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvh3dim2 35401*	There is a vector that is outside of 2 spans with a common vector. (Contributed by NM, 13-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )
Theorem	dvh3dim3N 35402*	There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 35401 everywhere. If this one is needed, make dvh3dim2 35401 into a lemma. (Contributed by NM, 21-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> T e. V )   =>    |- ( ph -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
Theorem	dochsnnz 35403	The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ._|_ ` { X } ) =/= { .0. } )
Theorem	dochsatshp 35404	The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014.) (Revised by Mario Carneiro, 1-Oct-2014.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- A = (LSAtoms ` U )   &    |- Y = (LSHyp ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( ._|_ ` Q ) e. Y )
Theorem	dochsatshpb 35405	The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- A = (LSAtoms ` U )   &    |- Y = (LSHyp ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> Q e. S )   =>    |- ( ph -> ( Q e. A <-> ( ._|_ ` Q ) e. Y ) )
Theorem	dochsnshp 35406	The orthocomplement of a nonzero singleton is a hyperplane. (Contributed by NM, 3-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- Y = (LSHyp ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( ._|_ ` { X } ) e. Y )
Theorem	dochshpsat 35407	A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- A = (LSAtoms ` U )   &    |- Y = (LSHyp ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. Y )   =>    |- ( ph -> ( ( ._|_ ` ( ._|_ ` X ) ) = X <-> ( ._|_ ` X ) e. A ) )
Theorem	dochkrsat 35408	The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- A = (LSAtoms ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( ._|_ ` ( L ` G ) ) =/= { .0. } <-> ( ._|_ ` ( L ` G ) ) e. A ) )
Theorem	dochkrsat2 35409	The orthocomplement of a kernel is an atom iff the double orthocomplement is not the vector space. (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 )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( L ` G ) ) e. A ) )
Theorem	dochsat0 35410	The orthocomplement of a kernel is either an atom or zero. (Contributed by NM, 29-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .0. = ( 0g ` U )   &    |- A = (LSAtoms ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( ._|_ ` ( L ` G ) ) e. A \/ ( ._|_ ` ( L ` G ) ) = { .0. } ) )
Theorem	dochkrsm 35411	The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 35367 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 35412	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 35413	Lemma for dochexmid 35421. 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 35414	Lemma for dochexmid 35421. (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 35415	Lemma for dochexmid 35421. Use atom exchange lsatexch1 32999 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 35416	Lemma for dochexmid 35421. (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 35417	Lemma for dochexmid 35421. (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 35418	Lemma for dochexmid 35421. (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 35419	Lemma for dochexmid 35421. Contradict dochexmidlem6 35418. (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 35420	Lemma for dochexmid 35421. The contradiction of dochexmidlem6 35418 and dochexmidlem7 35419 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 35421	Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 35330. 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 33930 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 35422	Lemma for dochsnkr 35425. (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 35423	Lemma for dochsnkr 35425. (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 35424	Lemma for dochsnkr 35425. (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 35425	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 35426*	Kernel of the explicit functional G determined by a nonzero vector X. Compare the more general lshpkr 33070. (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 35427*	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 35428*	Closure of the explicit functional G determined by a nonzero vector X. Compare the more general lshpkrcl 33069. (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 35429*	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 35430	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 35431*	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 33023. (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 35432*	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 33023. (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.30.11  Construction of involution and inner product from a Hilbert lattice
Syntax	clpoN 35433	Extend class notation with all polarities of a left module or left vector space.
class LPol
Definition	df-lpolN 35434*	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 35435*	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 35436*	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 35437*	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 35438	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 35439	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 35440	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 35441	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 35442	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 35443	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 35444*	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 35445*	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 35446*	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 35447*	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 35448*	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 35449*	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 35450	Property of a functional with a closed kernel. TODO: Make lcfl5 35449 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 35451*	Lemma for lcfl6 35453. A functional G (whose kernel is closed by dochsnkr 35425) 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 35452*	Lemma for lcfl7N 35454. 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 35453*	Property of a functional with a closed kernel. Note that ( L ` G ) = V means the functional is zero by lkr0f 33047. (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 35454*	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 33047. (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 35455*	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 35456*	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 35457*	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 35458	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 35459*	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 35460	Lemma for lclkr 35486. Use lshpat 33009 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 35461	Lemma for lclkr 35486. (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 35462	Lemma for lclkr 35486. (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 35463	Lemma for lclkr 35486. (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 35464	Lemma for lclkr 35486. 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 35465	Lemma for lclkr 35486. 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 35466	Lemma for lclkr 35486. 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 35467	Lemma for lclkr 35486. 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 35468	Lemma for lclkr 35486. 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 35469	Lemma for lclkr 35486. 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 35470	Lemma for lclkr 35486. 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 35471	Lemma for lclkr 35486. 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 35472	Lemma for lclkr 35486. 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 35473	Lemma for lclkr 35486. (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 35474	Lemma for lclkr 35486. 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 35475	Lemma for lclkr 35486. 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 35476	Lemma for lclkr 35486. 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 35477	Lemma for lclkr 35486. 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 35478	Lemma for lclkr 35486. 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 35479	Lemma for lclkr 35486. 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 35480	Lemma for lclkr 35486. lclkrlem2t 35479 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 35481	Lemma for lclkr 35486. When the hypotheses of lclkrlem2u 35480 and lclkrlem2u 35480 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 35421, which requires the orthomodular law dihoml4 35330 (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 35482	Lemma for lclkr 35486. This is the same as lclkrlem2u 35480 and lclkrlem2u 35480 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 35483	Lemma for lclkr 35486. Eliminate by cases the hypotheses of lclkrlem2u 35480, lclkrlem2u 35480 and lclkrlem2w 35482. (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 35484	Lemma for lclkr 35486. 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 35485*	The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 35460 through lclkrlem2y 35484 are used for the proof. Here we express lclkrlem2y 35484 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 35486*	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 35487*	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 35488*	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 35489*	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 35490*	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 35491*	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