P. 354 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35301-35400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hvmapffval 35301*	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 35302*	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 35303*	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 35304*	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 35305	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 35306*	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 35307*	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 35308	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 35309	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 35310	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 35311	Kernel of the vector to functional map. TODO: make this become lcfrlem11 35096. (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 35312	Relationship between mapd and HVMap, which can be used to satify the last hypothesis of mapdpg 35249. 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 35313	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 18357 and prcom 4084.) (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 35314	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 35315	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 35316	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 35317	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 35318*	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 35319*	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 35320*	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 35321*	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 35322*	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 35323*	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 35324*	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 35325*	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 35326*	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 35327*	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 35328*	Part of Part (8) in [Baer] p. 48. Eliminate w. TODO: this is an instance of mapdh8a 35318- 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 35329*	Part of Part (8) in [Baer] p. 48. Eliminate X e. ( N ` { Y , T } ). TODO: break out T =/= .0. in mapdh8e 35327 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 35330*	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 35331*	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 35332*	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 35333*	Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 35334? (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 35334*	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 35335	Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space.
class HDMap1
Syntax	chdma 35336	Extend class notation with map from vectors to functionals in the closed kernel dual space.
class HDMap
Definition	df-hdmap1 35337*	Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 35340 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 35338*	Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 35373 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 35339*	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 35340*	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 35341*	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 35342*	Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 35267.) TODO: change I = ( x e. _V |->... to ( ph -> ( I ` <. X , F , Y > ) =... in e.g. mapdh8 35332 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 35343	Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 35268.) (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 35344*	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 35345	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 35346*	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 35347*	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 35346 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 35348	Convert closure theorem mapdhcl 35270 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 35349	Convert mapdheq2 35272 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 35350	Convert mapdheq4 35275 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 35351	Lemma for hdmap1l6 35365. 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 35352	Lemma for hdmap1l6 35365. 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 35353	Lemma for hdmap1l6 35365. 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 35354	Lemmma for hdmap1l6 35365. (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 } ) )
Theorem	hdmap1l6b 35355	Lemmma for hdmap1l6 35365. (Contributed by NM, 24-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 = .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	hdmap1l6c 35356	Lemmma for hdmap1l6 35365. (Contributed by NM, 24-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 )   &    |- ( 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	hdmap1l6d 35357	Lemmma for hdmap1l6 35365. (Contributed by NM, 1-May-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 -> -. 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	hdmap1l6e 35358	Lemmma for hdmap1l6 35365. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-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 -> -. 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	hdmap1l6f 35359	Lemmma for hdmap1l6 35365. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-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 -> -. 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	hdmap1l6g 35360	Lemmma for hdmap1l6 35365. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |-