P. 356 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35501-35600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lcfl6lem 35501*	Lemma for lcfl6 35503. A functional G (whose kernel is closed by dochsnkr 35475) is comletely determined by a vector X in the orthocomplement in its kernel at which the functional value is 1. Note that the \ { .0. } in the X hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- .1. = ( 1r ` S )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )   &    |- ( ph -> ( G ` X ) = .1. )   =>    |- ( ph -> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) )
Theorem	lcfl7lem 35502*	Lemma for lcfl7N 35504. If two functionals G and J are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )   &    |- J = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { Y } ) v = ( w .+ ( k .x. Y ) ) ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G = J )   =>    |- ( ph -> X = Y )
Theorem	lcfl6 35503*	Property of a functional with a closed kernel. Note that ( L ` G ) = V means the functional is zero by lkr0f 33097. (Contributed by NM, 3-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( ( L ` G ) = V \/ E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) )
Theorem	lcfl7N 35504*	Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that ( L ` G ) = V means the functional is zero by lkr0f 33097. (Contributed by NM, 4-Jan-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> ( ( L ` G ) = V \/ E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) )
Theorem	lcfl8 35505*	Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( G e. C <-> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )
Theorem	lcfl8a 35506*	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 35507*	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 35508	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 35509*	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 35510	Lemma for lclkr 35536. Use lshpat 33059 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 35511	Lemma for lclkr 35536. (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 35512	Lemma for lclkr 35536. (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 35513	Lemma for lclkr 35536. (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 35514	Lemma for lclkr 35536. 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 35515	Lemma for lclkr 35536. 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 35516	Lemma for lclkr 35536. 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 35517	Lemma for lclkr 35536. 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 35518	Lemma for lclkr 35536. 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 35519	Lemma for lclkr 35536. 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 35520	Lemma for lclkr 35536. 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 35521	Lemma for lclkr 35536. 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 35522	Lemma for lclkr 35536. 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 35523	Lemma for lclkr 35536. (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 35524	Lemma for lclkr 35536. 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 35525	Lemma for lclkr 35536. 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 35526	Lemma for lclkr 35536. 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 35527	Lemma for lclkr 35536. 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 35528	Lemma for lclkr 35536. 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 35529	Lemma for lclkr 35536. 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 35530	Lemma for lclkr 35536. lclkrlem2t 35529 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 35531	Lemma for lclkr 35536. When the hypotheses of lclkrlem2u 35530 and lclkrlem2u 35530 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 35471, which requires the orthomodular law dihoml4 35380 (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 35532	Lemma for lclkr 35536. This is the same as lclkrlem2u 35530 and lclkrlem2u 35530 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 35533	Lemma for lclkr 35536. Eliminate by cases the hypotheses of lclkrlem2u 35530, lclkrlem2u 35530 and lclkrlem2w 35532. (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 35534	Lemma for lclkr 35536. 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 35535*	The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 35510 through lclkrlem2y 35534 are used for the proof. Here we express lclkrlem2y 35534 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 35536*	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 35537*	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 35538*	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 35539*	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 35540*	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 35541*	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 35542*	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 35536 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 35536 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 35543*	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 35631. (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 35544*	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 35545	Lemma for lcfr 35588. 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 35546	Lemma for lcfr 35588. (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 35547	Lemma for lcfr 35588. (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 35548*	Lemma for lcfr 35588. (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 35549*	Lemma for lcfr 35588. 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 35550*	Lemma for lcfr 35588. 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 35551*	Lemma for lcfr 35588. 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 35552*	Lemma for lcf1o 35554 and lcfr 35588. (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 35553*	Lemma for lcf1o 35554. (This part has undesirable $d's on J and ph that we remove in lcf1o 35554.) 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 35554*	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 35555*	Lemma for lcfr 35588. (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 35556*	Lemma for lcfr 35588. (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 35557*	Lemma for lcfr 35588. (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 35558*	Lemma for lcfr 35588. (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 35559*	Lemma for lcfr 35588. (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 35560*	Lemma for lcfr 35588. (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 35561*	Lemma for lcfr 35588. (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 35562	Lemma for lcfr 35588. 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 35563	Lemma for lcfr 35588. (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 35564	Lemma for lcfr 35588. (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 35565	Lemma for lcfr 35588. (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 35566	Lemma for lcfr 35588. (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 35567	Lemma for lcfr 35588. (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 35568	Lemma for lcfr 35588. 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 35569*	Lemma for lcfr 35588. (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 35570*	Lemma for lcfr 35588. Special case of lcfrlem35 35580 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 35571*	Lemma for lcfr 35588. Special case of lcfrlem36 35581 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. )   =>    |- (