HomeHome Metamath Proof Explorer
Theorem List (p. 321 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-21811)
  Hilbert Space Explorer  Hilbert Space Explorer
(21812-23334)
  Users' Mathboxes  Users' Mathboxes
(23335-32225)
 

Theorem List for Metamath Proof Explorer - 32001-32100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmapdh6eN 32001* Lemmma for mapdh6N 32008. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
 |-  Q  =  ( 0g `  C )   &    |-  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 ) } )
 ) ) ) )   &    |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  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 )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  .+  =  ( +g  `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( 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 >. ) ) )
 
Theoremmapdh6fN 32002* Lemmma for mapdh6N 32008. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
 |-  Q  =  ( 0g `  C )   &    |-  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 ) } )
 ) ) ) )   &    |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  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 )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  .+  =  ( +g  `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( 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 >. ) ) )
 
Theoremmapdh6gN 32003* Lemmma for mapdh6N 32008. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
 |-  Q  =  ( 0g `  C )   &    |-  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 ) } )
 ) ) ) )   &    |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  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 )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  .+  =  ( +g  `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( 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 >. ) 
 .+b  ( I `  <. X ,  F ,  ( Y  .+  Z )
 >. ) )  =  ( ( ( I `  <. X ,  F ,  w >. )  .+b  ( I `  <. X ,  F ,  Y >. ) )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremmapdh6hN 32004* Lemmma for mapdh6N 32008. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
 |-  Q  =  ( 0g `  C )   &    |-  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 ) } )
 ) ) ) )   &    |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  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 )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  .+  =  ( +g  `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremmapdh6iN 32005* Lemmma for mapdh6N 32008. Eliminate auxiliary vector  w. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
 |-  Q  =  ( 0g `  C )   &    |-  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 ) } )
 ) ) ) )   &    |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  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 )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  .+  =  ( +g  `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremmapdh6jN 32006* Lemmma for mapdh6N 32008. Eliminate  ( N { Y } ) = ( N  { Z } ) hypothesis. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
 |-  Q  =  ( 0g `  C )   &    |-  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 ) } )
 ) ) ) )   &    |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  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 )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  .+  =  ( +g  `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. ) 
 .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremmapdh6kN 32007* Lemmma for mapdh6N 32008. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
 |-  Q  =  ( 0g `  C )   &    |-  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 ) } )
 ) ) ) )   &    |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  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 )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  .+  =  ( +g  `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremmapdh6N 32008* Part (6) of [Baer] p. 47 line 6. Note that we use  -.  X  e.  ( N `  { Y ,  Z }
) which is equivalent to Baer's "Fx  i^i (Fy + Fz)" by lspdisjb 16089. TODO: If $ds with  I and  ph becomes a problem later, cbv's on  I variables here to get rid of them. . Maybe reorder hypotheses in lemmas to the more consistent order of this theorem, so they can be shared with this theorem. (Contributed by NM, 1-May-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 )   &    |-  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  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremmapdh7eN 32009* Part (7) of [Baer] p. 48 line 10 (5 of 6 cases). (Note: 1 of 6 and 2 of 6 are hypotheses a and b.) (Contributed by NM, 2-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 `  { u } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  u  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  v  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { u } )  =/=  ( N `  { v }
 ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { u ,  v } ) )   &    |-  ( ph  ->  ( I `  <. u ,  F ,  w >. )  =  E )   =>    |-  ( ph  ->  ( I `  <. w ,  E ,  u >. )  =  F )
 
Theoremmapdh7cN 32010* Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-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 `  { u } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  u  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  v  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { u } )  =/=  ( N `  { v }
 ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { u ,  v } ) )   &    |-  ( ph  ->  ( I `  <. u ,  F ,  v >. )  =  G )   =>    |-  ( ph  ->  ( I `  <. v ,  G ,  u >. )  =  F )
 
Theoremmapdh7dN 32011* Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-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 `  { u } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  u  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  v  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { u } )  =/=  ( N `  { v }
 ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { u ,  v } ) )   &    |-  ( ph  ->  ( I `  <. u ,  F ,  v >. )  =  G )   &    |-  ( ph  ->  ( I `  <. u ,  F ,  w >. )  =  E )   =>    |-  ( ph  ->  ( I `  <. v ,  G ,  w >. )  =  E )
 
Theoremmapdh7fN 32012* Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-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 `  { u } ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  u  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  v  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { u } )  =/=  ( N `  { v }
 ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { u ,  v } ) )   &    |-  ( ph  ->  ( I `  <. u ,  F ,  v >. )  =  G )   &    |-  ( ph  ->  ( I `  <. u ,  F ,  w >. )  =  E )   =>    |-  ( ph  ->  ( I `  <. w ,  E ,  v >. )  =  G )
 
Theoremmapdh75e 32013* Part (7) of [Baer] p. 48 line 10 (5 of 6 cases).  X,  Y,  Z are Baer's u, v, w. (Note: Cases 1 of 6 and 2 of 6 are hypotheses mapdh75b here and mapdh75a in mapdh75cN 32014.) (Contributed by NM, 2-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 ,  Z >. )  =  E )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Z } )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( I `  <. Z ,  E ,  X >. )  =  F )
 
Theoremmapdh75cN 32014* Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-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  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  X >. )  =  F )
 
Theoremmapdh75d 32015* Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-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  ->  ( N `  { Y }
 )  =/=  ( N ` 
 { Z } )
 )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( I `  <. Y ,  G ,  Z >. )  =  E )
 
Theoremmapdh75fN 32016* Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-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  ->  ( I `  <. X ,  F ,  Z >. )  =  E )   &    |-  ( ph  ->  ( N `  { Y }
 )  =/=  ( N ` 
 { Z } )
 )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( I `  <. Z ,  E ,  Y >. )  =  G )
 
Syntaxchvm 32017 Extend class notation with vector to dual map.
 class HVMap
 
Definitiondf-hvmap 32018* Extend class notation with a map from each nonzero vector  x to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier e.g. lcf1o 31812, dochfl1 31737- should we update those to use this definition? (Contributed by NM, 23-Mar-2015.)
 |- HVMap  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( 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 ) ) ) ) ) ) )
 
Theoremhvmapffval 32019* 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 32020* 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 32021* 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 32022* 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 32023 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 32024* 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 32025* 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 32026 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 32027 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 32028 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 32029 Kernel of the vector to functional map. TODO: make this become lcfrlem11 31814. (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 32030 Relationship between mapd and HVMap, which can be used to satify the last hypothesis of mapdpg 31967. 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 32031 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 16092 and prcom 3797.) (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 32032 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 32033 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 32034 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 32035 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 32036* 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 32037* 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 32038* 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 32039* 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 32040* 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 32041* 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 32042* 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 32043* 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 32044* 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 32045* 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 32046* Part of Part (8) in [Baer] p. 48. Eliminate  w. TODO: this is an instance of mapdh8a 32036- 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 32047* Part of Part (8) in [Baer] p. 48. Eliminate  X  e.  ( N `  { Y ,  T } ). TODO: break out  T  =/= 
.0. in mapdh8e 32045 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 32048* 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 32049* 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 32050* 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 32051* Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 32052? (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 32052* 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  =