P. 371 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	baerlem5blem2 37001	Lemma for baerlem5b 37004. (Contributed by NM, 13-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- R = (Scalar ` W )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- L = ( -g ` R )   &    |- Q = ( 0g ` R )   &    |- I = ( invg ` R )   =>    |- ( ph -> ( N ` { ( Y .+ Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) )
Theorem	baerlem3 37002	An equality that holds when X, Y, Z are independent (non-colinear) vectors. Part (3) in [Baer] p. 45. TODO fix ref. (Contributed by NM, 9-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   =>    |- ( ph -> ( N ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { ( X .- Z ) } ) ) ) )
Theorem	baerlem5a 37003	An equality that holds when X, Y, Z are independent (non-colinear) vectors. First equation of part (5) in [Baer] p. 46. (Contributed by NM, 10-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   =>    |- ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) )
Theorem	baerlem5b 37004	An equality that holds when X, Y, Z are independent (non-colinear) vectors. Second equation of part (5) in [Baer] p. 46. (Contributed by NM, 13-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   =>    |- ( ph -> ( N ` { ( Y .+ Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) )
Theorem	baerlem5amN 37005	An equality that holds when X, Y, Z are independent (non-colinear) vectors. Subtraction version of first equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 37007 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   =>    |- ( ph -> ( N ` { ( X .- ( Y .- Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .+ Z ) } ) .(+) ( N ` { Y } ) ) ) )
Theorem	baerlem5bmN 37006	An equality that holds when X, Y, Z are independent (non-colinear) vectors. Subtraction version of second equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 37007 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   =>    |- ( ph -> ( N ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) ) )
Theorem	baerlem5abmN 37007	An equality that holds when X, Y, Z are independent (non-colinear) vectors. Subtraction versions of first and second equations of part (5) in [Baer] p. 46, conjoined to share commonality in their proofs. TODO: Delete if not be needed. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   =>    |- ( ph -> ( ( N ` { ( X .- ( Y .- Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .+ Z ) } ) .(+) ( N ` { Y } ) ) ) /\ ( N ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) ) ) )
Theorem	mapdindp0 37008	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   &    |- ( ph -> ( Y .+ Z ) =/= .0. )   =>    |- ( ph -> ( N ` { ( Y .+ Z ) } ) = ( N ` { Y } ) )
Theorem	mapdindp1 37009	Vector independence lemma. (Contributed by NM, 1-May-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )
Theorem	mapdindp2 37010	Vector independence lemma. (Contributed by NM, 1-May-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> -. w e. ( N ` { X , ( Y .+ Z ) } ) )
Theorem	mapdindp3 37011	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> ( N ` { X } ) =/= ( N ` { ( w .+ Y ) } ) )
Theorem	mapdindp4 37012	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> -. Z e. ( N ` { X , ( w .+ Y ) } ) )
Theorem	mapdhval 37013*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> X e. A )   &    |- ( ph -> F e. B )   &    |- ( ph -> Y e. E )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )
Theorem	mapdhval0 37014*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X e. A )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( I ` <. X , F , .0. >. ) = Q )
Theorem	mapdhval2 37015*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> X e. A )   &    |- ( ph -> F e. B )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )
Theorem	mapdhcl 37016*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. V )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) e. D )
Theorem	mapdheq 37017*	Lemmma for ~? mapdh . The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 4-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( ( I ` <. X , F , Y >. ) = G <-> ( ( M ` ( N ` { Y } ) ) = ( J ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R G ) } ) ) ) )
Theorem	mapdheq2 37018*	Lemmma for ~? mapdh . One direction of part (2) in [Baer] p. 45. (Contributed by NM, 4-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( ( I ` <. X , F , Y >. ) = G -> ( I ` <. Y , G , X >. ) = F ) )
Theorem	mapdheq2biN 37019*	Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 37018 seems to require an additional hypothesis not mentioned in Baer. TODO fix ref. TODO: We probably don't need this; delete if never used. (Contributed by NM, 4-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )   =>    |- ( ph -> ( ( I ` <. X , F , Y >. ) = G <-> ( I ` <. Y , G , X >. ) = F ) )
Theorem	mapdheq4lem 37020*	Lemma for mapdheq4 37021. Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( M ` ( N ` { ( Y .- Z ) } ) ) = ( J ` { ( G R E ) } ) )
Theorem	mapdheq4 37021*	Lemma for ~? mapdh . Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( I ` <. Y , G , Z >. ) = E )
Theorem	mapdh6lem1N 37022*	Lemma for mapdh6N 37036. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( M ` ( N ` { ( X .- ( Y .+ Z ) ) } ) ) = ( J ` { ( F R ( G .+b E ) ) } ) )
Theorem	mapdh6lem2N 37023*	Lemma for mapdh6N 37036. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( M ` ( N ` { ( Y .+ Z ) } ) ) = ( J ` { ( G .+b E ) } ) )
Theorem	mapdh6aN 37024*	Lemma for mapdh6N 37036. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6b0N 37025*	Lemmma for mapdh6N 37036. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> ( ( N ` { X } ) i^i ( N ` { Y , Z } ) ) = { .0. } )   =>    |- ( ph -> -. X e. ( N ` { Y , Z } ) )
Theorem	mapdh6bN 37026*	Lemmma for mapdh6N 37036. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y = .0. )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6cN 37027*	Lemmma for mapdh6N 37036. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z = .0. )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6dN 37028*	Lemmma for mapdh6N 37036. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> ( I ` <. X , F , ( w .+ ( Y .+ Z ) ) >. ) = ( ( I ` <. X , F , w >. ) .+b ( I ` <. X , F , ( Y .+ Z ) >. ) ) )
Theorem	mapdh6eN 37029*	Lemmma for mapdh6N 37036. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> ( I ` <. X , F , ( ( w .+ Y ) .+ Z ) >. ) = ( ( I ` <. X , F , ( w .+ Y ) >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6fN 37030*	Lemmma for mapdh6N 37036. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> ( I ` <. X , F , ( w .+ Y ) >. ) = ( ( I ` <. X , F , w >. ) .+b ( I ` <. X , F , Y >. ) ) )
Theorem	mapdh6gN 37031*	Lemmma for mapdh6N 37036. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> ( ( I ` <. X , F , w >. ) .+b ( I ` <. X , F , ( Y .+ Z ) >. ) ) = ( ( ( I ` <. X , F , w >. ) .+b ( I ` <. X , F , Y >. ) ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6hN 37032*	Lemmma for mapdh6N 37036. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6iN 37033*	Lemmma for mapdh6N 37036. Eliminate auxiliary vector w. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6jN 37034*	Lemmma for mapdh6N 37036. Eliminate ( N { Y } ) = ( N { Z } ) hypothesis. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6kN 37035*	Lemmma for mapdh6N 37036. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6N 37036*	Part (6) of [Baer] p. 47 line 6. Note that we use -. X e. ( N ` { Y , Z } ) which is equivalent to Baer's "Fx i^i (Fy + Fz)" by lspdisjb 19126. TODO: If $ds with I and ph becomes a problem later, cbv's on I variables here to get rid of them. . Maybe reorder hypotheses in lemmas to the more consistent order of this theorem, so they can be shared with this theorem. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .+b = ( +g ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh7eN 37037*	Part (7) of [Baer] p. 48 line 10 (5 of 6 cases). (Note: 1 of 6 and 2 of 6 are hypotheses a and b.) (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { u } ) ) = ( J ` { F } ) )   &    |- ( ph -> u e. ( V \ { .0. } ) )   &    |- ( ph -> v e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { u } ) =/= ( N ` { v } ) )   &    |- ( ph -> -. w e. ( N ` { u , v } ) )   &    |- ( ph -> ( I ` <. u , F , w >. ) = E )   =>    |- ( ph -> ( I ` <. w , E , u >. ) = F )
Theorem	mapdh7cN 37038*	Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { u } ) ) = ( J ` { F } ) )   &    |- ( ph -> u e. ( V \ { .0. } ) )   &    |- ( ph -> v e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { u } ) =/= ( N ` { v } ) )   &    |- ( ph -> -. w e. ( N ` { u , v } ) )   &    |- ( ph -> ( I ` <. u , F , v >. ) = G )   =>    |- ( ph -> ( I ` <. v , G , u >. ) = F )
Theorem	mapdh7dN 37039*	Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { u } ) ) = ( J ` { F } ) )   &    |- ( ph -> u e. ( V \ { .0. } ) )   &    |- ( ph -> v e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { u } ) =/= ( N ` { v } ) )   &    |- ( ph -> -. w e. ( N ` { u , v } ) )   &    |- ( ph -> ( I ` <. u , F , v >. ) = G )   &    |- ( ph -> ( I ` <. u , F , w >. ) = E )   =>    |- ( ph -> ( I ` <. v , G , w >. ) = E )
Theorem	mapdh7fN 37040*	Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { u } ) ) = ( J ` { F } ) )   &    |- ( ph -> u e. ( V \ { .0. } ) )   &    |- ( ph -> v e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { u } ) =/= ( N ` { v } ) )   &    |- ( ph -> -. w e. ( N ` { u , v } ) )   &    |- ( ph -> ( I ` <. u , F , v >. ) = G )   &    |- ( ph -> ( I ` <. u , F , w >. ) = E )   =>    |- ( ph -> ( I ` <. w , E , v >. ) = G )
Theorem	mapdh75e 37041*	Part (7) of [Baer] p. 48 line 10 (5 of 6 cases). X, Y, Z are Baer's u, v, w. (Note: Cases 1 of 6 and 2 of 6 are hypotheses mapdh75b here and mapdh75a in mapdh75cN 37042.) (Contributed by NM, 2-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. Z , E , X >. ) = F )
Theorem	mapdh75cN 37042*	Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. Y , G , X >. ) = F )
Theorem	mapdh75d 37043*	Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. Y , G , Z >. ) = E )
Theorem	mapdh75fN 37044*	Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. Z , E , Y >. ) = G )
Syntax	chvm 37045	Extend class notation with vector to dual map.
class HVMap
Definition	df-hvmap 37046*	Extend class notation with a map from each nonzero vector x to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier e.g. lcf1o 36840, dochfl1 36765- should we update those to use this definition? (Contributed by NM, 23-Mar-2015.)
|- HVMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` (Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) ) ) )
Theorem	hvmapffval 37047*	Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
|- H = ( LHyp ` K )   =>    |- ( K e. X -> (HVMap ` K ) = ( w e. H |-> ( x e. ( ( Base ` ( ( DVecH ` K ) ` w ) ) \ { ( 0g ` ( ( DVecH ` K ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( iota_ j e. ( Base ` (Scalar ` ( ( DVecH ` K ) ` w ) ) ) E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) ) ) ) )
Theorem	hvmapfval 37048*	Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- O = ( ( ocH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   =>    |- ( ph -> M = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) )
Theorem	hvmapval 37049*	Value of map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- O = ( ( ocH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( M ` X ) = ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) v = ( t .+ ( j .x. X ) ) ) ) )
Theorem	hvmapvalvalN 37050*	Value of value of map (i.e. functional value) from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- O = ( ( ocH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- S = (Scalar ` U )   &    |- R = ( Base ` S )   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ( M ` X ) ` Y ) = ( iota_ j e. R E. t e. ( O ` { X } ) Y = ( t .+ ( j .x. X ) ) ) )
Theorem	hvmapidN 37051	The value of the vector to functional map, at the vector, is one. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- S = (Scalar ` U )   &    |- .1. = ( 1r ` S )   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( ( M ` X ) ` X ) = .1. )
Theorem	hvmap1o 37052*	The vector to functional map provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C. (Contributed by NM, 27-Mar-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) }   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )
Theorem	hvmapclN 37053*	Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- L = (LKer ` U )   &    |- D = (LDual ` U )   &    |- Q = ( 0g ` D )   &    |- C = { f e. F | ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) }   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( M ` X ) e. ( C \ { Q } ) )
Theorem	hvmap1o2 37054	The vector to functional map provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C. (Contributed by NM, 27-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- O = ( 0g ` C )   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( F \ { O } ) )
Theorem	hvmapcl2 37055	Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- O = ( 0g ` C )   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( M ` X ) e. ( F \ { O } ) )
Theorem	hvmaplfl 37056	The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- F = (LFnl ` U )   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( M ` X ) e. F )
Theorem	hvmaplkr 37057	Kernel of the vector to functional map. TODO: make this become lcfrlem11 36842. (Contributed by NM, 29-Mar-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- L = (LKer ` U )   &    |- M = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( L ` ( M ` X ) ) = ( O ` { X } ) )
Theorem	mapdhvmap 37058	Relationship between mapd and HVMap, which can be used to satify the last hypothesis of mapdpg 36995. Equation 10 of [Baer] p. 48. (Contributed by NM, 29-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- P = ( (HVMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { ( P ` X ) } ) )
Theorem	lspindp5 37059	Obtain an independent vector set U , X , Y from a vector U dependent on X and Z and another independent set Z , X , Y. (Here we don't show the ( N ` { X } ) =/= ( N ` { Y } ) part of the independence, which passes straight through. We also don't show nonzero vector requirements that are redundant for this theorem. Different orderings can be obtained using lspexch 19129 and prcom 4267.) (Contributed by NM, 4-May-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> U e. V )   &    |- ( ph -> Z e. ( N ` { X , U } ) )   &    |- ( ph -> -. Z e. ( N ` { X , Y } ) )   =>    |- ( ph -> -. U e. ( N ` { X , Y } ) )
Theorem	hdmaplem1 37060	Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. Z e. ( ( N ` { X } ) u. ( N ` { Y } ) ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( N ` { Z } ) =/= ( N ` { X } ) )
Theorem	hdmaplem2N 37061	Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. Z e. ( ( N ` { X } ) u. ( N ` { Y } ) ) )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( N ` { Z } ) =/= ( N ` { Y } ) )
Theorem	hdmaplem3 37062	Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. Z e. ( ( N ` { X } ) u. ( N ` { Y } ) ) )   &    |- ( ph -> Y e. V )   &    |- .0. = ( 0g ` W )   =>    |- ( ph -> Z e. ( V \ { .0. } ) )
Theorem	hdmaplem4 37063	Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .0. = ( 0g ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Z } ) =/= ( N ` { X } ) )   &    |- ( ph -> ( N ` { Z } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> -. Z e. ( ( N ` { X } ) u. ( N ` { Y } ) ) )
Theorem	mapdh8a 37064*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 5-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , T } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. X , F , T >. ) )
Theorem	mapdh8aa 37065*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 12-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Z } ) =/= ( N ` { T } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> -. Y e. ( N ` { Z , T } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. Z , E , T >. ) )
Theorem	mapdh8ab 37066*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { X } ) = ( N ` { T } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. Z , E , T >. ) )
Theorem	mapdh8ac 37067*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) = ( N ` { T } ) )   &    |- ( ph -> ( I ` <. X , F , w >. ) = B )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { w } ) )   &    |- ( ph -> -. X e. ( N ` { Y , w } ) )   &    |- ( ph -> ( N ` { w } ) =/= ( N ` { Z } ) )   &    |- ( ph -> -. X e. ( N ` { w , Z } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. Z , E , T >. ) )
Theorem	mapdh8ad 37068*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) = ( N ` { T } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. Z , E , T >. ) )
Theorem	mapdh8b 37069*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( I ` <. Y , G , w >. ) = E )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { w } ) =/= ( N ` { T } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { w } ) )   &    |- ( ph -> X e. ( N ` { Y , T } ) )   &    |- ( ph -> -. X e. ( N ` { Y , w } ) )   =>    |- ( ph -> ( I ` <. w , E , T >. ) = ( I ` <. Y , G , T >. ) )
Theorem	mapdh8c 37070*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , w >. ) = E )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { w } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { w } ) )   &    |- ( ph -> X e. ( N ` { Y , T } ) )   &    |- ( ph -> -. X e. ( N ` { Y , w } ) )   =>    |- ( ph -> ( I ` <. w , E , T >. ) = ( I ` <. X , F , T >. ) )
Theorem	mapdh8d0N 37071*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 10-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { w } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { w } ) )   &    |- ( ph -> -. X e. ( N ` { Y , w } ) )   &    |- ( ph -> X e. ( N ` { Y , T } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. X , F , T >. ) )
Theorem	mapdh8d 37072*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { w } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { w } ) )   &    |- ( ph -> -. X e. ( N ` { Y , w } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. X , F , T >. ) )
Theorem	mapdh8e 37073*	Part of Part (8) in [Baer] p. 48. Eliminate w. (Contributed by NM, 10-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   &    |- ( ph -> X e. ( N ` { Y , T } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. X , F , T >. ) )
Theorem	mapdh8fN 37074*	Part of Part (8) in [Baer] p. 48. Eliminate w. TODO: this is an instance of mapdh8a 37064- delete this? (Contributed by NM, 10-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   &    |- ( ph -> -. X e. ( N ` { Y , T } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. X , F , T >. ) )
Theorem	mapdh8g 37075*	Part of Part (8) in [Baer] p. 48. Eliminate X e. ( N ` { Y , T } ). TODO: break out T =/= .0. in mapdh8e 37073 so we can share hypotheses. Also, look at hypothesis sharing for earlier mapdh8* and mapdh75* stuff. (Contributed by NM, 10-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   =>    |- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. X , F , T >. ) )
Theorem	mapdh8i 37076*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 11-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { Z } ) =/= ( N ` { T } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { T } ) )   =>    |- ( ph -> ( I ` <. Y , ( I ` <. X , F , Y >. ) , T >. ) = ( I ` <. Z , ( I ` <. X , F , Z >. ) , T >. ) )
Theorem	mapdh8j 37077*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { Z } ) =/= ( N ` { T } ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. Y , ( I ` <. X , F , Y >. ) , T >. ) = ( I ` <. Z , ( I ` <. X , F , Z >. ) , T >. ) )
Theorem	mapdh8 37078*	Part (8) in [Baer] p. 48. Given a reference vector X, the value of function I at a vector T is independent of the choice of auxiliary vectors Y and Z. Unlike Baer's, our version does not require X, Y, and Z to be independent, and also is defined for all Y and Z that are not colinear with X or T. We do this to make the definition of Baer's sigma function more straightforward. (This part eliminates T =/= .0..) (Contributed by NM, 13-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) )   &    |- ( ph -> ( N ` { Z } ) =/= ( N ` { T } ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( I ` <. Y , ( I ` <. X , F , Y >. ) , T >. ) = ( I ` <. Z , ( I ` <. X , F , Z >. ) , T >. ) )
Theorem	mapdh9a 37079*	Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 37080? (Contributed by NM, 14-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )
Theorem	mapdh9aOLDN 37080*	Lemma for part (9) in [Baer] p. 48. (Contributed by NM, 14-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> E! y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )
Syntax	chdma1 37081	Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space.
class HDMap1
Syntax	chdma 37082	Extend class notation with map from vectors to functionals in the closed kernel dual space.
class HDMap
Definition	df-hdmap1 37083*	Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 37086 description for more details. (Contributed by NM, 14-May-2015.)
|- HDMap1 = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )
Definition	df-hdmap 37084*	Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 37119 description for more details. (Contributed by NM, 15-May-2015.)
|- HDMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >. / e ]. [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( (HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( (LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( (HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) )
Theorem	hdmap1ffval 37085*	Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015.)
|- H = ( LHyp ` K )   =>    |- ( K e. X -> (HDMap1 ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )
Theorem	hdmap1fval 37086*	Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span J to the convention L for this section. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   =>    |- ( ph -> I = ( x e. ( ( V X. D ) X. V ) |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) )
Theorem	hdmap1vallem 37087*	Value of preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   &    |- ( ph -> T e. ( ( V X. D ) X. V ) )   =>    |- ( ph -> ( I ` T ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) )
Theorem	hdmap1val 37088*	Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 37013.) TODO: change I = ( x e. _V |->... to ( ph -> ( I ` <. X , F , Y > ) =... in e.g. mapdh8 37078 to shorten proofs with no $d on x. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> F e. D )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )
Theorem	hdmap1val0 37089	Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 37014.) (Contributed by NM, 17-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( I ` <. X , F , .0. >. ) = Q )
Theorem	hdmap1val2 37090*	Value of preliminary map from vectors to functionals in the closed kernel dual space, for nonzero Y. (Contributed by NM, 16-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> F e. D )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) )
Theorem	hdmap1eq 37091	The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 16-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   =>    |- ( ph -> ( ( I ` <. X , F , Y >. ) = G <-> ( ( M ` ( N ` { Y } ) ) = ( L ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R G ) } ) ) ) )
Theorem	hdmap1cbv 37092*	Frequently used lemma to change bound variables in L hypothesis. (Contributed by NM, 15-May-2015.)
|- L = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   =>    |- L = ( y e. _V |-> if ( ( 2nd ` y ) = .0. , Q , ( iota_ i e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) ) ) )
Theorem	hdmap1valc 37093*	Connect the value of the preliminary map from vectors to functionals I to the hypothesis L used by earlier theorems. Note: the X e. ( V \ { .0. } ) hypothesis could be the more general X e. V but the former will be easier to use. TODO: use the I function directly in those theorems, so this theorem becomes unnecessary? TODO: The hdmap1cbv 37092 is probably unnecessary, but it would mean different $d's later on. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> Y e. V )   &    |- L = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) = ( L ` <. X , F , Y >. ) )
Theorem	hdmap1cl 37094	Convert closure theorem mapdhcl 37016 to use HDMap1 function. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) e. D )
Theorem	hdmap1eq2 37095	Convert mapdheq2 37018 to use HDMap1 function. (Contributed by NM, 16-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   =>    |- ( ph -> ( I ` <. Y , G , X >. ) = F )
Theorem	hdmap1eq4N 37096	Convert mapdheq4 37021 to use HDMap1 function. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = B )   =>    |- ( ph -> ( I ` <. Y , G , Z >. ) = B )
Theorem	hdmap1l6lem1 37097	Lemma for hdmap1l6 37111. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .+b = ( +g ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( M ` ( N ` { ( X .- ( Y .+ Z ) ) } ) ) = ( L ` { ( F R ( G .+b E ) ) } ) )
Theorem	hdmap1l6lem2 37098	Lemma for hdmap1l6 37111. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .+b = ( +g ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( M ` ( N ` { ( Y .+ Z ) } ) ) = ( L ` { ( G .+b E ) } ) )
Theorem	hdmap1l6a 37099	Lemma for hdmap1l6 37111. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .+b = ( +g ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	hdmap1l6b0N 37100	Lemmma for hdmap1l6 37111. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .+b = ( +g ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> ( ( N ` { X } ) i^i ( N ` { Y , Z } ) ) = { .0. } )   =>    |- ( ph -> -. X e. ( N ` { Y , Z } ) )