P. 371 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37001-37100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lcfls1lem 37001*	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 37002*	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 37003*	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 37004*	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 37005*	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 37006*	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 37000 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 37000 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 37007*	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 37095. (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 37008*	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 37009	Lemma for lcfr 37052. 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 37010	Lemma for lcfr 37052. (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 37011	Lemma for lcfr 37052. (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 37012*	Lemma for lcfr 37052. (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 37013*	Lemma for lcfr 37052. 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 37014*	Lemma for lcfr 37052. 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 37015*	Lemma for lcfr 37052. 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 37016*	Lemma for lcf1o 37018 and lcfr 37052. (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 37017*	Lemma for lcf1o 37018. (This part has undesirable $d's on J and ph that we remove in lcf1o 37018.) 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 37018*	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 37019*	Lemma for lcfr 37052. (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 37020*	Lemma for lcfr 37052. (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 37021*	Lemma for lcfr 37052. (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 37022*	Lemma for lcfr 37052. (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 37023*	Lemma for lcfr 37052. (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 37024*	Lemma for lcfr 37052. (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 37025*	Lemma for lcfr 37052. (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 37026	Lemma for lcfr 37052. 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 37027	Lemma for lcfr 37052. (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 37028	Lemma for lcfr 37052. (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 37029	Lemma for lcfr 37052. (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 37030	Lemma for lcfr 37052. (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 37031	Lemma for lcfr 37052. (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 37032	Lemma for lcfr 37052. 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 37033*	Lemma for lcfr 37052. (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 37034*	Lemma for lcfr 37052. Special case of lcfrlem35 37044 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 37035*	Lemma for lcfr 37052. Special case of lcfrlem36 37045 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 37036*	Lemma for lcfr 37052. Special case of lcfrlem37 37046 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 37037*	Lemma for lcfr 37052. 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 37038*	Lemma for lcfr 37052. (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 37039*	Lemma for lcfr 37052. (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 37040*	Lemma for lcfr 37052. (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 37041*	Lemma for lcfr 37052. (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 37042*	Lemma for lcfr 37052. (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 37043*	Lemma for lcfr 37052. (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 37044*	Lemma for lcfr 37052. (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 37045*	Lemma for lcfr 37052. (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 37046*	Lemma for lcfr 37052. (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 37047*	Lemma for lcfr 37052. Combine lcfrlem27 37036 and lcfrlem37 37046. (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 37048*	Lemma for lcfr 37052. 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 37049*	Lemma for lcfr 37052. 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 37050*	Lemma for lcfr 37052. 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 37051*	Lemma for lcfr 37052. 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 37052*	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 37053	Extend class notation with vector space of functionals with closed kernels.
class LCDual
Definition	df-lcdual 37054*	Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 37116. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 37092 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 37055*	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 37056*	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 37057*	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 37058	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 37059	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 37060*	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 37061	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 37062	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 37063	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 37064	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 37065	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 37066	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 37067	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 37068	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 37069	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 37070	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 37071	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 37072	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 37073	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 37074	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 37075	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 37076	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 37077	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 37078	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 37079	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 37080	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 37081	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 37082	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 37083	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 ) )   &    |- ( ph -> X e. R )   =>    |- ( ph -> ( X .x. .0. ) = .0. )
Theorem	lcdvsub 37084	The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` U )   &    |- N = ( invg ` S )   &    |- .1. = ( 1r ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- .+ = ( +g ` C )   &    |- .x. = ( .s ` C )   &    |- .- = ( -g ` C )   &    |- (