HomeHome Metamath Proof Explorer
Theorem List (p. 320 of 321)
< 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-22269)
  Hilbert Space Explorer  Hilbert Space Explorer
(22270-23792)
  Users' Mathboxes  Users' Mathboxes
(23793-32079)
 

Theorem List for Metamath Proof Explorer - 31901-32000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmapdh8g 31901* Part of Part (8) in [Baer] p. 48. Eliminate  X  e.  ( N `  { Y ,  T } ). TODO: break out  T  =/= 
.0. in mapdh8e 31899 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 >. ) )
 
Theoremmapdh8i 31902* 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 >. ) )
 
Theoremmapdh8j 31903* 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 31904* 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 31905* Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 31906? (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 31906* 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 31907 Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space.
 class HDMap1
 
Syntaxchdma 31908 Extend class notation with map from vectors to functionals in the closed kernel dual space.
 class HDMap
 
Definitiondf-hdmap1 31909* Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 31912 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 31910* Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 31945 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 31911* 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 31912* 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 31913* 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 31914* Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 31839.) TODO: change  I  =  ( x  e.  _V  |->... to  ( ph  ->  ( I `  <. X ,  F ,  Y  >  )  =... in e.g. mapdh8 31904 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 31915 Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 31840.) (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 31916* 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 31917 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 31918* 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 31919* 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 31918 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 31920 Convert closure theorem mapdhcl 31842 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 31921 Convert mapdheq2 31844 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 31922 Convert mapdheq4 31847 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 31923 Lemma for hdmap1l6 31937. 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 31924 Lemma for hdmap1l6 31937. 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 31925 Lemma for hdmap1l6 31937. 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 31926 Lemmma for hdmap1l6 31937. (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 31927 Lemmma for hdmap1l6 31937. (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 31928 Lemmma for hdmap1l6 31937. (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 31929 Lemmma for hdmap1l6 31937. (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 31930 Lemmma for hdmap1l6 31937. 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 31931 Lemmma for hdmap1l6 31937. 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 31932 Lemmma for hdmap1l6 31937. 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 31933 Lemmma for hdmap1l6 31937. 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 31934 Lemmma for hdmap1l6 31937. 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 31935 Lemmma for hdmap1l6 31937. 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 31936 Lemmma for hdmap1l6 31937. 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 31937 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 16125. (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 31938 (Convert mapdh6N 31862 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 16125. TODO: No longer used and should be deleted. Use hdmap1l6 31937 instead. Also delete unused mapdh6N 31862 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 31939* Lemma for hdmap1eu 31941. TODO: combine with hdmap1eu 31941 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 31940* Lemma for hdmap1euOLDN 31942. TODO: combine with hdmap1euOLDN 31942 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 31941* Convert mapdh9a 31905 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 31942* Convert mapdh9aOLDN 31906 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 31943 Lemma for hdmapneg 31964. 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  =  ( inv g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  S  =  ( inv 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  ->  ( 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 31944* 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 31945* 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 31946* 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 31227). 
( J `  E
) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 31884 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 31948. If a separate auxiliary vector is known, hdmapval2 31950 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 31947 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 31948 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 31949* Lemma for hdmapval2 31950. (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 31950 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 31886 through hdmaplem4 31889, 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 31951 Value of map from vectors to functionals at zero. Note: we use dvh3dim 31561 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 31962 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 31952 Lemma for hdmapevec 31953. TODO: combine with hdmapevec 31953 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 31953 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 31954 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 31955 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 31956 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 31957 Lemma for hdmap10 31958. (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 31958 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 31959 Lemma for hdmapadd 31961. (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 31960 Lemma for hdmapadd 31961. (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 31961 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 31962 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 31963 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 31964 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  =  ( inv g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  I  =  ( inv g `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  ( S `  ( M `  T ) )  =  ( I `  ( S `  T ) ) )
 
Theoremhdmapsub 31965 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 ) `