HomeHome Metamath Proof Explorer
Theorem List (p. 322 of 323)
< 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-21500)
  Hilbert Space Explorer  Hilbert Space Explorer
(21501-23023)
  Users' Mathboxes  Users' Mathboxes
(23024-32227)
 

Theorem List for Metamath Proof Explorer - 32101-32200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremhdmapevec 32101 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 32102 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 32103 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 32104 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 32105 Lemma for hdmap10 32106. (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 32106 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 32107 Lemma for hdmapadd 32109. (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 32108 Lemma for hdmapadd 32109. (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 32109 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 32110 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 32111 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 32112 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 32113 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 32114 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 32115 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 32116 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 32117 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 32118 Lemma for hdmaprnN 32130. 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 32119 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 32120 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 32121 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 32122 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 32123 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 31902 and mapdcnv11N 31922. 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 32124* Lemma for hdmaprnN 32130. (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 32125* Lemma for hdmaprnN 32130. 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 32126* Lemma for hdmaprnN 32130. 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 32127* Lemma for hdmaprnN 32130. 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 32128 Lemma for hdmaprnN 32130. 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 32129 Lemma for hdmaprnN 32130. 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 32130 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 32131 Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 32109, 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 32132 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 32133* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  .0. so it can be used in hdmap14lem10 32143. (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 32134 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 32135* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  Z so it can be used in hdmap14lem10 32143. (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 32136* 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 32137* Simplify  ( A  \  { Q } ) in hdmap14lem3 32136 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 32138* Simplify  ( A  \  { Q } ) in hdmap14lem3 32136 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 32137 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 32137 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 32139* 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 32140* Combine cases of  F. TODO: Can this be done at once in hdmap14lem3 32136, in order to get rid of hdmap14lem6 32139? Perhaps modify lspsneu 15878 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 32141 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 32142 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 32143 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 32144 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 32145* 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 32146* 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 32147* 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 32148* 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 32149 Extend class notation with g-map.
 class HGMap
 
Definitiondf-hgmap 32150* 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 32151* 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 32152* 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 32153* 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 32148. (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 32154 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 32155 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 32156 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 32157 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 32158 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 32159 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 32160 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 32161 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 32162 Lemma for hgmaprnN 32167. (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 32163 Lemma for hgmaprnN 32167. 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 32164* Lemma for hgmaprnN 32167. 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 32165* Lemma for hgmaprnN 32167. 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 32166 Lemma for hgmaprnN 32167. 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 32167 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 32168 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 32169 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 32170 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 32171 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 32172 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 32173 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 32174 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 32175 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 32176 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 32177 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 32178 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 32179 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 32180 Membership in the kernel (as shown by hdmaplkr 32179) 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 32181 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 32182 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 32183 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 32184 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 32102. 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 ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  C  e.  ( O `  { E } ) )   =>    |-  ( ph  ->  ( ( S `  E ) `  C )  =  .0.  )
 
Theoremhdmapinvlem2 32185 Line 28 in [Baer] p. 110, 0 = f(w,u). (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 ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  C  e.  ( O `  { E } ) )   =>    |-  ( ph  ->  ( ( S `  C ) `  E )  =  .0.  )
 
Theoremhdmapinvlem3 32186 Line 30 in [Baer] p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .x. 
 =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  .X.  =  ( .r `  R )   &    |-  .0.  =  ( 0g `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  C  e.  ( O `  { E } ) )   &    |-  ( ph  ->  D  e.  ( O `  { E }
 ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  ( ph  ->  J  e.  B )   &    |-  ( ph  ->  ( I  .X.  ( G `  J ) )  =  ( ( S `  D ) `  C ) )   =>    |-  ( ph  ->  (
 ( S `  (
 ( J  .x.  E )  .-  D ) ) `
  ( ( I 
 .x.  E )  .+  C ) )  =  .0.  )
 
Theoremhdmapinvlem4 32187 Part 1.1 of Proposition 1 of [Baer] p. 110. We use  C,  D,  I, and  J for Baer's u, v, s, and t. Our unit vector  E has the required properties for his w by hdmapevec2 32102. Our  ( ( S `  D ) `  C ) means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .x. 
 =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  .X.  =  ( .r `  R )   &    |-  .0.  =  ( 0g `  R )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  G  =  ( (HGMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  C  e.  ( O `  { E } ) )   &    |-  ( ph  ->  D  e.  ( O `  { E }
 ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  ( ph  ->  J  e.  B )   &    |-  ( ph  ->  ( I  .X.  ( G `  J ) )  =  ( ( S `  D ) `  C ) )   =>    |-  ( ph  ->  ( J  .X.  ( G `  I ) )  =  ( ( S `  C ) `  D ) )
 
Theoremhdmapglem5 32188 Part 1.2 in [Baer] p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .x. 
 =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  .X.  =  ( .r `  R )   &    |-  .0.  =  ( 0g