HomeHome Metamath Proof Explorer
Theorem List (p. 354 of 402)
< 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-26575)
  Hilbert Space Explorer  Hilbert Space Explorer
(26576-28098)
  Users' Mathboxes  Users' Mathboxes
(28099-40159)
 

Theorem List for Metamath Proof Explorer - 35301-35400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremhvmapffval 35301* Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
 |-  H  =  ( LHyp `  K )   =>    |-  ( K  e.  X  ->  (HVMap `  K )  =  ( w  e.  H  |->  ( x  e.  ( (
 Base `  ( ( DVecH `  K ) `  w ) )  \  { ( 0g `  ( ( DVecH `  K ) `  w ) ) } )  |->  ( v  e.  ( Base `  ( ( DVecH `  K ) `  w ) )  |->  ( iota_ j  e.  ( Base `  (Scalar `  ( ( DVecH `  K ) `  w ) ) ) E. t  e.  ( ( ( ocH `  K ) `  w ) `  { x }
 ) v  =  ( t ( +g  `  (
 ( DVecH `  K ) `  w ) ) ( j ( .s `  ( ( DVecH `  K ) `  w ) ) x ) ) ) ) ) ) )
 
Theoremhvmapfval 35302* Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  (
 Base `  S )   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  A  /\  W  e.  H ) )   =>    |-  ( ph  ->  M  =  ( x  e.  ( V  \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ j  e.  R  E. t  e.  ( O `  { x } ) v  =  ( t  .+  (
 j  .x.  x )
 ) ) ) ) )
 
Theoremhvmapval 35303* Value of map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  (
 Base `  S )   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  A  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( M `  X )  =  ( v  e.  V  |->  (
 iota_ j  e.  R  E. t  e.  ( O `  { X }
 ) v  =  ( t  .+  ( j 
 .x.  X ) ) ) ) )
 
TheoremhvmapvalvalN 35304* Value of value of map (i.e. functional value) from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  (
 Base `  S )   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  A  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  (
 ( M `  X ) `  Y )  =  ( iota_ j  e.  R  E. t  e.  ( O `  { X }
 ) Y  =  ( t  .+  ( j 
 .x.  X ) ) ) )
 
TheoremhvmapidN 35305 The value of the vector to functional map, at the vector, is one. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .1.  =  ( 1r `  S )   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( ( M `  X ) `  X )  =  .1.  )
 
Theoremhvmap1o 35306* The vector to functional map provides a bijection from nonzero vectors  V to nonzero functionals with closed kernels  C. (Contributed by NM, 27-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( 0g `  D )   &    |-  C  =  { f  e.  F  |  ( O `
  ( O `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   =>    |-  ( ph  ->  M : ( V  \  {  .0.  } ) -1-1-onto-> ( C 
 \  { Q }
 ) )
 
TheoremhvmapclN 35307* Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( 0g `  D )   &    |-  C  =  { f  e.  F  |  ( O `
  ( O `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( M `  X )  e.  ( C  \  { Q } ) )
 
Theoremhvmap1o2 35308 The vector to functional map provides a bijection from nonzero vectors  V to nonzero functionals with closed kernels  C. (Contributed by NM, 27-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  O  =  ( 0g `  C )   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  M : ( V  \  {  .0.  } ) -1-1-onto-> ( F 
 \  { O }
 ) )
 
Theoremhvmapcl2 35309 Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  O  =  ( 0g `  C )   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( M `  X )  e.  ( F  \  { O } ) )
 
Theoremhvmaplfl 35310 The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( M `  X )  e.  F )
 
Theoremhvmaplkr 35311 Kernel of the vector to functional map. TODO: make this become lcfrlem11 35096. (Contributed by NM, 29-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  L  =  (LKer `  U )   &    |-  M  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( L `  ( M `
  X ) )  =  ( O `  { X } ) )
 
Theoremmapdhvmap 35312 Relationship between mapd and HVMap, which can be used to satify the last hypothesis of mapdpg 35249. Equation 10 of [Baer] p. 48. (Contributed by NM, 29-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  J  =  (
 LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  P  =  ( (HVMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { ( P `  X ) }
 ) )
 
Theoremlspindp5 35313 Obtain an independent vector set  U ,  X ,  Y from a vector 
U dependent on  X and  Z and another independent set  Z ,  X ,  Y. (Here we don't show the  ( N `  { X } )  =/=  ( N `  { Y } ) part of the independence, which passes straight through. We also don't show nonzero vector requirements that are redundant for this theorem. Different orderings can be obtained using lspexch 18357 and prcom 4084.) (Contributed by NM, 4-May-2015.)
 |-  V  =  ( Base `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  U  e.  V )   &    |-  ( ph  ->  Z  e.  ( N `  { X ,  U } ) )   &    |-  ( ph  ->  -.  Z  e.  ( N `  { X ,  Y } ) )   =>    |-  ( ph  ->  -.  U  e.  ( N `  { X ,  Y } ) )
 
Theoremhdmaplem1 35314 Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)
 |-  V  =  ( Base `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LMod )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  -.  Z  e.  ( ( N `  { X } )  u.  ( N `  { Y }
 ) ) )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  ( N `  { Z }
 )  =/=  ( N ` 
 { X } )
 )
 
Theoremhdmaplem2N 35315 Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LMod )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  -.  Z  e.  ( ( N `  { X } )  u.  ( N `  { Y }
 ) ) )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  ( N `  { Z }
 )  =/=  ( N ` 
 { Y } )
 )
 
Theoremhdmaplem3 35316 Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)
 |-  V  =  ( Base `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LMod )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  -.  Z  e.  ( ( N `  { X } )  u.  ( N `  { Y }
 ) ) )   &    |-  ( ph  ->  Y  e.  V )   &    |- 
 .0.  =  ( 0g `  W )   =>    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )
 
Theoremhdmaplem4 35317 Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)
 |-  V  =  ( Base `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { Z } )  =/=  ( N `  { X } ) )   &    |-  ( ph  ->  ( N `  { Z } )  =/=  ( N `  { Y } ) )   =>    |-  ( ph  ->  -.  Z  e.  ( ( N `  { X } )  u.  ( N `  { Y }
 ) ) )
 
Theoremmapdh8a 35318* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 5-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  T } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. X ,  F ,  T >. ) )
 
Theoremmapdh8aa 35319* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 12-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Z >. )  =  E )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { Z } )  =/=  ( N `  { T } ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  -.  Y  e.  ( N `
  { Z ,  T } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. Z ,  E ,  T >. ) )
 
Theoremmapdh8ab 35320* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Z >. )  =  E )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z }
 ) )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { X } )  =  ( N `  { T } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. Z ,  E ,  T >. ) )
 
Theoremmapdh8ac 35321* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Z >. )  =  E )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { X } )  =  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  w >. )  =  B )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { w }
 ) )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  w } ) )   &    |-  ( ph  ->  ( N `  { w } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { w ,  Z } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. Z ,  E ,  T >. ) )
 
Theoremmapdh8ad 35322* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Z >. )  =  E )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { X } )  =  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Z }
 ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. Z ,  E ,  T >. ) )
 
Theoremmapdh8b 35323* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { Y } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( I `  <. Y ,  G ,  w >. )  =  E )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { w } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =/=  ( N `  { w } ) )   &    |-  ( ph  ->  X  e.  ( N `  { Y ,  T } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  w } ) )   =>    |-  ( ph  ->  ( I `  <. w ,  E ,  T >. )  =  ( I `  <. Y ,  G ,  T >. ) )
 
Theoremmapdh8c 35324* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  w >. )  =  E )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =/=  ( N `  { T } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { w } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { w }
 ) )   &    |-  ( ph  ->  X  e.  ( N `  { Y ,  T }
 ) )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  w } ) )   =>    |-  ( ph  ->  ( I `  <. w ,  E ,  T >. )  =  ( I `  <. X ,  F ,  T >. ) )
 
Theoremmapdh8d0N 35325* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 10-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =/=  ( N `  { T } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { w } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { w }
 ) )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  w } ) )   &    |-  ( ph  ->  X  e.  ( N `  { Y ,  T } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. X ,  F ,  T >. ) )
 
Theoremmapdh8d 35326* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =/=  ( N `  { T } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { w } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { w }
 ) )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  w } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. X ,  F ,  T >. ) )
 
Theoremmapdh8e 35327* Part of Part (8) in [Baer] p. 48. Eliminate  w. (Contributed by NM, 10-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { T } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { T } ) )   &    |-  ( ph  ->  X  e.  ( N `  { Y ,  T } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. X ,  F ,  T >. ) )
 
Theoremmapdh8fN 35328* Part of Part (8) in [Baer] p. 48. Eliminate  w. TODO: this is an instance of mapdh8a 35318- delete this? (Contributed by NM, 10-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { T } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { T } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  T } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. X ,  F ,  T >. ) )
 
Theoremmapdh8g 35329* Part of Part (8) in [Baer] p. 48. Eliminate  X  e.  ( N `  { Y ,  T } ). TODO: break out  T  =/= 
.0. in mapdh8e 35327 so we can share hypotheses. Also, look at hypothesis sharing for earlier mapdh8* and mapdh75* stuff. (Contributed by NM, 10-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { T } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { T } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  T >. )  =  ( I `  <. X ,  F ,  T >. ) )
 
Theoremmapdh8i 35330* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 11-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Z }
 ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { Z } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { X } )  =/=  ( N `  { T } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  ( I `  <. X ,  F ,  Y >. ) ,  T >. )  =  ( I `  <. Z ,  ( I `  <. X ,  F ,  Z >. ) ,  T >. ) )
 
Theoremmapdh8j 35331* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Z }
 ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { Z } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  ( I `  <. X ,  F ,  Y >. ) ,  T >. )  =  ( I `
  <. Z ,  ( I `  <. X ,  F ,  Z >. ) ,  T >. ) )
 
Theoremmapdh8 35332* Part (8) in [Baer] p. 48. Given a reference vector  X, the value of function  I at a vector  T is independent of the choice of auxiliary vectors  Y and  Z. Unlike Baer's, our version does not require  X,  Y, and  Z to be independent, and also is defined for all  Y and  Z that are not colinear with  X or  T. We do this to make the definition of Baer's sigma function more straightforward. (This part eliminates  T  =/=  .0..) (Contributed by NM, 13-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Z }
 ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  ( N `  { Z } )  =/=  ( N `  { T }
 ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  ( I `  <. Y ,  ( I `  <. X ,  F ,  Y >. ) ,  T >. )  =  ( I `  <. Z ,  ( I `  <. X ,  F ,  Z >. ) ,  T >. ) )
 
Theoremmapdh9a 35333* Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 35334? (Contributed by NM, 14-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  E! y  e.  D  A. z  e.  V  ( -.  z  e.  (
 ( N `  { X } )  u.  ( N `  { T }
 ) )  ->  y  =  ( I `  <. z ,  ( I `  <. X ,  F ,  z >. ) ,  T >. ) ) )
 
Theoremmapdh9aOLDN 35334* Lemma for part (9) in [Baer] p. 48. (Contributed by NM, 14-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  E! y  e.  D  A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T } )  ->  y  =  ( I `  <. z ,  ( I `  <. X ,  F ,  z >. ) ,  T >. ) ) )
 
Syntaxchdma1 35335 Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space.
 class HDMap1
 
Syntaxchdma 35336 Extend class notation with map from vectors to functionals in the closed kernel dual space.
 class HDMap
 
Definitiondf-hdmap1 35337* Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 35340 description for more details. (Contributed by NM, 14-May-2015.)
 |- HDMap1  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { a  |  [. ( ( DVecH `  k ) `  w )  /  u ]. [. ( Base `  u )  /  v ]. [. ( LSpan `  u )  /  n ].
 [. ( (LCDual `  k
 ) `  w )  /  c ]. [. ( Base `  c )  /  d ]. [. ( LSpan `  c )  /  j ]. [. ( (mapd `  k ) `  w )  /  m ]. a  e.  ( x  e.  (
 ( v  X.  d
 )  X.  v )  |->  if ( ( 2nd `  x )  =  ( 0g `  u ) ,  ( 0g `  c ) ,  ( iota_ h  e.  d  (
 ( m `  ( n `  { ( 2nd `  x ) } )
 )  =  ( j `
  { h }
 )  /\  ( m `  ( n `  { (
 ( 1st `  ( 1st `  x ) ) (
 -g `  u )
 ( 2nd `  x )
 ) } ) )  =  ( j `  { ( ( 2nd `  ( 1st `  x ) ) ( -g `  c ) h ) } ) ) ) ) ) } )
 )
 
Definitiondf-hdmap 35338* Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 35373 description for more details. (Contributed by NM, 15-May-2015.)
 |- HDMap  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { a  |  [. <. (  _I  |`  ( Base `  k ) ) ,  (  _I  |`  ( (
 LTrn `  k ) `  w ) ) >.  /  e ]. [. (
 ( DVecH `  k ) `  w )  /  u ].
 [. ( Base `  u )  /  v ]. [. (
 (HDMap1 `  k ) `  w )  /  i ]. a  e.  (
 t  e.  v  |->  (
 iota_ y  e.  ( Base `  ( (LCDual `  k
 ) `  w )
 ) A. z  e.  v  ( -.  z  e.  (
 ( ( LSpan `  u ) `  { e }
 )  u.  ( (
 LSpan `  u ) `  { t } )
 )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e ) ,  z >. ) ,  t >. ) ) ) ) } ) )
 
Theoremhdmap1ffval 35339* Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015.)
 |-  H  =  ( LHyp `  K )   =>    |-  ( K  e.  X  ->  (HDMap1 `  K )  =  ( w  e.  H  |->  { a  |  [. (
 ( DVecH `  K ) `  w )  /  u ].
 [. ( Base `  u )  /  v ]. [. ( LSpan `  u )  /  n ]. [. ( (LCDual `  K ) `  w )  /  c ]. [. ( Base `  c )  /  d ]. [. ( LSpan `  c )  /  j ]. [. ( (mapd `  K ) `  w )  /  m ]. a  e.  ( x  e.  (
 ( v  X.  d
 )  X.  v )  |->  if ( ( 2nd `  x )  =  ( 0g `  u ) ,  ( 0g `  c ) ,  ( iota_ h  e.  d  (
 ( m `  ( n `  { ( 2nd `  x ) } )
 )  =  ( j `
  { h }
 )  /\  ( m `  ( n `  { (
 ( 1st `  ( 1st `  x ) ) (
 -g `  u )
 ( 2nd `  x )
 ) } ) )  =  ( j `  { ( ( 2nd `  ( 1st `  x ) ) ( -g `  c ) h ) } ) ) ) ) ) } )
 )
 
Theoremhdmap1fval 35340* Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span  J to the convention  L for this section. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  A  /\  W  e.  H ) )   =>    |-  ( ph  ->  I  =  ( x  e.  (
 ( V  X.  D )  X.  V )  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) ) )
 
Theoremhdmap1vallem 35341* Value of preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  A  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  ( ( V  X.  D )  X.  V ) )   =>    |-  ( ph  ->  ( I `  T )  =  if ( ( 2nd `  T )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  T ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  T ) )  .-  ( 2nd `  T ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  T ) ) R h ) } )
 ) ) ) )
 
Theoremhdmap1val 35342* Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 35267.) TODO: change  I  =  ( x  e.  _V  |->... to  ( ph  ->  ( I `  <. X ,  F ,  Y  >  )  =... in e.g. mapdh8 35332 to shorten proofs with no $d on  x. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  A  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  if ( Y  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( F R h ) }
 ) ) ) ) )
 
Theoremhdmap1val0 35343 Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 35268.) (Contributed by NM, 17-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  .0.  >. )  =  Q )
 
Theoremhdmap1val2 35344* Value of preliminary map from vectors to functionals in the closed kernel dual space, for nonzero  Y. (Contributed by NM, 16-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  (
 iota_ h  e.  D  ( ( M `  ( N `  { Y } ) )  =  ( L `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( L `
  { ( F R h ) }
 ) ) ) )
 
Theoremhdmap1eq 35345 The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 16-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  G  e.  D )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( L `  { F } ) )   =>    |-  ( ph  ->  ( ( I `  <. X ,  F ,  Y >. )  =  G  <->  ( ( M `  ( N `  { Y }
 ) )  =  ( L `  { G } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( L `
  { ( F R G ) }
 ) ) ) )
 
Theoremhdmap1cbv 35346* Frequently used lemma to change bound variables in  L hypothesis. (Contributed by NM, 15-May-2015.)
 |-  L  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   =>    |-  L  =  ( y  e.  _V  |->  if ( ( 2nd `  y )  =  .0. 
 ,  Q ,  ( iota_
 i  e.  D  ( ( M `  ( N `  { ( 2nd `  y ) } )
 )  =  ( J `
  { i }
 )  /\  ( M `  ( N `  { (
 ( 1st `  ( 1st `  y ) )  .-  ( 2nd `  y )
 ) } ) )  =  ( J `  { ( ( 2nd `  ( 1st `  y
 ) ) R i ) } ) ) ) ) )
 
Theoremhdmap1valc 35347* Connect the value of the preliminary map from vectors to functionals  I to the hypothesis  L used by earlier theorems. Note: the  X  e.  ( V  \  {  .0.  } ) hypothesis could be the more general  X  e.  V but the former will be easier to use. TODO: use the  I function directly in those theorems, so this theorem becomes unnecessary? TODO: The hdmap1cbv 35346 is probably unnecessary, but it would mean different $d's later on. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  Y  e.  V )   &    |-  L  =  ( x  e.  _V  |->  if ( ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  ( L `  <. X ,  F ,  Y >. ) )
 
Theoremhdmap1cl 35348 Convert closure theorem mapdhcl 35270 to use HDMap1 function. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  e.  D )
 
Theoremhdmap1eq2 35349 Convert mapdheq2 35272 to use HDMap1 function. (Contributed by NM, 16-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  X >. )  =  F )
 
Theoremhdmap1eq4N 35350 Convert mapdheq4 35275 to use HDMap1 function. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z }
 ) )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Z >. )  =  B )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  Z >. )  =  B )
 
Theoremhdmap1l6lem1 35351 Lemma for hdmap1l6 35365. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Z >. )  =  E )   =>    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  ( Y  .+  Z ) ) } ) )  =  ( L `  { ( F R ( G  .+b  E ) ) } ) )
 
Theoremhdmap1l6lem2 35352 Lemma for hdmap1l6 35365. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Z >. )  =  E )   =>    |-  ( ph  ->  ( M `  ( N `  { ( Y  .+  Z ) } )
 )  =  ( L `
  { ( G 
 .+b  E ) } )
 )
 
Theoremhdmap1l6a 35353 Lemma for hdmap1l6 35365. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Z >. )  =  E )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. ) 
 .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6b0N 35354 Lemmma for hdmap1l6 35365. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  ( ( N `  { X } )  i^i  ( N `
  { Y ,  Z } ) )  =  {  .0.  } )   =>    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )
 
Theoremhdmap1l6b 35355 Lemmma for hdmap1l6 35365. (Contributed by NM, 24-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  =  .0.  )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. ) 
 .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6c 35356 Lemmma for hdmap1l6 35365. (Contributed by NM, 24-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  =  .0.  )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6d 35357 Lemmma for hdmap1l6 35365. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( w  .+  ( Y  .+  Z ) ) >. )  =  ( ( I `  <. X ,  F ,  w >. )  .+b  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. ) ) )
 
Theoremhdmap1l6e 35358 Lemmma for hdmap1l6 35365. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( ( w  .+  Y )  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  ( w  .+  Y )
 >. )  .+b  ( I `
  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6f 35359 Lemmma for hdmap1l6 35365. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( w  .+  Y ) >. )  =  ( ( I `  <. X ,  F ,  w >. )  .+b  ( I `  <. X ,  F ,  Y >. ) ) )
 
Theoremhdmap1l6g 35360 Lemmma for hdmap1l6 35365. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-