P. 368 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36701-36800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lcfl8a 36701*	Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) <-> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )
Theorem	lcfl8b 36702*	Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Y = ( 0g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. ( C \ { Y } ) )   =>    |- ( ph -> E. x e. ( V \ { .0. } ) ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) )
Theorem	lcfl9a 36703	Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( ._|_ ` { X } ) C_ ( L ` G ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
Theorem	lclkrlem1 36704*	The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .s ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> G e. C )   =>    |- ( ph -> ( X .x. G ) e. C )
Theorem	lclkrlem2a 36705	Lemma for lclkr 36731. Use lshpat 34254 to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )   &    |- ( ph -> -. X e. ( ._|_ ` { B } ) )   =>    |- ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )
Theorem	lclkrlem2b 36706	Lemma for lclkr 36731. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   =>    |- ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )
Theorem	lclkrlem2c 36707	Lemma for lclkr 36731. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- J = (LSHyp ` U )   =>    |- ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) e. J )
Theorem	lclkrlem2d 36708	Lemma for lclkr 36731. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- I = ( ( DIsoH ` K ) ` W )   =>    |- ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) e. ran I )
Theorem	lclkrlem2e 36709	Lemma for lclkr 36731. The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` E ) = ( L ` G ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2f 36710	Lemma for lclkr 36731. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( L ` E ) =/= ( L ` G ) )   &    |- ( ph -> ( L ` ( E .+ G ) ) e. J )   =>    |- ( ph -> ( ( ( L ` E ) i^i ( L ` G ) ) .(+) ( N ` { B } ) ) C_ ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2g 36711	Lemma for lclkr 36731. Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( L ` E ) =/= ( L ` G ) )   &    |- ( ph -> ( L ` ( E .+ G ) ) e. J )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2h 36712	Lemma for lclkr 36731. Eliminate the ( L ` ( E .+ G ) ) e. J hypothesis. (Contributed by NM, 16-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( L ` E ) =/= ( L ` G ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2i 36713	Lemma for lclkr 36731. Eliminate the ( L ` E ) =/= ( L ` G ) hypothesis. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2j 36714	Lemma for lclkr 36731. Kernel closure when Y is zero. (Contributed by NM, 18-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y = .0. )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2k 36715	Lemma for lclkr 36731. Kernel closure when X is zero. (Contributed by NM, 18-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X = .0. )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2l 36716	Lemma for lclkr 36731. Eliminate the X =/= .0., Y =/= .0. hypotheses. (Contributed by NM, 18-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- .0. = ( 0g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> B e. ( V \ { .0. } ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` B ) = Q )   &    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2m 36717	Lemma for lclkr 36731. Construct a vector B that makes the sum of functionals zero. Combine with B e. V to shorten overall proof. (Contributed by NM, 17-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> U e. LVec )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   =>    |- ( ph -> ( B e. V /\ ( ( E .+ G ) ` B ) = .0. ) )
Theorem	lclkrlem2n 36718	Lemma for lclkr 36731. (Contributed by NM, 12-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> U e. LVec )   &    |- ( ph -> ( ( E .+ G ) ` X ) = .0. )   &    |- ( ph -> ( ( E .+ G ) ` Y ) = .0. )   =>    |- ( ph -> ( N ` { X , Y } ) C_ ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2o 36719	Lemma for lclkr 36731. When B is nonzero, the vectors X and Y can't both belong to the hyperplane generated by B. (Contributed by NM, 17-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B =/= ( 0g ` U ) )   =>    |- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )
Theorem	lclkrlem2p 36720	Lemma for lclkr 36731. When B is zero, X and Y must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B = ( 0g ` U ) )   =>    |- ( ph -> ( ._|_ ` { Y } ) C_ ( ._|_ ` { X } ) )
Theorem	lclkrlem2q 36721	Lemma for lclkr 36731. The sum has a closed kernel when B is nonzero. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B =/= ( 0g ` U ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2r 36722	Lemma for lclkr 36731. When B is zero, i.e. when X and Y are colinear, the intersection of the kernels of E and G equal the kernel of G, so the kernels of G and the sum are comparable. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B = ( 0g ` U ) )   =>    |- ( ph -> ( L ` G ) C_ ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2s 36723	Lemma for lclkr 36731. Thus, the sum has a closed kernel when B is zero. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   &    |- ( ph -> B = ( 0g ` U ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2t 36724	Lemma for lclkr 36731. We eliminate all hypotheses with B here. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2u 36725	Lemma for lclkr 36731. lclkrlem2t 36724 with X and Y swapped. (Contributed by NM, 18-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` X ) =/= .0. )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2v 36726	Lemma for lclkr 36731. When the hypotheses of lclkrlem2u 36725 and lclkrlem2u 36725 are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid 36666, which requires the orthomodular law dihoml4 36575 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` X ) = .0. )   &    |- ( ph -> ( ( E .+ G ) ` Y ) = .0. )   =>    |- ( ph -> ( L ` ( E .+ G ) ) = V )
Theorem	lclkrlem2w 36727	Lemma for lclkr 36731. This is the same as lclkrlem2u 36725 and lclkrlem2u 36725 with the inequality hypotheses negated. When the sum of two functionals is zero at each generating vector, the kernel is the vector space and therefore closed. (Contributed by NM, 16-Jan-2015.)
|- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .X. = ( .r ` S )   &    |- .0. = ( 0g ` S )   &    |- I = ( invr ` S )   &    |- .- = ( -g ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- N = ( LSpan ` U )   &    |- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   &    |- ( ph -> ( ( E .+ G ) ` X ) = .0. )   &    |- ( ph -> ( ( E .+ G ) ` Y ) = .0. )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2x 36728	Lemma for lclkr 36731. Eliminate by cases the hypotheses of lclkrlem2u 36725, lclkrlem2u 36725 and lclkrlem2w 36727. (Contributed by NM, 18-Jan-2015.)
|- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )   &    |- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2y 36729	Lemma for lclkr 36731. Restate the hypotheses for E and G to say their kernels are closed, in order to eliminate the generating vectors X and Y. (Contributed by NM, 18-Jan-2015.)
|- L = (LKer ` U )   &    |- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> E e. F )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) )   &    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )   =>    |- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
Theorem	lclkrlem2 36730*	The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 36705 through lclkrlem2y 36729 are used for the proof. Here we express lclkrlem2y 36729 in terms of membership in the set C of functionals with closed kernels. (Contributed by NM, 18-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> E e. C )   &    |- ( ph -> G e. C )   =>    |- ( ph -> ( E .+ G ) e. C )
Theorem	lclkr 36731*	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 36732*	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 36733*	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 36734*	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 36735*	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 36736*	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 36737*	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 36731 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 36731 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 36738*	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 36826. (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 36739*	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 36740	Lemma for lcfr 36783. 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 36741	Lemma for lcfr 36783. (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 36742	Lemma for lcfr 36783. (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 36743*	Lemma for lcfr 36783. (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 36744*	Lemma for lcfr 36783. 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 36745*	Lemma for lcfr 36783. 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 36746*	Lemma for lcfr 36783. 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 36747*	Lemma for lcf1o 36749 and lcfr 36783. (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 36748*	Lemma for lcf1o 36749. (This part has undesirable $d's on J and ph that we remove in lcf1o 36749.) 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 36749*	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 36750*	Lemma for lcfr 36783. (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 36751*	Lemma for lcfr 36783. (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 36752*	Lemma for lcfr 36783. (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 36753*	Lemma for lcfr 36783. (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 36754*	Lemma for lcfr 36783. (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 36755*	Lemma for lcfr 36783. (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 36756*	Lemma for lcfr 36783. (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 36757	Lemma for lcfr 36783. 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 36758	Lemma for lcfr 36783. (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 36759	Lemma for lcfr 36783. (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 36760	Lemma for lcfr 36783. (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 36761	Lemma for lcfr 36783. (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 36762	Lemma for lcfr 36783. (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 36763	Lemma for lcfr 36783. 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 36764*	Lemma for lcfr 36783. (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 36765*	Lemma for lcfr 36783. Special case of lcfrlem35 36775 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 36766*	Lemma for lcfr 36783. Special case of lcfrlem36 36776 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 36767*	Lemma for lcfr 36783. Special case of lcfrlem37 36777 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 36768*	Lemma for lcfr 36783. 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 36769*	Lemma for lcfr 36783. (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 )