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	lclkr 35101*	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 35102*	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 35103*	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 35104*	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 35105*	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 35106*	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 35107*	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 35101 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 35101 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 35108*	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 35196. (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 35109*	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 35110	Lemma for lcfr 35153. 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 35111	Lemma for lcfr 35153. (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 35112	Lemma for lcfr 35153. (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 35113*	Lemma for lcfr 35153. (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 35114*	Lemma for lcfr 35153. 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 35115*	Lemma for lcfr 35153. 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 35116*	Lemma for lcfr 35153. 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 )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> X e. E )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> Y = .0. )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem8 35117*	Lemma for lcf1o 35119 and lcfr 35153. (Contributed by NM, 21-Feb-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( 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 -> ( J ` X ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) )
Theorem	lcfrlem9 35118*	Lemma for lcf1o 35119. (This part has undesirable $d's on J and ph that we remove in lcf1o 35119.) TODO: ugly proof; maybe have better subtheorems or abbreviate some iota_ k expansions with J ` z? TODO: Some redundant $d's? (Contributed by NM, 22-Feb-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> J : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )
Theorem	lcf1o 35119*	Define a function J that provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C. (Contributed by NM, 22-Feb-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> J : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )
Theorem	lcfrlem10 35120*	Lemma for lcfr 35153. (Contributed by NM, 23-Feb-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( 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 -> ( J ` X ) e. F )
Theorem	lcfrlem11 35121*	Lemma for lcfr 35153. (Contributed by NM, 23-Feb-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( 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 ` ( J ` X ) ) = ( ._|_ ` { X } ) )
Theorem	lcfrlem12N 35122*	Lemma for lcfr 35153. (Contributed by NM, 23-Feb-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( 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. } ) )   &    |- B = ( 0g ` S )   &    |- ( ph -> Y e. ( ._|_ ` { X } ) )   =>    |- ( ph -> ( ( J ` X ) ` Y ) = B )
Theorem	lcfrlem13 35123*	Lemma for lcfr 35153. (Contributed by NM, 8-Mar-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( 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 -> ( J ` X ) e. ( C \ { Q } ) )
Theorem	lcfrlem14 35124*	Lemma for lcfr 35153. (Contributed by NM, 10-Mar-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( 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. } ) )   &    |- N = ( LSpan ` U )   =>    |- ( ph -> ( ._|_ ` ( L ` ( J ` X ) ) ) = ( N ` { X } ) )
Theorem	lcfrlem15 35125*	Lemma for lcfr 35153. (Contributed by NM, 9-Mar-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( 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 ` ( J ` X ) ) ) )
Theorem	lcfrlem16 35126*	Lemma for lcfr 35153. (Contributed by NM, 8-Mar-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 )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- P = ( LSubSp ` D )   &    |- ( ph -> G e. P )   &    |- ( ph -> G C_ C )   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> X e. ( E \ { .0. } ) )   =>    |- ( ph -> ( J ` X ) e. G )
Theorem	lcfrlem17 35127	Lemma for lcfr 35153. Condition needed more than once. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( X .+ Y ) e. ( V \ { .0. } ) )
Theorem	lcfrlem18 35128	Lemma for lcfr 35153. (Contributed by NM, 24-Feb-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( ._|_ ` { X , Y } ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
Theorem	lcfrlem19 35129	Lemma for lcfr 35153. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( -. X e. ( ._|_ ` { ( X .+ Y ) } ) \/ -. Y e. ( ._|_ ` { ( X .+ Y ) } ) ) )
Theorem	lcfrlem20 35130	Lemma for lcfr 35153. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. X e. ( ._|_ ` { ( X .+ Y ) } ) )   =>    |- ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )
Theorem	lcfrlem21 35131	Lemma for lcfr 35153. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )
Theorem	lcfrlem22 35132	Lemma for lcfr 35153. (Contributed by NM, 24-Feb-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   =>    |- ( ph -> B e. A )
Theorem	lcfrlem23 35133	Lemma for lcfr 35153. TODO: this proof was built from other proof pieces that may change N ` { X , Y } into subspace sum and back unnecessarily, or similar things. (Contributed by NM, 1-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ph -> ( ( ._|_ ` { X , Y } ) .(+) B ) = ( ._|_ ` { ( X .+ Y ) } ) )
Theorem	lcfrlem24 35134*	Lemma for lcfr 35153. (Contributed by NM, 24-Feb-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   =>    |- ( ph -> ( ._|_ ` { X , Y } ) = ( ( L ` ( J ` X ) ) i^i ( L ` ( J ` Y ) ) ) )
Theorem	lcfrlem25 35135*	Lemma for lcfr 35153. Special case of lcfrlem35 35145 when ( ( J ` Y ) ` I ) is zero. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) = Q )   &    |- ( ph -> I =/= .0. )   =>    |- ( ph -> ( ._|_ ` { ( X .+ Y ) } ) = ( L ` ( J ` Y ) ) )
Theorem	lcfrlem26 35136*	Lemma for lcfr 35153. Special case of lcfrlem36 35146 when ( ( J ` Y ) ` I ) is zero. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) = Q )   &    |- ( ph -> I =/= .0. )   =>    |- ( ph -> ( X .+ Y ) e. ( ._|_ ` ( L ` ( J ` Y ) ) ) )
Theorem	lcfrlem27 35137*	Lemma for lcfr 35153. Special case of lcfrlem37 35147 when ( ( J ` Y ) ` I ) is zero. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) = Q )   &    |- ( ph -> I =/= .0. )   &    |- ( ph -> G e. ( LSubSp ` D ) )   &    |- ( ph -> G C_ { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem28 35138*	Lemma for lcfr 35153. TODO: This can be a hypothesis since the zero version of ( J ` Y ) ` I needs it. (Contributed by NM, 9-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   =>    |- ( ph -> I =/= .0. )
Theorem	lcfrlem29 35139*	Lemma for lcfr 35153. (Contributed by NM, 9-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   =>    |- ( ph -> ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) e. R )
Theorem	lcfrlem30 35140*	Lemma for lcfr 35153. (Contributed by NM, 6-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   =>    |- ( ph -> C e. (LFnl ` U ) )
Theorem	lcfrlem31 35141*	Lemma for lcfr 35153. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   &    |- ( ph -> ( ( J ` X ) ` I ) =/= Q )   &    |- ( ph -> C = ( 0g ` D ) )   =>    |- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )
Theorem	lcfrlem32 35142*	Lemma for lcfr 35153. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   &    |- ( ph -> ( ( J ` X ) ` I ) =/= Q )   =>    |- ( ph -> C =/= ( 0g ` D ) )
Theorem	lcfrlem33 35143*	Lemma for lcfr 35153. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   &    |- ( ph -> ( ( J ` X ) ` I ) = Q )   =>    |- ( ph -> C =/= ( 0g ` D ) )
Theorem	lcfrlem34 35144*	Lemma for lcfr 35153. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   =>    |- ( ph -> C =/= ( 0g ` D ) )
Theorem	lcfrlem35 35145*	Lemma for lcfr 35153. (Contributed by NM, 2-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   =>    |- ( ph -> ( ._|_ ` { ( X .+ Y ) } ) = ( L ` C ) )
Theorem	lcfrlem36 35146*	Lemma for lcfr 35153. (Contributed by NM, 6-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   =>    |- ( ph -> ( X .+ Y ) e. ( ._|_ ` ( L ` C ) ) )
Theorem	lcfrlem37 35147*	Lemma for lcfr 35153. (Contributed by NM, 8-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   &    |- ( ph -> G e. ( LSubSp ` D ) )   &    |- ( ph -> G C_ { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem38 35148*	Lemma for lcfr 35153. Combine lcfrlem27 35137 and lcfrlem37 35147. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X =/= .0. )   &    |- ( ph -> Y =/= .0. )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- ( ph -> I e. B )   &    |- ( ph -> I =/= .0. )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem39 35149*	Lemma for lcfr 35153. Eliminate J. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X =/= .0. )   &    |- ( ph -> Y =/= .0. )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- ( ph -> I e. B )   &    |- ( ph -> I =/= .0. )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem40 35150*	Lemma for lcfr 35153. Eliminate B and I. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X =/= .0. )   &    |- ( ph -> Y =/= .0. )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem41 35151*	Lemma for lcfr 35153. Eliminate span condition. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X =/= .0. )   &    |- ( ph -> Y =/= .0. )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem42 35152*	Lemma for lcfr 35153. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfr 35153*	Reconstruction of a subspace from a dual subspace of functionals with closed kernels. Our proof was suggested by Mario Carneiro, 20-Feb-2015. (Contributed by NM, 5-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 ) }   &    |- Q = U_ g e. R ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> R e. T )   &    |- ( ph -> R C_ C )   =>    |- ( ph -> Q e. S )
Syntax	clcd 35154	Extend class notation with vector space of functionals with closed kernels.
class LCDual
Definition	df-lcdual 35155*	Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 35217. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 35193 using ( Base ` ( (LCDual ` K ) ` W ) ). (Contributed by NM, 13-Mar-2015.)
|- LCDual = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( (LDual ` ( ( DVecH ` k ) ` w ) ) ↾s { f e. (LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) } ) ) )
Theorem	lcdfval 35156*	Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   =>    |- ( K e. X -> (LCDual ` K ) = ( w e. H |-> ( (LDual ` ( ( DVecH ` K ) ` w ) ) ↾s { f e. (LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( (LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) } ) ) )
Theorem	lcdval 35157*	Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- C = ( (LCDual ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( K e. X /\ W e. H ) )   =>    |- ( ph -> C = ( D ↾s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) )
Theorem	lcdval2 35158*	Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- C = ( (LCDual ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( K e. X /\ W e. H ) )   &    |- B = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   =>    |- ( ph -> C = ( D ↾s B ) )
Theorem	lcdlvec 35159	The dual vector space of functionals with closed kernels is a left vector space. (Contributed by NM, 14-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> C e. LVec )
Theorem	lcdlmod 35160	The dual vector space of functionals with closed kernels is a left module. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> C e. LMod )
Theorem	lcdvbase 35161*	Vector base set of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- B = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> V = B )
Theorem	lcdvbasess 35162	The vector base set of the closed kernel dual space is a set of functionals. (Contributed by NM, 15-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> V C_ F )
Theorem	lcdvbaselfl 35163	A vector in the base set of the closed kernel dual space is a functional. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> X e. F )
Theorem	lcdvbasecl 35164	Closure of the value of a vector (functional) in the closed kernel dual space. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- E = ( Base ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. E )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( F ` X ) e. R )
Theorem	lcdvadd 35165	Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> .+b = .+ )
Theorem	lcdvaddval 35166	The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- .+ = ( +g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .+b = ( +g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> G e. D )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( F .+b G ) ` X ) = ( ( F ` X ) .+ ( G ` X ) ) )
Theorem	lcdsca 35167	The ring of scalars of the closed kernel dual space. (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- O = (oppr ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- R = (Scalar ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> R = O )
Theorem	lcdsbase 35168	Base set of scalar ring for the closed kernel dual of a vector space. (Contributed by NM, 18-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- L = ( Base ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- R = ( Base ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> R = L )
Theorem	lcdsadd 35169	Scalar addition for the closed kernel vector space dual. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- .+ = ( +g ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- .+b = ( +g ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> .+b = .+ )
Theorem	lcdsmul 35170	Scalar multiplication for the closed kernel vector space dual. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- L = ( Base ` F )   &    |- .x. = ( .r ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- .xb = ( .r ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. L )   &    |- ( ph -> Y e. L )   =>    |- ( ph -> ( X .xb Y ) = ( Y .x. X ) )
Theorem	lcdvs 35171	Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (LDual ` U )   &    |- .x. = ( .s ` D )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> .xb = .x. )
Theorem	lcdvsval 35172	Value of scalar product operation value for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- .x. = ( .r ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- .xb = ( .s ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. R )   &    |- ( ph -> G e. F )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( ( X .xb G ) ` A ) = ( ( G ` A ) .x. X ) )
Theorem	lcdvscl 35173	The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- .x. = ( .s ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. R )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( X .x. G ) e. V )
Theorem	lcdlssvscl 35174	Closure of scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- R = ( Base ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- .x. = ( .s ` C )   &    |- S = ( LSubSp ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> L e. S )   &    |- ( ph -> X e. R )   &    |- ( ph -> Y e. L )   =>    |- ( ph -> ( X .x. Y ) e. L )
Theorem	lcdvsass 35175	Associative law for scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- L = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- .xb = ( .s ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. L )   &    |- ( ph -> Y e. L )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( Y .x. X ) .xb G ) = ( X .xb ( Y .xb G ) ) )
Theorem	lcd0 35176	The zero scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- .0. = ( 0g ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- O = ( 0g ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> O = .0. )
Theorem	lcd1 35177	The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- .1. = ( 1r ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- I = ( 1r ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> I = .1. )
Theorem	lcdneg 35178	The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 11-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- M = ( invg ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- N = ( invg ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> N = M )
Theorem	lcd0v 35179	The zero functional in the set of functionals with closed kernels. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> O = ( V X. { .0. } ) )
Theorem	lcd0v2 35180	The zero functional in the set of functionals with closed kernels. (Contributed by NM, 27-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (LDual ` U )   &    |- .0. = ( 0g ` D )   &    |- C = ( (LCDual ` K ) ` W )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> O = .0. )
Theorem	lcd0vvalN 35181	Value of the zero functional at any vector. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- .0. = ( 0g ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( O ` X ) = .0. )
Theorem	lcd0vcl 35182	Closure of the zero functional in the set of functionals with closed kernels. (Contributed by NM, 15-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> O e. V )
Theorem	lcd0vs 35183	A scalar zero times a functional is the zero functional. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- .x. = ( .s ` C )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( .0. .x. G ) = O )
Theorem	lcdvs0N 35184	A scalar times the zero functional is the zero functional. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .x. = ( .s ` C )   &    |- .0. = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H )<