HomeHome Metamath Proof Explorer
Theorem List (p. 355 of 409) 		< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-26620) 		  Hilbert Space Explorer  Hilbert Space Explorer
(26621-28143) 		  Users' Mathboxes  Users' Mathboxes
(28144-40813) 		 

Theorem List for Metamath Proof Explorer - 35401-35500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmapdh8j 35401* 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 >. ) )
 
Theoremmapdh8 35402* 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 >. ) )
 
Theoremmapdh9a 35403* Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 35404? (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 >. ) ) )
 
Theoremmapdh9aOLDN 35404* 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 >. ) ) )
 
Syntaxchdma1 35405 Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space.
class HDMap1
 
Syntaxchdma 35406 Extend class notation with map from vectors to functionals in the closed kernel dual space.
class HDMap
 
Definitiondf-hdmap1 35407* Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 35410 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 ) } ) ) ) ) ) } ) )
 
Definitiondf-hdmap 35408* Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 35443 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 >. ) ) ) ) } ) )
 
Theoremhdmap1ffval 35409* 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 ) } ) ) ) ) ) } ) )
 
Theoremhdmap1fval 35410* 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 ) } ) ) ) ) ) )
 
Theoremhdmap1vallem 35411* 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 ) } ) ) ) ) )
 
Theoremhdmap1val 35412* Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 35337.) TODO: change I = ( x e. _V |->... to ( ph -> ( I ` <. X , F , Y > ) =... in e.g. mapdh8 35402 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 ) } ) ) ) ) )
 
Theoremhdmap1val0 35413 Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 35338.) (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 )
 
Theoremhdmap1val2 35414* 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 ) } ) ) ) )
 
Theoremhdmap1eq 35415 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 ) } ) ) ) )
 
Theoremhdmap1cbv 35416* 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 ) } ) ) ) ) )
 
Theoremhdmap1valc 35417* 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 35416 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 >. ) )
 
Theoremhdmap1cl 35418 Convert closure theorem mapdhcl 35340 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 )
 
Theoremhdmap1eq2 35419 Convert mapdheq2 35342 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 )
 
Theoremhdmap1eq4N 35420 Convert mapdheq4 35345 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 )
 
Theoremhdmap1l6lem1 35421 Lemma for hdmap1l6 35435. 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 ) ) } ) )
 
Theoremhdmap1l6lem2 35422 Lemma for hdmap1l6 35435. 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 ) } ) )
 
Theoremhdmap1l6a 35423 Lemma for hdmap1l6 35435. 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 >. ) ) )
 
Theoremhdmap1l6b0N 35424 Lemmma for hdmap1l6 35435. (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 } ) )
 
Theoremhdmap1l6b 35425 Lemmma for hdmap1l6 35435. (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 >. ) ) )
 
Theoremhdmap1l6c 35426 Lemmma for hdmap1l6 35435. (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 >. ) ) )
 
Theoremhdmap1l6d 35427 Lemmma for hdmap1l6 35435. (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 ) >. ) ) )
 
Theoremhdmap1l6e 35428 Lemmma for hdmap1l6 35435. 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 >. ) ) )
 
Theoremhdmap1l6f 35429 Lemmma for hdmap1l6 35435. 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 >. ) ) )
 
Theoremhdmap1l6g 35430 Lemmma for hdmap1l6 35435. 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 )   &    |- .- = ( -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 >. ) .+b ( I ` <. X , F , ( Y .+ Z ) >. ) ) = ( ( ( I ` <. X , F , w >. ) .+b ( I ` <. X , F , Y >. ) ) .+b ( I ` <. X , F , Z >. ) ) )
 
Theoremhdmap1l6h 35431 Lemmma for hdmap1l6 35435. Part (6) of [Baer] p. 48 line 2. (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 , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
 
Theoremhdmap1l6i 35432 Lemmma for hdmap1l6 35435. Eliminate auxiliary vector w. (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 -> 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 >. ) ) )
 
Theoremhdmap1l6j 35433 Lemmma for hdmap1l6 35435. Eliminate ( N { Y } ) = ( N { Z } ) hypothesis. (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 -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
 
Theoremhdmap1l6k 35434 Lemmma for hdmap1l6 35435. Eliminate nonzero vector requirement. (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 -> 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 >. ) ) )
 
Theoremhdmap1l6 35435 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 18398. (Contributed by NM, 17-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 )   &    |- .+b = ( +g ` 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 -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
 
Theoremhdmap1p6N 35436 (Convert mapdh6N 35360 to use HDMap1 function.) 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 18398. TODO: No longer used and should be deleted. Use hdmap1l6 35435 instead. Also delete unused mapdh6N 35360 etc. leading up to this. (Contributed by NM, 17-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 )   &    |- .+b = ( +g ` 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 -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
 
Theoremhdmap1eulem 35437* Lemma for hdmap1eu 35439. TODO: combine with hdmap1eu 35439 or at least share some hypotheses. (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 -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> T 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 -> E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )
 
Theoremhdmap1eulemOLDN 35438* Lemma for hdmap1euOLDN 35440. TODO: combine with hdmap1euOLDN 35440 or at least share some hypotheses. (Contributed by NM, 15-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 = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> T 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 -> E! y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )
 
Theoremhdmap1eu 35439* Convert mapdh9a 35403 to use the HDMap1 notation. (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 -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( 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 >. ) ) )
 
Theoremhdmap1euOLDN 35440* Convert mapdh9aOLDN 35404 to use the HDMap1 notation. (Contributed by NM, 15-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 -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( 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 >. ) ) )
 
Theoremhdmap1neglem1N 35441 Lemma for hdmapneg 35462. TODO: Not used; delete. (Contributed by NM, 23-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = ( invg ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- S = ( invg ` 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 ` <. ( R ` X ) , ( S ` F ) , ( R ` Y ) >. ) = ( S ` G ) )
 
Theoremhdmapffval 35442* Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   =>    |- ( K e. X -> (HDMap ` K ) = ( w e. H |-> { 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 >. ) ) ) ) } ) )
 
Theoremhdmapfval 35443* Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   =>    |- ( ph -> S = ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) )
 
Theoremhdmapval 35444* Value of map from vectors to functionals in the closed kernel dual space. This is the function sigma on line 27 above part 9 in [Baer] p. 48. We select a convenient fixed reference vector E to be <. 0 , 1 >. (corresponding to vector u on p. 48 line 7) whose span is the lattice isomorphism map of the fiducial atom P = ( ( oc ` K ) ` W ) (see dvheveccl 34725). ( J ` E ) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 35382 shows in Baer's notation (Fu)* = Gu'). Baer's independent vectors v and w on line 7 correspond to our z that the A. z e. V ranges over. The middle term ( I ` <. E , ( J ` E ) , z >. ) provides isolation to allow E and T to assume the same value without conflict. Closure is shown by hdmapcl 35446. If a separate auxiliary vector is known, hdmapval2 35448 provides a version without quantification. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( S ` T ) = ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
 
TheoremhdmapfnN 35445 Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> S Fn V )
 
Theoremhdmapcl 35446 Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( S ` T ) e. D )
 
Theoremhdmapval2lem 35447* Lemma for hdmapval2 35448. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   &    |- ( ph -> F e. D )   =>    |- ( ph -> ( ( S ` T ) = F <-> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
 
Theoremhdmapval2 35448 Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two =/= hypothesis? Consider hdmaplem1 35384 through hdmaplem4 35387, which would become obsolete. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( ( N ` { E } ) u. ( N ` { T } ) ) )   =>    |- ( ph -> ( S ` T ) = ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. ) )
 
Theoremhdmapval0 35449 Value of map from vectors to functionals at zero. Note: we use dvh3dim 35059 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 35460 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- Q = ( 0g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ( S ` .0. ) = Q )
 
Theoremhdmapeveclem 35450 Lemma for hdmapevec 35451. TODO: combine with hdmapevec 35451 if it shortens overall. (Contributed by NM, 16-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- J = ( (HVMap ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( ( N ` { E } ) u. ( N ` { E } ) ) )   =>    |- ( ph -> ( S ` E ) = ( J ` E ) )
 
Theoremhdmapevec 35451 Value of map from vectors to functionals at the reference vector E. (Contributed by NM, 16-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- J = ( (HVMap ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ( S ` E ) = ( J ` E ) )
 
Theoremhdmapevec2 35452 The inner product of the reference vector E with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of [Holland95] p. 14 line 32, [ e , e ] =/= 0 is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- J = ( (HVMap ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- .1. = ( 1r ` R )   =>    |- ( ph -> ( ( S ` E ) ` E ) = .1. )
 
Theoremhdmapval3lemN 35453 Value of map from vectors to functionals at arguments not colinear with the reference vector E. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( N ` { T } ) =/= ( N ` { E } ) )   &    |- ( ph -> T e. ( V \ { ( 0g ` U ) } ) )   &    |- ( ph -> x e. V )   &    |- ( ph -> -. x e. ( N ` { E , T } ) )   =>    |- ( ph -> ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) )
 
Theoremhdmapval3N 35454 Value of map from vectors to functionals at arguments not colinear with the reference vector E. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( N ` { T } ) =/= ( N ` { E } ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) )
 
Theoremhdmap10lem 35455 Lemma for hdmap10 35456. (Contributed by NM, 17-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- .0. = ( 0g ` U )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> T e. ( V \ { .0. } ) )   =>    |- ( ph -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )
 
Theoremhdmap10 35456 Part 10 in [Baer] p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )
 
Theoremhdmap11lem1 35457 Lemma for hdmapadd 35459. (Contributed by NM, 26-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- D = ( Base ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> z e. V )   &    |- ( ph -> -. z e. ( N ` { X , Y } ) )   &    |- ( ph -> ( N ` { z } ) =/= ( N ` { E } ) )   =>    |- ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )
 
Theoremhdmap11lem2 35458 Lemma for hdmapadd 35459. (Contributed by NM, 26-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- D = ( Base ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   =>    |- ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )
 
Theoremhdmapadd 35459 Part 11 in [Baer] p. 48 line 35, (a+b)S = aS+bS in their notation (S = sigma). (Contributed by NM, 22-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )
 
Theoremhdmapeq0 35460 Part of proof of part 12 in [Baer] p. 49 line 3. (Contributed by NM, 22-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- Q = ( 0g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( ( S ` T ) = Q <-> T = .0. ) )
 
Theoremhdmapnzcl 35461 Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- Q = ( 0g ` C )   &    |- D = ( Base ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   =>    |- ( ph -> ( S ` T ) e. ( D \ { Q } ) )
 
Theoremhdmapneg 35462 Part of proof of part 12 in [Baer] p. 49 line 4. The sigma map of a negative is the negative of the sigma map. (Contributed by NM, 24-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- M = ( invg ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- I = ( invg ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( S ` ( M ` T ) ) = ( I ` ( S ` T ) ) )
 
Theoremhdmapsub 35463 Part of proof of part 12 in [Baer] p. 49 line 5, (a-b)S = aS-bS in their notation (S = sigma). (Contributed by NM, 26-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- N = ( -g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( S ` ( X .- Y ) ) = ( ( S ` X ) N ( S ` Y ) ) )
 
Theoremhdmap11 35464 Part of proof of part 12 in [Baer] p. 49 line 4, aS=bS iff a=b in their notation (S = sigma). The sigma map is one-to-one. (Contributed by NM, 26-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ( S ` X ) = ( S ` Y ) <-> X = Y ) )
 
Theoremhdmaprnlem1N 35465 Part of proof of part 12 in [Baer] p. 49 line 10, Gu' =/= Gs. Our ( N ` { v } ) is Baer's T. (Contributed by NM, 26-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   =>    |- ( ph -> ( L ` { ( S ` u ) } ) =/= ( L ` { s } ) )
 
Theoremhdmaprnlem3N 35466 Part of proof of part 12 in [Baer] p. 49 line 15, T =/= P. Our ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) is Baer's P, where P* = G(u'+s). (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   =>    |- ( ph -> ( N ` { v } ) =/= ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) )
 
Theoremhdmaprnlem3uN 35467 Part of proof of part 12 in [Baer] p. 49. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C