HomeHome Metamath Proof Explorer
Theorem List (p. 314 of 315)
< 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-21494)
  Hilbert Space Explorer  Hilbert Space Explorer
(21495-23017)
  Users' Mathboxes  Users' Mathboxes
(23018-31433)
 

Theorem List for Metamath Proof Explorer - 31301-31400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
TheoremhdmapfnN 31301 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 31302 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 31303* Lemma for hdmapval2 31304. (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 31304 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 31240 through hdmaplem4 31243, 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 31305 Value of map from vectors to functionals at zero. Note: we use dvh3dim 30915 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 31316 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 31306 Lemma for hdmapevec 31307. TODO: combine with hdmapevec 31307 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 31307 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 31308 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 31309 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 31310 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 31311 Lemma for hdmap10 31312. (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 31312 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 31313 Lemma for hdmapadd 31315. (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 31314 Lemma for hdmapadd 31315. (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 31315 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 31316 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 31317 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 31318 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 31319 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 31320 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 31321 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 31322 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 31323 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 31324 Lemma for hdmaprnN 31336. 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 31325 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 31326 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 31327 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 31328 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 31329 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 31108 and mapdcnv11N 31128. 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 31330* Lemma for hdmaprnN 31336. (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 31331* Lemma for hdmaprnN 31336. 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 31332* Lemma for hdmaprnN 31336. 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 31333* Lemma for hdmaprnN 31336. 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 31334 Lemma for hdmaprnN 31336. 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 31335 Lemma for hdmaprnN 31336. 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 31336 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 31337 Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 31315, 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 31338 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 31339* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  .0. so it can be used in hdmap14lem10 31349. (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 31340 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 31341* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  Z so it can be used in hdmap14lem10 31349. (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 31342* 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 31343* Simplify  ( A  \  { Q } ) in hdmap14lem3 31342 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 31344* Simplify  ( A  \  { Q } ) in hdmap14lem3 31342 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 31343 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 31343 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 31345* 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 31346* Combine cases of  F. TODO: Can this be done at once in hdmap14lem3 31342, in order to get rid of hdmap14lem6 31345? Perhaps modify lspsneu 15872 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 31347 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 31348 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 31349 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 31350 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 31351* 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 31352* 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 31353* 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 31354* 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 31355 Extend class notation with g-map.
 class HGMap
 
Definitiondf-hgmap 31356* 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 31357* 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 31358* 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 31359* 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 31354. (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 31360 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 31361 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 31362 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 31363 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 31364 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 31365 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 31366 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 31367 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 31368 Lemma for hgmaprnN 31373. (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 31369 Lemma for hgmaprnN 31373. 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 31370* Lemma for hgmaprnN 31373. 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 31371* Lemma for hgmaprnN 31373. 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 31372 Lemma for hgmaprnN 31373. 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 31373 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 31374 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 31375 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 31376 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 31377 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  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  (
 ( S `  Y ) `  X )  e.  B )
 
Theoremhdmapln1 31378 Linearity property that will be used for inner product. TODO: try to combine hypotheses in hdmap*ln* series. (Contributed by NM, 7-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .+^  =  ( +g  `  R )   &    |-  .X.  =  ( .r `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  A  e.  B )   =>    |-  ( ph  ->  ( ( S `  Z ) `  ( ( A 
 .x.  X )  .+  Y ) )  =  (
 ( A  .X.  (
 ( S `  Z ) `  X ) )  .+^  ( ( S `  Z ) `  Y ) ) )
 
Theoremhdmaplna1 31379 Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  R  =  (Scalar `  U )   &    |-  .+^  =  (
 +g  `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   =>    |-  ( ph  ->  (
 ( S `  Z ) `  ( X  .+  Y ) )  =  ( ( ( S `
  Z ) `  X )  .+^  ( ( S `  Z ) `
  Y ) ) )
 
Theoremhdmaplns1 31380 Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  N  =  ( -g `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   =>    |-  ( ph  ->  (
 ( S `  Z ) `  ( X  .-  Y ) )  =  ( ( ( S `
  Z ) `  X ) N ( ( S `  Z ) `  Y ) ) )
 
Theoremhdmaplnm1 31381 Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .X.  =  ( .r `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  A  e.  B )   =>    |-  ( ph  ->  (
 ( S `  Y ) `  ( A  .x.  X ) )  =  ( A  .X.  ( ( S `  Y ) `  X ) ) )
 
Theoremhdmaplna2 31382 Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  R  =  (Scalar `  U )   &    |-  .+^  =  (
 +g  `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   =>    |-  ( ph  ->  (
 ( S `  ( Y  .+  Z ) ) `
  X )  =  ( ( ( S `
  Y ) `  X )  .+^  ( ( S `  Z ) `
  X ) ) )
 
Theoremhdmapglnm2 31383 g-linear property of second (inner product) argument. Line 19 in [Holland95] p. 14. (Contributed by NM, 10-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .X.  =  ( .r `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  A  e.  B )   =>    |-  ( ph  ->  (
 ( S `  ( A  .x.  Y ) ) `
  X )  =  ( ( ( S `
  Y ) `  X )  .X.  ( G `
  A ) ) )
 
Theoremhdmapgln2 31384 g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .+^  =  ( +g  `  R )   &    |-  .X.  =  ( .r `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  A  e.  B )   =>    |-  ( ph  ->  ( ( S `  (
 ( A  .x.  Y )  .+  Z ) ) `
  X )  =  ( ( ( ( S `  Y ) `
  X )  .X.  ( G `  A ) )  .+^  ( ( S `  Z ) `  X ) ) )
 
Theoremhdmaplkr 31385 Kernel of the vector to dual map. Line 16 in [Holland95] p. 14. TODO: eliminate  F hypothesis. (Contributed by NM, 9-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  F  =  (LFnl `  U )   &    |-  Y  =  (LKer `  U )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  ( Y `  ( S `
  X ) )  =  ( O `  { X } ) )
 
Theoremhdmapellkr 31386 Membership in the kernel (as shown by hdmaplkr 31385) of the vector to dual map. Line 17 in [Holland95] p. 14. (Contributed by NM, 16-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  .0.  =  ( 0g `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  (
 ( ( S `  X ) `  Y )  =  .0.  <->  Y  e.  ( O `  { X }
 ) ) )
 
Theoremhdmapip0 31387 Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  Z  =  ( 0g
 `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  ( ( ( S `  X ) `  X )  =  Z  <->  X  =  .0.  ) )
 
Theoremhdmapip1 31388 Construct a proportional vector  Y whose inner product with the original  X equals one. (Contributed by NM, 13-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  .1.  =  ( 1r `  R )   &    |-  N  =  ( invr `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  Y  =  ( ( N `  ( ( S `  X ) `  X ) )  .x.  X )   =>    |-  ( ph  ->  ( ( S `  X ) `  Y )  =  .1.  )
 
Theoremhdmapip0com 31389 Commutation property of Baer's sigma map (Holland's A map). Line 20 of [Holland95] p. 14. Also part of Lemma 1 of [Baer] p. 110 line 7. (Contributed by NM, 9-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  .0.  =  ( 0g `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  (
 ( ( S `  X ) `  Y )  =  .0.  <->  ( ( S `
  Y ) `  X )  =  .0.  ) )
 
Theoremhdmapinvlem1 31390 Line 27 in [Baer] p. 110. We use  C for Baer's u. Our unit vector  E has the required properties for his w by hdmapevec2 31308. Our  ( ( S `  E ) `  C ) means the inner product  <. C ,  E >. i.e. his f(u,w) (note argument reversal). (Contributed by NM, 11-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .x.  =  ( .r `  R )   &    |-  .0.  =  ( 0g `  R )   &    |-  S  =  ( (HDMap `  K ) `