P. 353 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35201-35300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lcfrlem20 35201	Lemma for lcfr 35224. (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 35202	Lemma for lcfr 35224. (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 35203	Lemma for lcfr 35224. (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 35204	Lemma for lcfr 35224. 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 35205*	Lemma for lcfr 35224. (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 35206*	Lemma for lcfr 35224. Special case of lcfrlem35 35216 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 35207*	Lemma for lcfr 35224. Special case of lcfrlem36 35217 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 35208*	Lemma for lcfr 35224. Special case of lcfrlem37 35218 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 35209*	Lemma for lcfr 35224. 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 35210*	Lemma for lcfr 35224. (Contributed by NM, 9-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   =>    |- ( ph -> ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) e. R )
Theorem	lcfrlem30 35211*	Lemma for lcfr 35224. (Contributed by NM, 6-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   =>    |- ( ph -> C e. (LFnl ` U ) )
Theorem	lcfrlem31 35212*	Lemma for lcfr 35224. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   &    |- ( ph -> ( ( J ` X ) ` I ) =/= Q )   &    |- ( ph -> C = ( 0g ` D ) )   =>    |- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )
Theorem	lcfrlem32 35213*	Lemma for lcfr 35224. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   &    |- ( ph -> ( ( J ` X ) ` I ) =/= Q )   =>    |- ( ph -> C =/= ( 0g ` D ) )
Theorem	lcfrlem33 35214*	Lemma for lcfr 35224. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   &    |- ( ph -> ( ( J ` X ) ` I ) = Q )   =>    |- ( ph -> C =/= ( 0g ` D ) )
Theorem	lcfrlem34 35215*	Lemma for lcfr 35224. (Contributed by NM, 10-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   =>    |- ( ph -> C =/= ( 0g ` D ) )
Theorem	lcfrlem35 35216*	Lemma for lcfr 35224. (Contributed by NM, 2-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   =>    |- ( ph -> ( ._|_ ` { ( X .+ Y ) } ) = ( L ` C ) )
Theorem	lcfrlem36 35217*	Lemma for lcfr 35224. (Contributed by NM, 6-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   =>    |- ( ph -> ( X .+ Y ) e. ( ._|_ ` ( L ` C ) ) )
Theorem	lcfrlem37 35218*	Lemma for lcfr 35224. (Contributed by NM, 8-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- A = (LSAtoms ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- Q = ( 0g ` S )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   &    |- ( ph -> I e. B )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )   &    |- F = ( invr ` S )   &    |- .- = ( -g ` D )   &    |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )   &    |- ( ph -> G e. ( LSubSp ` D ) )   &    |- ( ph -> G C_ { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem38 35219*	Lemma for lcfr 35224. Combine lcfrlem27 35208 and lcfrlem37 35218. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X =/= .0. )   &    |- ( ph -> Y =/= .0. )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- ( ph -> I e. B )   &    |- ( ph -> I =/= .0. )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem39 35220*	Lemma for lcfr 35224. Eliminate J. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X =/= .0. )   &    |- ( ph -> Y =/= .0. )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )   &    |- ( ph -> I e. B )   &    |- ( ph -> I =/= .0. )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem40 35221*	Lemma for lcfr 35224. Eliminate B and I. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X =/= .0. )   &    |- ( ph -> Y =/= .0. )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem41 35222*	Lemma for lcfr 35224. Eliminate span condition. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X =/= .0. )   &    |- ( ph -> Y =/= .0. )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfrlem42 35223*	Lemma for lcfr 35224. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( LSubSp ` D )   &    |- C = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- E = U_ g e. G ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. Q )   &    |- ( ph -> G C_ C )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y e. E )   =>    |- ( ph -> ( X .+ Y ) e. E )
Theorem	lcfr 35224*	Reconstruction of a subspace from a dual subspace of functionals with closed kernels. Our proof was suggested by Mario Carneiro, 20-Feb-2015. (Contributed by NM, 5-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- Q = U_ g e. R ( ._|_ ` ( L ` g ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> R e. T )   &    |- ( ph -> R C_ C )   =>    |- ( ph -> Q e. S )
Syntax	clcd 35225	Extend class notation with vector space of functionals with closed kernels.
class LCDual
Definition	df-lcdual 35226*	Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 35288. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 35264 using ( Base ` ( (LCDual ` K ) ` W ) ). (Contributed by NM, 13-Mar-2015.)
|- LCDual = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( (LDual ` ( ( DVecH ` k ) ` w ) ) ↾s { f e. (LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) } ) ) )
Theorem	lcdfval 35227*	Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   =>    |- ( K e. X -> (LCDual ` K ) = ( w e. H |-> ( (LDual ` ( ( DVecH ` K ) ` w ) ) ↾s { f e. (LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( (LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) } ) ) )
Theorem	lcdval 35228*	Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- C = ( (LCDual ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( K e. X /\ W e. H ) )   =>    |- ( ph -> C = ( D ↾s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) )
Theorem	lcdval2 35229*	Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- C = ( (LCDual ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- ( ph -> ( K e. X /\ W e. H ) )   &    |- B = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   =>    |- ( ph -> C = ( D ↾s B ) )
Theorem	lcdlvec 35230	The dual vector space of functionals with closed kernels is a left vector space. (Contributed by NM, 14-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> C e. LVec )
Theorem	lcdlmod 35231	The dual vector space of functionals with closed kernels is a left module. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> C e. LMod )
Theorem	lcdvbase 35232*	Vector base set of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- ._|_ = ( ( ocH ` K ) ` W )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- B = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> V = B )
Theorem	lcdvbasess 35233	The vector base set of the closed kernel dual space is a set of functionals. (Contributed by NM, 15-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> V C_ F )
Theorem	lcdvbaselfl 35234	A vector in the base set of the closed kernel dual space is a functional. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> X e. F )
Theorem	lcdvbasecl 35235	Closure of the value of a vector (functional) in the closed kernel dual space. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- E = ( Base ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. E )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( F ` X ) e. R )
Theorem	lcdvadd 35236	Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (LDual ` U )   &    |- .+ = ( +g ` D )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> .+b = .+ )
Theorem	lcdvaddval 35237	The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- .+ = ( +g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .+b = ( +g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> G e. D )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( F .+b G ) ` X ) = ( ( F ` X ) .+ ( G ` X ) ) )
Theorem	lcdsca 35238	The ring of scalars of the closed kernel dual space. (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- O = (oppr ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- R = (Scalar ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> R = O )
Theorem	lcdsbase 35239	Base set of scalar ring for the closed kernel dual of a vector space. (Contributed by NM, 18-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- L = ( Base ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- R = ( Base ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> R = L )
Theorem	lcdsadd 35240	Scalar addition for the closed kernel vector space dual. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- .+ = ( +g ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- .+b = ( +g ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> .+b = .+ )
Theorem	lcdsmul 35241	Scalar multiplication for the closed kernel vector space dual. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- L = ( Base ` F )   &    |- .x. = ( .r ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- .xb = ( .r ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. L )   &    |- ( ph -> Y e. L )   =>    |- ( ph -> ( X .xb Y ) = ( Y .x. X ) )
Theorem	lcdvs 35242	Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (LDual ` U )   &    |- .x. = ( .s ` D )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> .xb = .x. )
Theorem	lcdvsval 35243	Value of scalar product operation value for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- .x. = ( .r ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- .xb = ( .s ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. R )   &    |- ( ph -> G e. F )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( ( X .xb G ) ` A ) = ( ( G ` A ) .x. X ) )
Theorem	lcdvscl 35244	The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- .x. = ( .s ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. R )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( X .x. G ) e. V )
Theorem	lcdlssvscl 35245	Closure of scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- R = ( Base ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- .x. = ( .s ` C )   &    |- S = ( LSubSp ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> L e. S )   &    |- ( ph -> X e. R )   &    |- ( ph -> Y e. L )   =>    |- ( ph -> ( X .x. Y ) e. L )
Theorem	lcdvsass 35246	Associative law for scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- L = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- .xb = ( .s ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. L )   &    |- ( ph -> Y e. L )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( Y .x. X ) .xb G ) = ( X .xb ( Y .xb G ) ) )
Theorem	lcd0 35247	The zero scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- .0. = ( 0g ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- O = ( 0g ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> O = .0. )
Theorem	lcd1 35248	The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- .1. = ( 1r ` F )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- I = ( 1r ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> I = .1. )
Theorem	lcdneg 35249	The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 11-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- M = ( invg ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = (Scalar ` C )   &    |- N = ( invg ` S )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> N = M )
Theorem	lcd0v 35250	The zero functional in the set of functionals with closed kernels. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> O = ( V X. { .0. } ) )
Theorem	lcd0v2 35251	The zero functional in the set of functionals with closed kernels. (Contributed by NM, 27-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (LDual ` U )   &    |- .0. = ( 0g ` D )   &    |- C = ( (LCDual ` K ) ` W )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> O = .0. )
Theorem	lcd0vvalN 35252	Value of the zero functional at any vector. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = (Scalar ` U )   &    |- .0. = ( 0g ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( O ` X ) = .0. )
Theorem	lcd0vcl 35253	Closure of the zero functional in the set of functionals with closed kernels. (Contributed by NM, 15-Mar-2015.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> O e. V )
Theorem	lcd0vs 35254	A scalar zero times a functional is the zero functional. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- .x. = ( .s ` C )   &    |- O = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( .0. .x. G ) = O )
Theorem	lcdvs0N 35255	A scalar times the zero functional is the zero functional. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .x. = ( .s ` C )   &    |- .0. = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. R )   =>    |- ( ph -> ( X .x. .0. ) = .0. )
Theorem	lcdvsub 35256	The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` U )   &    |- N = ( invg ` S )   &    |- .1. = ( 1r ` S )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- .+ = ( +g ` C )   &    |- .x. = ( .s ` C )   &    |- .- = ( -g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( F .- G ) = ( F .+ ( ( N ` .1. ) .x. G ) ) )
Theorem	lcdvsubval 35257	The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 11-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- S = ( -g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .- = ( -g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> G e. D )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( F .- G ) ` X ) = ( ( F ` X ) S ( G ` X ) ) )
Theorem	lcdlss 35258*	Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = ( LSubSp ` C )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- B = { f e. F | ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> S = ( T i^i ~P B ) )
Theorem	lcdlss2N 35259	Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- S = ( LSubSp ` C )   &    |- V = ( Base ` C )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> S = ( T i^i ~P V ) )
Theorem	lcdlsp 35260	Span in the set of functionals with closed kernels. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (LDual ` U )   &    |- M = ( LSpan ` D )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- N = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G C_ F )   =>    |- ( ph -> ( N ` G ) = ( M ` G ) )
Theorem	lcdlkreqN 35261	Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- L = (LKer ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .0. = ( 0g ` C )   &    |- N = ( LSpan ` C )   &    |- V = ( Base ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> I e. V )   &    |- ( ph -> G e. ( N ` { I } ) )   &    |- ( ph -> G =/= .0. )   =>    |- ( ph -> ( L ` G ) = ( L ` I ) )
Theorem	lcdlkreq2N 35262	Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` S )   &    |- L = (LKer ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- V = ( Base ` C )   &    |- .x. = ( .s ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> A e. ( R \ { .0. } ) )   &    |- ( ph -> I e. V )   &    |- ( ph -> G = ( A .x. I ) )   =>    |- ( ph -> ( L ` G ) = ( L ` I ) )
Syntax	cmpd 35263	Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels.
class mapd
Definition	df-mapd 35264*	Extend class notation with a one-to-one onto (mapd1o 35287), order-preserving (mapdord 35277) map, called a projectivity (definition of projectivity in [Baer] p. 40), from subspaces of vector space H to those subspaces of the dual space having functionals with closed kernels. (Contributed by NM, 25-Jan-2015.)
|- mapd = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( s e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) |-> { f e. (LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) /\ ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) C_ s ) } ) ) )
Theorem	mapdffval 35265*	Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.)
|- H = ( LHyp ` K )   =>    |- ( K e. X -> (mapd ` K ) = ( w e. H |-> ( s e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) |-> { f e. (LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( (LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) /\ ( ( ( ocH ` K ) ` w ) ` ( (LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) } ) ) )
Theorem	mapdfval 35266*	Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   =>    |- ( ( K e. X /\ W e. H ) -> M = ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) )
Theorem	mapdval 35267*	Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. X /\ W e. H ) )   &    |- ( ph -> T e. S )   =>    |- ( ph -> ( M ` T ) = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } )
Theorem	mapdvalc 35268*	Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. X /\ W e. H ) )   &    |- ( ph -> T e. S )   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   =>    |- ( ph -> ( M ` T ) = { f e. C | ( O ` ( L ` f ) ) C_ T } )
Theorem	mapdval2N 35269*	Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. S )   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   =>    |- ( ph -> ( M ` T ) = { f e. C | E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) } )
Theorem	mapdval3N 35270*	Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. S )   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   =>    |- ( ph -> ( M ` T ) = U_ v e. T { f e. C | ( O ` ( L ` f ) ) = ( N ` { v } ) } )
Theorem	mapdval4N 35271*	Value of projectivity from vector space H to dual space. TODO: 1. This is shorter than others - make it the official def? (but is not as obvious that it is C_ C) 2. The unneeded direction of lcfl8a 35142 has awkward E.- add another thm with only one direction of it? 3. Swap O ` { v } and L ` f? (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. S )   =>    |- ( ph -> ( M ` T ) = { f e. F | E. v e. T ( O ` { v } ) = ( L ` f ) } )
Theorem	mapdval5N 35272*	Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. S )   =>    |- ( ph -> ( M ` T ) = U_ v e. T { f e. F | ( O ` { v } ) = ( L ` f ) } )
Theorem	mapdordlem1a 35273*	Lemma for mapdord 35277. (Contributed by NM, 27-Jan-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- Y = (LSHyp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- T = { g e. F | ( O ` ( O ` ( L ` g ) ) ) e. Y }   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ( J e. T <-> ( J e. C /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) )
Theorem	mapdordlem1bN 35274*	Lemma for mapdord 35277. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.)
|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   =>    |- ( J e. C <-> ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) ) )
Theorem	mapdordlem1 35275*	Lemma for mapdord 35277. (Contributed by NM, 27-Jan-2015.)
|- T = { g e. F | ( O ` ( O ` ( L ` g ) ) ) e. Y }   =>    |- ( J e. T <-> ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) )
Theorem	mapdordlem2 35276*	Lemma for mapdord 35277. Ordering property of projectivity M. TODO: This was proved using some hacked-up older proofs. Maybe simplify; get rid of the T hypothesis. (Contributed by NM, 27-Jan-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   &    |- O = ( ( ocH ` K ) ` W )   &    |- A = (LSAtoms ` U )   &    |- F = (LFnl ` U )   &    |- J = (LSHyp ` U )   &    |- L = (LKer ` U )   &    |- T = { g e. F | ( O ` ( O ` ( L ` g ) ) ) e. J }   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   =>    |- ( ph -> ( ( M ` X ) C_ ( M ` Y ) <-> X C_ Y ) )
Theorem	mapdord 35277	Ordering property of the map defined by df-mapd 35264. Property (b) of [Baer] p. 40. (Contributed by NM, 27-Jan-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> ( ( M ` X ) C_ ( M ` Y ) <-> X C_ Y ) )
Theorem	mapd11 35278	The map defined by df-mapd 35264 is one-to-one. Property (c) of [Baer] p. 40. (Contributed by NM, 12-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> ( ( M ` X ) = ( M ` Y ) <-> X = Y ) )
Theorem	mapddlssN 35279	The mapping of a subspace of vector space H to the dual space is a subspace of the dual space. TODO: Make this obsolete, use mapdcl2 35295 instead. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> R e. S )   =>    |- ( ph -> ( M ` R ) e. T )
Theorem	mapdsn 35280*	Value of the map defined by df-mapd 35264 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( M ` ( N ` { X } ) ) = { f e. F | ( O ` { X } ) C_ ( L ` f ) } )
Theorem	mapdsn2 35281*	Value of the map defined by df-mapd 35264 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( L ` G ) = ( O ` { X } ) )   =>    |- ( ph -> ( M ` ( N ` { X } ) ) = { f e. F | ( L ` G ) C_ ( L ` f ) } )
Theorem	mapdsn3 35282	Value of the map defined by df-mapd 35264 at the span of a singleton. (Contributed by NM, 17-Feb-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- P = ( LSpan ` D )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( L ` G ) = ( O ` { X } ) )   =>    |- ( ph -> ( M ` ( N ` { X } ) ) = ( P ` { G } ) )
Theorem	mapd1dim2lem1N 35283*	Value of the map defined by df-mapd 35264 at an atom. (Contributed by NM, 10-Feb-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- A = (LSAtoms ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( M ` Q ) = { f e. F | E. v e. Q ( O ` { v } ) = ( L ` f ) } )
Theorem	mapdrvallem2 35284*	Lemma for mapdrval 35286. TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> R e. T )   &    |- ( ph -> R C_ C )   &    |- Q = U_ h e. R ( O ` ( L ` h ) )   &    |- V = ( Base ` U )   &    |- A = (LSAtoms ` U )   &    |- N = ( LSpan ` U )   &    |- .0. = ( 0g ` U )   &    |- Y = ( 0g ` D )   =>    |- ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ Q } C_ R )
Theorem	mapdrvallem3 35285*	Lemma for mapdrval 35286. (Contributed by NM, 2-Feb-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> R e. T )   &    |- ( ph -> R C_ C )   &    |- Q = U_ h e. R ( O ` ( L ` h ) )   &    |- V = ( Base ` U )   &    |- A = (LSAtoms ` U )   &    |- N = ( LSpan ` U )   &    |- .0. = ( 0g ` U )   &    |- Y = ( 0g ` D )   =>    |- ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ Q } = R )
Theorem	mapdrval 35286*	Given a dual subspace R (of functionals with closed kernels), reconstruct the subspace Q that maps to it. (Contributed by NM, 12-Mar-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> R e. T )   &    |- ( ph -> R C_ C )   &    |- Q = U_ h e. R ( O ` ( L ` h ) )   =>    |- ( ph -> ( M ` Q ) = R )
Theorem	mapd1o 35287*	The map defined by df-mapd 35264 is one-to-one and onto the set of dual subspaces of functionals with closed kernels. This shows M satisfies part of the definition of projectivity of [Baer] p. 40. TODO: change theorems leading to this (lcfr 35224, mapdrval 35286, lclkrs 35178, lclkr 35172,...) to use T i^i ~P C? TODO: maybe get rid of $d's for g vs. K U W,. propagate to mapdrn 35288 and any others. (Contributed by NM, 12-Mar-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> M : S -1-1-onto-> ( T i^i ~P C ) )
Theorem	mapdrn 35288*	Range of the map defined by df-mapd 35264. (Contributed by NM, 12-Mar-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- T = ( LSubSp ` D )   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ran M = ( T i^i ~P C ) )
Theorem	mapdunirnN 35289*	Union of the range of the map defined by df-mapd 35264. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> U. ran M = C )
Theorem	mapdrn2 35290	Range of the map defined by df-mapd 35264. TODO: this seems to be needed a lot in hdmaprnlem3eN 35500 etc. Would it be better to change df-mapd 35264 theorems to use LSubSp ` C instead of ran M? (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- C = ( (LCDual ` K ) ` W )   &    |- T = ( LSubSp ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ran M = T )
Theorem	mapdcnvcl 35291	Closure of the converse of the map defined by df-mapd 35264. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ran M )   =>    |- ( ph -> ( `' M ` X ) e. S )
Theorem	mapdcl 35292	Closure the value of the map defined by df-mapd 35264. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   =>    |- ( ph -> ( M ` X ) e. ran M )
Theorem	mapdcnvid1N 35293	Converse of the value of the map defined by df-mapd 35264. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   =>    |- ( ph -> ( `' M ` ( M ` X ) ) = X )
Theorem	mapdsord 35294	Strong ordering property of themap defined by df-mapd 35264. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> ( ( M ` X ) C. ( M ` Y ) <-> X C. Y ) )
Theorem	mapdcl2 35295	The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- T = ( LSubSp ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> R e. S )   =>    |- ( ph -> ( M ` R ) e. T )
Theorem	mapdcnvid2 35296	Value of the converse of the map defined by df-mapd 35264. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ran M )   =>    |- ( ph -> ( M ` ( `' M ` X ) ) = X )
Theorem	mapdcnvordN 35297	Ordering property of the converse of the map defined by df-mapd 35264. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ran M )   &    |- ( ph -> Y e. ran M )   =>    |- ( ph -> ( ( `' M ` X ) C_ ( `' M ` Y ) <-> X C_ Y ) )
Theorem	mapdcnv11N 35298	The converse of the map defined by df-mapd 35264 is one-to-one. (Contributed by NM, 13