HomeHome Metamath Proof Explorer
Theorem List (p. 352 of 394)
< 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-26403)
  Hilbert Space Explorer  Hilbert Space Explorer
(26404-27926)
  Users' Mathboxes  Users' Mathboxes
(27927-39314)
 

Theorem List for Metamath Proof Explorer - 35101-35200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremhdmap1eulem 35101* Lemma for hdmap1eu 35103. TODO: combine with hdmap1eu 35103 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 35102* Lemma for hdmap1euOLDN 35104. TODO: combine with hdmap1euOLDN 35104 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 35103* Convert mapdh9a 35067 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 35104* Convert mapdh9aOLDN 35068 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 35105 Lemma for hdmapneg 35126. TODO: Not used; delete. (Contributed by NM, 23-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  ( invg `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  S  =  ( invg `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   =>    |-  ( ph  ->  ( I `  <. ( R `  X ) ,  ( S `  F ) ,  ( R `  Y ) >. )  =  ( S `  G ) )
 
Theoremhdmapffval 35106* 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 35107* 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 35108* 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 34389). 
( J `  E
) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 35046 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 35110. If a separate auxiliary vector is known, hdmapval2 35112 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 35109 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 35110 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 35111* Lemma for hdmapval2 35112. (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 35112 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 35048 through hdmaplem4 35051, 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 35113 Value of map from vectors to functionals at zero. Note: we use dvh3dim 34723 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 35124 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 35114 Lemma for hdmapevec 35115. TODO: combine with hdmapevec 35115 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 35115 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 35116 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 35117 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 35118 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 35119 Lemma for hdmap10 35120. (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 35120 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 35121 Lemma for hdmapadd 35123. (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 35122 Lemma for hdmapadd 35123. (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 35123 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 35124 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 35125 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 35126 Part of proof of part 12 in [Baer] p. 49 line 4. The sigma map of a negative is the negative of the sigma map. (Contributed by NM, 24-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  M  =  ( invg `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  I  =  ( invg `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  ( S `  ( M `  T ) )  =  ( I `  ( S `  T ) ) )
 
Theoremhdmapsub 35127 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 35128 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 35129 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 35130 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 35131 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 35132 Lemma for hdmaprnN 35144. 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 35133 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 35134 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 35135 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 35136 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 35137 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 34916 and mapdcnv11N 34936. 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 35138* Lemma for hdmaprnN 35144. (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 35139* Lemma for hdmaprnN 35144. 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 35140* Lemma for hdmaprnN 35144. 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 35141* Lemma for hdmaprnN 35144. 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 35142 Lemma for hdmaprnN 35144. 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 35143 Lemma for hdmaprnN 35144. 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 35144 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 35145 Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 35123, 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 35146 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 35147* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  .0. so it can be used in hdmap14lem10 35157. (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 35148 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 35149* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  Z so it can be used in hdmap14lem10 35157. (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 35150* 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 35151* Simplify  ( A  \  { Q } ) in hdmap14lem3 35150 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 35152* Simplify  ( A  \  { Q } ) in hdmap14lem3 35150 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 35151 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 35151 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 35153* 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 35154* Combine cases of  F. TODO: Can this be done at once in hdmap14lem3 35150, in order to get rid of hdmap14lem6 35153? Perhaps modify lspsneu 18274 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 35155 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 35156 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 35157 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 35158 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 35159* 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 35160* 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 35161* 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 35162* 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 35163 Extend class notation with g-map.
 class HGMap
 
Definitiondf-hgmap 35164* 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 35165* 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 35166* 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 35167* 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 35162. (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 35168 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 35169 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 35170 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 35171 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 35172 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 35173 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 35174 Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .+  =  ( +g  `  R )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   =>    |-  ( ph  ->  ( G `  ( X  .+  Y ) )  =  ( ( G `  X )  .+  ( G `
  Y ) ) )
 
Theoremhgmapmul 35175 Part 15 of [Baer] p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .x.  =  ( .r `  R )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   =>    |-  ( ph  ->  ( G `  ( X  .x.  Y ) )  =  ( ( G `  Y )  .x.  ( G `  X ) ) )
 
Theoremhgmaprnlem1N 35176 Lemma for hgmaprnN 35181. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  .xb  =  ( .s `  C )   &    |-  Q  =  ( 0g `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  z  e.  A )   &    |-  ( ph  ->  t  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  s  e.  V )   &    |-  ( ph  ->  ( S `  s )  =  ( z  .xb  ( S `  t ) ) )   &    |-  ( ph  ->  k  e.  B )   &    |-  ( ph  ->  s  =  ( k  .x.  t )
 )   =>    |-  ( ph  ->  z  e.  ran  G )
 
Theoremhgmaprnlem2N 35177 Lemma for hgmaprnN 35181. Part 15 of [Baer] p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero  z is taken care of automatically. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  .xb  =  ( .s `  C )   &    |-  Q  =  ( 0g `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  z  e.  A )   &    |-  ( ph  ->  t  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  s  e.  V )   &    |-  ( ph  ->  ( S `  s )  =  ( z  .xb  ( S `  t ) ) )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  N  =  (
 LSpan `  U )   &    |-  L  =  ( LSpan `  C )   =>    |-  ( ph  ->  ( N `  { s } )  C_  ( N `  { t } ) )
 
Theoremhgmaprnlem3N 35178* Lemma for hgmaprnN 35181. Eliminate  k. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  .xb  =  ( .s `  C )   &    |-  Q  =  ( 0g `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  z  e.  A )   &    |-  ( ph  ->  t  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  s  e.  V )   &    |-  ( ph  ->  ( S `  s )  =  ( z  .xb  ( S `  t ) ) )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  N  =  (
 LSpan `  U )   &    |-  L  =  ( LSpan `  C )   =>    |-  ( ph  ->  z  e.  ran  G )
 
Theoremhgmaprnlem4N 35179* Lemma for hgmaprnN 35181. Eliminate  s. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  .xb  =  ( .s `  C )   &    |-  Q  =  ( 0g `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  z  e.  A )   &    |-  ( ph  ->  t  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  z  e.  ran 
 G )
 
Theoremhgmaprnlem5N 35180 Lemma for hgmaprnN 35181. Eliminate  t. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  .xb  =  ( .s `  C )   &    |-  Q  =  ( 0g `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  z  e.  A )   =>    |-  ( ph  ->  z  e.  ran  G )
 
TheoremhgmaprnN 35181 Part of proof of part 16 in [Baer] p. 50 line 23, Fs=G, except that we use the original vector space scalars for the range. (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  ->  ran  G  =  B )
 
Theoremhgmap11 35182 The scalar sigma map is one-to-one. (Contributed by NM, 7-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  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   =>    |-  ( ph  ->  (
 ( G `  X )  =  ( G `  Y )  <->  X  =  Y ) )
 
Theoremhgmapf1oN 35183 The scalar sigma map is a one-to-one onto function. (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 : B -1-1-onto-> B )
 
Theoremhgmapeq0 35184 The scalar sigma map is zero iff its argument is zero. (Contributed by NM, 12-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .0.  =  ( 0g `  R )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  B )   =>    |-  ( ph  ->  (
 ( G `  X )  =  .0.  <->  X  =  .0.  ) )
 
Theoremhdmapipcl 35185 The inner product (Hermitian form)  ( X ,  Y
) will be defined as  ( ( S `  Y ) `  X ). Show closure. (Contributed by NM, 7-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\