HomeHome Metamath Proof Explorer
Theorem List (p. 324 of 325)
< 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-22374)
  Hilbert Space Explorer  Hilbert Space Explorer
(22375-23897)
  Users' Mathboxes  Users' Mathboxes
(23898-32447)
 

Theorem List for Metamath Proof Explorer - 32301-32400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremhdmap1l6h 32301 Lemmma for hdmap1l6 32305. 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 32302 Lemmma for hdmap1l6 32305. 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 32303 Lemmma for hdmap1l6 32305. 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 32304 Lemmma for hdmap1l6 32305. 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 32305 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 16153. (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 32306 (Convert mapdh6N 32230 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 16153. TODO: No longer used and should be deleted. Use hdmap1l6 32305 instead. Also delete unused mapdh6N 32230 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 32307* Lemma for hdmap1eu 32309. TODO: combine with hdmap1eu 32309 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 32308* Lemma for hdmap1euOLDN 32310. TODO: combine with hdmap1euOLDN 32310 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 32309* Convert mapdh9a 32273 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 32310* Convert mapdh9aOLDN 32274 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 32311 Lemma for hdmapneg 32332. 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 32312* 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 32313* 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 32314* 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 31595). 
( J `  E
) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 32252 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 32316. If a separate auxiliary vector is known, hdmapval2 32318 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 32315 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 32316 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 32317* Lemma for hdmapval2 32318. (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 32318 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 32254 through hdmaplem4 32257, 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 32319 Value of map from vectors to functionals at zero. Note: we use dvh3dim 31929 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 32330 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 32320 Lemma for hdmapevec 32321. TODO: combine with hdmapevec 32321 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 32321 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 32322 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 32323 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 32324 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 32325 Lemma for hdmap10 32326. (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 32326 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 32327 Lemma for hdmapadd 32329. (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 32328 Lemma for hdmapadd 32329. (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 32329 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 32330 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 32331 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 32332 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 32333 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 32334 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 32335 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 32336 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 32337 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 )   =>    |-  ( ph  ->  ( N `  { u } )  =/=  ( `' M `  ( L `
  { ( ( S `  u ) 
 .+b  s ) }
 ) ) )
 
Theoremhdmaprnlem4tN 32338 Lemma for hdmaprnN 32350. TODO: This lemma doesn't quite pay for itself even though used 4 times. Maybe prove this directly instead. (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  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   =>    |-  ( ph  ->  t  e.  V )
 
Theoremhdmaprnlem4N 32339 Part of proof of part 12 in [Baer] p. 49 line 19. (T* =) (Ft)* = Gs. (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  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( M `  ( N `  { t } )
 )  =  ( L `
  { s }
 ) )
 
Theoremhdmaprnlem6N 32340 Part of proof of part 12 in [Baer] p. 49 line 18, G(u'+s) = G(u'+t). (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  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  U )   &    |-  ( ph  ->  ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )   =>    |-  ( ph  ->  ( L `  { (
 ( S `  u )  .+b  s ) }
 )  =  ( L `
  { ( ( S `  u ) 
 .+b  ( S `  t ) ) }
 ) )
 
Theoremhdmaprnlem7N 32341 Part of proof of part 12 in [Baer] p. 49 line 19, s-St  e. G(u'+s) = P*. (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  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  U )   &    |-  ( ph  ->  ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )   =>    |-  ( ph  ->  ( s ( -g `  C ) ( S `  t ) )  e.  ( L `  { (
 ( S `  u )  .+b  s ) }
 ) )
 
Theoremhdmaprnlem8N 32342 Part of proof of part 12 in [Baer] p. 49 line 19, s-St  e. (Ft)* = T*. (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  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  U )   &    |-  ( ph  ->  ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )   =>    |-  ( ph  ->  ( s ( -g `  C ) ( S `  t ) )  e.  ( M `  ( N `  { t }
 ) ) )
 
Theoremhdmaprnlem9N 32343 Part of proof of part 12 in [Baer] p. 49 line 21, s=S(t). TODO: we seem to be going back and forth with mapd11 32122 and mapdcnv11N 32142. Use better hypotheses and/or theorems? (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  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  U )   &    |-  ( ph  ->  ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )   =>    |-  ( ph  ->  s  =  ( S `  t ) )
 
Theoremhdmaprnlem3eN 32344* Lemma for hdmaprnN 32350. (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 )   &    |-  .+  =  ( +g  `  U )   =>    |-  ( ph  ->  E. t  e.  (
 ( N `  { v } )  \  {  .0.  } ) ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )
 
Theoremhdmaprnlem10N 32345* Lemma for hdmaprnN 32350. Show  s is in the range of  S. (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 )   &    |-  .+  =  ( +g  `  U )   =>    |-  ( ph  ->  E. t  e.  V  ( S `  t )  =  s )
 
Theoremhdmaprnlem11N 32346* Lemma for hdmaprnN 32350. Show  s is in the range of  S. (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 )   &    |-  .+  =  ( +g  `  U )   =>    |-  ( ph  ->  s  e.  ran  S )
 
Theoremhdmaprnlem15N 32347* Lemma for hdmaprnN 32350. Eliminate  u. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .0.  =  ( 0g `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  s  e.  ( D  \  {  .0.  } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `  { v } )
 )  =  ( L `
  { s }
 ) )   =>    |-  ( ph  ->  s  e.  ran  S )
 
Theoremhdmaprnlem16N 32348 Lemma for hdmaprnN 32350. Eliminate  v. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .0.  =  ( 0g `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  s  e.  ( D  \  {  .0.  } ) )   =>    |-  ( ph  ->  s  e.  ran  S )
 
Theoremhdmaprnlem17N 32349 Lemma for hdmaprnN 32350. Include zero. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .0.  =  ( 0g `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  s  e.  D )   =>    |-  ( ph  ->  s  e.  ran  S )
 
TheoremhdmaprnN 32350 Part of proof of part 12 in [Baer] p. 49 line 21, As=B. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ran  S  =  D )
 
Theoremhdmapf1oN 32351 Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 32329, this shows the map is an automorphism from the additive group of vectors to the additive group of functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  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  ->  S : V -1-1-onto-> D )
 
Theoremhdmap14lem1a 32352 Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  F  e.  B )   &    |- 
 .0.  =  ( 0g `  R )   &    |-  ( ph  ->  F  =/=  .0.  )   =>    |-  ( ph  ->  ( L `  { ( S `  X ) }
 )  =  ( L `
  { ( S `
  ( F  .x.  X ) ) } )
 )
 
Theoremhdmap14lem2a 32353* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  .0. so it can be used in hdmap14lem10 32363. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  F  e.  B )   =>    |-  ( ph  ->  E. g  e.  A  ( S `  ( F  .x.  X ) )  =  ( g 
 .xb  ( S `  X ) ) )
 
Theoremhdmap14lem1 32354 Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  ( L ` 
 { ( S `  X ) } )  =  ( L `  { ( S `  ( F  .x.  X ) ) } )
 )
 
Theoremhdmap14lem2N 32355* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  Z so it can be used in hdmap14lem10 32363. (Contributed by NM, 31-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  E. g  e.  ( A  \  { Q } ) ( S `
  ( F  .x.  X ) )  =  ( g  .xb  ( S `  X ) ) )
 
Theoremhdmap14lem3 32356* Prior to part 14 in [Baer] p. 49, line 26. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  E! g  e.  ( A  \  { Q } ) ( S `
  ( F  .x.  X ) )  =  ( g  .xb  ( S `  X ) ) )
 
Theoremhdmap14lem4a 32357* Simplify  ( A  \  { Q } ) in hdmap14lem3 32356 to provide a slightly simpler definition later. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  ( E! g  e.  ( A  \  { Q } )
 ( S `  ( F  .x.  X ) )  =  ( g  .xb  ( S `  X ) )  <->  E! g  e.  A  ( S `  ( F 
 .x.  X ) )  =  ( g  .xb  ( S `  X ) ) ) )
 
Theoremhdmap14lem4 32358* Simplify  ( A  \  { Q } ) in hdmap14lem3 32356 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 32357 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 32357 into this one. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  E! g  e.  A  ( S `  ( F  .x.  X ) )  =  ( g 
 .xb  ( S `  X ) ) )
 
Theoremhdmap14lem6 32359* Case where  F is zero. (Contributed by NM, 1-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  =  Z )   =>    |-  ( ph  ->  E! g  e.  A  ( S `  ( F 
 .x.  X ) )  =  ( g  .xb  ( S `  X ) ) )
 
Theoremhdmap14lem7 32360* Combine cases of  F. TODO: Can this be done at once in hdmap14lem3 32356, in order to get rid of hdmap14lem6 32359? Perhaps modify lspsneu 16150 to become  E! k  e.  K instead of  E! k  e.  ( K  \  {  .0.  } )? (Contributed by NM, 1-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  F  e.  B )   =>    |-  ( ph  ->  E! g  e.  A  ( S `  ( F  .x.  X ) )  =  ( g  .xb  ( S `  X ) ) )
 
Theoremhdmap14lem8 32361 Part of proof of part 14 in [Baer] p. 49 lines 33-35. (Contributed by NM, 1-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( +g  `  C )   &    |-  .xb  =  ( .s `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  B )   &    |-  ( ph  ->  G  e.  A )   &    |-  ( ph  ->  I  e.  A )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  X ) )  =  ( G  .xb  ( S `  X ) ) )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  Y ) )  =  ( I  .xb  ( S `  Y ) ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  J  e.  A )   &    |-  ( ph  ->  ( S `  ( F  .x.  ( X 
 .+  Y ) ) )  =  ( J 
 .xb  ( S `  ( X  .+  Y ) ) ) )   =>    |-  ( ph  ->  ( ( J  .xb  ( S `  X ) ) 
 .+b  ( J  .xb  ( S `  Y ) ) )  =  ( ( G  .xb  ( S `  X ) ) 
 .+b  ( I  .xb  ( S `  Y ) ) ) )
 
Theoremhdmap14lem9 32362 Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 1-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( +g  `  C )   &    |-  .xb  =  ( .s `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  B )   &    |-  ( ph  ->  G  e.  A )   &    |-  ( ph  ->  I  e.  A )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  X ) )  =  ( G  .xb  ( S `  X ) ) )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  Y ) )  =  ( I  .xb  ( S `  Y ) ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  J  e.  A )   &    |-  ( ph  ->  ( S `  ( F  .x.  ( X 
 .+  Y ) ) )  =  ( J 
 .xb  ( S `  ( X  .+  Y ) ) ) )   =>    |-  ( ph  ->  G  =  I )
 
Theoremhdmap14lem10 32363 Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 3-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( +g  `  C )   &    |-  .xb  =  ( .s `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  B )   &    |-  ( ph  ->  G  e.  A )   &    |-  ( ph  ->  I  e.  A )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  X ) )  =  ( G  .xb  ( S `  X ) ) )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  Y ) )  =  ( I  .xb  ( S `  Y ) ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   =>    |-  ( ph  ->  G  =  I )
 
Theoremhdmap14lem11 32364 Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 3-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( +g  `  C )   &    |-  .xb  =  ( .s `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  B )   &    |-  ( ph  ->  G  e.  A )   &    |-  ( ph  ->  I  e.  A )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  X ) )  =  ( G  .xb  ( S `  X ) ) )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  Y ) )  =  ( I  .xb  ( S `  Y ) ) )   =>    |-  ( ph  ->  G  =  I )
 
Theoremhdmap14lem12 32365* Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  B )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  G  e.  A )   =>    |-  ( ph  ->  (
 ( S `  ( F  .x.  X ) )  =  ( G  .xb  ( S `  X ) )  <->  A. y  e.  ( V  \  {  .0.  }
 ) ( S `  ( F  .x.  y ) )  =  ( G 
 .xb  ( S `  y ) ) ) )
 
Theoremhdmap14lem13 32366* Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  B )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  G  e.  A )   =>    |-  ( ph  ->  (
 ( S `  ( F  .x.  X ) )  =  ( G  .xb  ( S `  X ) )  <->  A. y  e.  V  ( S `  ( F 
 .x.  y ) )  =  ( G  .xb  ( S `  y ) ) ) )
 
Theoremhdmap14lem14 32367* Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  B )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   =>    |-  ( ph  ->  E! g  e.  A  A. x  e.  V  ( S `  ( F  .x.  x ) )  =  ( g 
 .xb  ( S `  x ) ) )
 
Theoremhdmap14lem15 32368* Part of proof of part 14 in [Baer] p. 50 line 3. Convert scalar base of dual to scalar base of vector space. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  B )   =>    |-  ( ph  ->  E! g  e.  B  A. x  e.  V  ( S `  ( F  .x.  x ) )  =  ( g  .xb  ( S `  x ) ) )
 
Syntaxchg 32369 Extend class notation with g-map.
 class HGMap
 
Definitiondf-hgmap 32370* Define map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
 |- HGMap  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { a  |  [. ( ( DVecH `  k ) `  w )  /  u ]. [. ( Base `  (Scalar `  u ) )  /  b ]. [. ( (HDMap `  k ) `  w )  /  m ]. a  e.  ( x  e.  b  |->  ( iota_ y  e.  b A. v  e.  ( Base `  u ) ( m `  ( x ( .s `  u ) v ) )  =  ( y ( .s `  ( (LCDual `  k ) `  w ) ) ( m `
  v ) ) ) ) } )
 )
 
Theoremhgmapffval 32371* Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
 |-  H  =  ( LHyp `  K )   =>    |-  ( K  e.  X  ->  (HGMap `  K )  =  ( w  e.  H  |->  { a  |  [. (
 ( DVecH `  K ) `  w )  /  u ].
 [. ( Base `  (Scalar `  u ) )  /  b ]. [. ( (HDMap `  K ) `  w )  /  m ]. a  e.  ( x  e.  b  |->  ( iota_ y  e.  b A. v  e.  ( Base `  u ) ( m `  ( x ( .s `  u ) v ) )  =  ( y ( .s `  ( (LCDual `  K ) `  w ) ) ( m `
  v ) ) ) ) } )
 )
 
Theoremhgmapfval 32372* Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  M  =  ( (HDMap `  K ) `  W )   &    |-  I  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  Y  /\  W  e.  H ) )   =>    |-  ( ph  ->  I  =  ( x  e.  B  |->  ( iota_ y  e.  B A. v  e.  V  ( M `  ( x 
 .x.  v ) )  =  ( y  .xb  ( M `  v ) ) ) ) )
 
Theoremhgmapval 32373* Value of map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. Function sigma of scalar f in part 14 of [Baer] p. 50 line 4. TODO: variable names are inherited from older version. Maybe make more consistent with hdmap14lem15 32368. (Contributed by NM, 25-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  M  =  ( (HDMap `  K ) `  W )   &    |-  I  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  Y  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  B )   =>    |-  ( ph  ->  ( I `  X )  =  ( iota_ y  e.  B A. v  e.  V  ( M `  ( X  .x.  v ) )  =  ( y 
 .xb  ( M `  v ) ) ) )
 
TheoremhgmapfnN 32374 Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  G  Fn  B )
 
Theoremhgmapcl 32375 Closure of scalar sigma map i.e. the map from the vector space scalar base to the dual space scalar base. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  B )   =>    |-  ( ph  ->  ( G `  F )  e.  B )
 
Theoremhgmapdcl 32376 Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  Q  =  (Scalar `  C )   &    |-  A  =  ( Base `  Q )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  B )   =>    |-  ( ph  ->  ( G `  F )  e.  A )
 
Theoremhgmapvs 32377 Part 15 of [Baer] p. 50 line 6. Also line 15 in [Holland95] p. 14. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  F  e.  B )   =>    |-  ( ph  ->  ( S `  ( F  .x.  X ) )  =  ( ( G `  F )  .xb  ( S `  X ) ) )
 
Theoremhgmapval0 32378 Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  .0.  =  ( 0g `  R )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ( G `  .0.  )  =  .0.  )
 
Theoremhgmapval1 32379 Value of the scalar sigma map at one. (Contributed by NM, 12-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  .1.  =  ( 1r `  R )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ( G `  .1.  )  =  .1.  )
 
Theoremhgmapadd 32380 Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W