HomeHome Metamath Proof Explorer
Theorem List (p. 323 of 325)
< 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-22374)
  Hilbert Space Explorer  Hilbert Space Explorer
(22375-23897)
  Users' Mathboxes  Users' Mathboxes
(23898-32447)
 

Theorem List for Metamath Proof Explorer - 32201-32300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorembaerlem5abmN 32201 An equality that holds when  X,  Y,  Z are independent (non-colinear) vectors. Subtraction versions of first and second equations of part (5) in [Baer] p. 46, conjoined to share commonality in their proofs. TODO: Delete if not be needed. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   =>    |-  ( ph  ->  (
 ( N `  { ( X  .-  ( Y  .-  Z ) ) }
 )  =  ( ( ( N `  { ( X  .-  Y ) }
 )  .(+)  ( N `  { Z } ) )  i^i  ( ( N `
  { ( X 
 .+  Z ) }
 )  .(+)  ( N `  { Y } ) ) )  /\  ( N `
  { ( Y 
 .-  Z ) }
 )  =  ( ( ( N `  { Y } )  .(+)  ( N `
  { Z }
 ) )  i^i  (
 ( N `  { ( X  .-  ( Y  .-  Z ) ) }
 )  .(+)  ( N `  { X } ) ) ) ) )
 
Theoremmapdindp0 32202 Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .+  =  ( +g  `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =  ( N `  { Z }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   &    |-  ( ph  ->  ( Y  .+  Z )  =/=  .0.  )   =>    |-  ( ph  ->  ( N `  { ( Y  .+  Z ) } )  =  ( N `  { Y } ) )
 
Theoremmapdindp1 32203 Vector independence lemma. (Contributed by NM, 1-May-2015.)
 |-  V  =  ( Base `  W )   &    |-  .+  =  ( +g  `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =  ( N `  { Z }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { ( Y 
 .+  Z ) }
 ) )
 
Theoremmapdindp2 32204 Vector independence lemma. (Contributed by NM, 1-May-2015.)
 |-  V  =  ( Base `  W )   &    |-  .+  =  ( +g  `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =  ( N `  { Z }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  ( Y  .+  Z ) } ) )
 
Theoremmapdindp3 32205 Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .+  =  ( +g  `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =  ( N `  { Z }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { ( w 
 .+  Y ) }
 ) )
 
Theoremmapdindp4 32206 Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .+  =  ( +g  `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =  ( N `  { Z }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  -.  Z  e.  ( N `
  { X ,  ( w  .+  Y ) } ) )
 
Theoremmapdhval 32207* Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 6-May-2015.)
 |-  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 ) } )
 ) ) ) )   &    |-  ( ph  ->  X  e.  A )   &    |-  ( ph  ->  F  e.  B )   &    |-  ( ph  ->  Y  e.  E )   =>    |-  ( 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 ) }
 ) ) ) ) )
 
Theoremmapdhval0 32208* Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
 |-  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 ) } )
 ) ) ) )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  e.  A )   &    |-  ( ph  ->  F  e.  B )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  .0.  >. )  =  Q )
 
Theoremmapdhval2 32209* Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
 |-  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 ) } )
 ) ) ) )   &    |-  ( ph  ->  X  e.  A )   &    |-  ( ph  ->  F  e.  B )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  (
 iota_ h  e.  D ( ( M `  ( N `  { Y } ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( F R h ) }
 ) ) ) )
 
Theoremmapdhcl 32210* Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
 |-  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.  }
 ) )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  e.  D )
 
Theoremmapdheq 32211* Lemmma for ~? mapdh . The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 4-Apr-2015.)
 |-  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.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  G  e.  D )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   =>    |-  ( ph  ->  (
 ( I `  <. X ,  F ,  Y >. )  =  G  <->  ( ( M `
  ( N `  { Y } ) )  =  ( J `  { G } )  /\  ( M `  ( N `
  { ( X 
 .-  Y ) }
 ) )  =  ( J `  { ( F R G ) }
 ) ) ) )
 
Theoremmapdheq2 32212* Lemmma for ~? mapdh . One direction of part (2) in [Baer] p. 45. (Contributed by NM, 4-Apr-2015.)
 |-  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.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  G  e.  D )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   =>    |-  ( ph  ->  (
 ( I `  <. X ,  F ,  Y >. )  =  G  ->  ( I `  <. Y ,  G ,  X >. )  =  F ) )
 
Theoremmapdheq2biN 32213* Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 32212 seems to require an additional hypothesis not mentioned in Baer. TODO fix ref. TODO: We probably don't need this; delete if never used. (Contributed by NM, 4-Apr-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.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  G  e.  D )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { Y }
 ) )  =  ( J `  { G } ) )   =>    |-  ( ph  ->  ( ( I `  <. X ,  F ,  Y >. )  =  G  <->  ( I `  <. Y ,  G ,  X >. )  =  F ) )
 
Theoremmapdheq4lem 32214* Lemma for mapdheq4 32215. Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
 |-  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.  }
 ) )   &    |-  ( 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 ) } )
 )  =  ( J `
  { ( G R E ) }
 ) )
 
Theoremmapdheq4 32215* Lemma for ~? mapdh . Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
 |-  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.  }
 ) )   &    |-  ( 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 `  <. Y ,  G ,  Z >. )  =  E )
 
Theoremmapdh6lem1N 32216* Lemma for mapdh6N 32230. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-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  \  {  .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 ) ) } ) )  =  ( J `  { ( F R ( G  .+b  E ) ) } ) )
 
Theoremmapdh6lem2N 32217* Lemma for mapdh6N 32230. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-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  \  {  .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 ) } )
 )  =  ( J `
  { ( G 
 .+b  E ) } )
 )
 
Theoremmapdh6aN 32218* Lemma for mapdh6N 32230. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-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  \  {  .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 >. ) ) )
 
Theoremmapdh6b0N 32219* Lemmma for mapdh6N 32230. (Contributed by NM, 23-Apr-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  ->  ( ( N `  { X } )  i^i  ( N `
  { Y ,  Z } ) )  =  {  .0.  } )   =>    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )
 
Theoremmapdh6bN 32220* Lemmma for mapdh6N 32230. (Contributed by NM, 24-Apr-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  =  .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 >. ) ) )
 
Theoremmapdh6cN 32221* Lemmma for mapdh6N 32230. (Contributed by NM, 24-Apr-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  =  .0.  )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremmapdh6dN 32222* Lemmma for mapdh6N 32230. (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 >. )  .+b  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. ) ) )
 
Theoremmapdh6eN 32223* Lemmma for mapdh6N 32230. 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 32224* Lemmma for mapdh6N 32230. 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 32225* Lemmma for mapdh6N 32230. 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 32226* Lemmma for mapdh6N 32230. 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 32227* Lemmma for mapdh6N 32230. 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 32228* Lemmma for mapdh6N 32230. 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 32229* Lemmma for mapdh6N 32230. 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 32230* 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 16153. 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 32231* 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 32232* 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 32233* 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 32234* 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 32235* 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 32236.) (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 32236* 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 32237* 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 32238* 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 32239 Extend class notation with vector to dual map.
 class HVMap
 
Definitiondf-hvmap 32240* 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 32034, dochfl1 31959- 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 32241* 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 32242* 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 32243* 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 32244* 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 32245 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 32246* 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 32247* 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 32248 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 32249 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 32250 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 32251 Kernel of the vector to functional map. TODO: make this become lcfrlem11 32036. (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 32252 Relationship between mapd and HVMap, which can be used to satify the last hypothesis of mapdpg 32189. 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 32253 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 16156 and prcom 3842.) (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 32254 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 32255 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 32256 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 32257 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 32258* 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  \  {