HomeHome Metamath Proof Explorer
Theorem List (p. 309 of 310)
< 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-21328)
  Hilbert Space Explorer  Hilbert Space Explorer
(21329-22851)
  Users' Mathboxes  Users' Mathboxes
(22852-30955)
 

Theorem List for Metamath Proof Explorer - 30801-30900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremhdmap1l6a 30801 Lemma for hdmap1l6 30813. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Z >. )  =  E )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. ) 
 .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6b0N 30802 Lemmma for hdmap1l6 30813. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  ( ( N `  { X } )  i^i  ( N `
  { Y ,  Z } ) )  =  {  .0.  } )   =>    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )
 
Theoremhdmap1l6b 30803 Lemmma for hdmap1l6 30813. (Contributed by NM, 24-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  =  .0.  )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. ) 
 .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6c 30804 Lemmma for hdmap1l6 30813. (Contributed by NM, 24-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  =  .0.  )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6d 30805 Lemmma for hdmap1l6 30813. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( w  .+  ( Y  .+  Z ) ) >. )  =  ( ( I `  <. X ,  F ,  w >. )  .+b  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. ) ) )
 
Theoremhdmap1l6e 30806 Lemmma for hdmap1l6 30813. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( ( w  .+  Y )  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  ( w  .+  Y )
 >. )  .+b  ( I `
  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6f 30807 Lemmma for hdmap1l6 30813. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( w  .+  Y ) >. )  =  ( ( I `  <. X ,  F ,  w >. )  .+b  ( I `  <. X ,  F ,  Y >. ) ) )
 
Theoremhdmap1l6g 30808 Lemmma for hdmap1l6 30813. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( ( I `  <. X ,  F ,  w >. ) 
 .+b  ( I `  <. X ,  F ,  ( Y  .+  Z )
 >. ) )  =  ( ( ( I `  <. X ,  F ,  w >. )  .+b  ( I `  <. X ,  F ,  Y >. ) )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6h 30809 Lemmma for hdmap1l6 30813. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N ` 
 { Y } )  =  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  w  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  -.  w  e.  ( N `
  { X ,  Y } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6i 30810 Lemmma for hdmap1l6 30813. Eliminate auxiliary vector  w. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  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 >. ) ) )
 
Theoremhdmap1l6j 30811 Lemmma for hdmap1l6 30813. Eliminate  ( N { Y } ) = ( N  { Z } ) hypothesis. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. ) 
 .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1l6k 30812 Lemmma for hdmap1l6 30813. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  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 >. ) ) )
 
Theoremhdmap1l6 30813 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 15714. (Contributed by NM, 17-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 )   &    |-  .+b  =  ( +g  `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( L `  { F } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1p6N 30814 (Convert mapdh6N 30738 to use HDMap1 function.) 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 15714. TODO: No longer used and should be deleted. Use hdmap1l6 30813 instead. Also delete unused mapdh6N 30738 etc. leading up to this. (Contributed by NM, 17-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 )   &    |-  .+b  =  ( +g  `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( L `  { F } ) )   =>    |-  ( ph  ->  ( I `  <. X ,  F ,  ( Y  .+  Z ) >. )  =  ( ( I `  <. X ,  F ,  Y >. )  .+b  ( I `  <. X ,  F ,  Z >. ) ) )
 
Theoremhdmap1eulem 30815* Lemma for hdmap1eu 30817. TODO: combine with hdmap1eu 30817 or at least share some hypotheses. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  Q  =  ( 0g
 `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  T  e.  V )   &    |-  L  =  ( x  e.  _V  |->  if (
 ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   =>    |-  ( ph  ->  E! y  e.  D  A. z  e.  V  ( -.  z  e.  ( ( N `  { X } )  u.  ( N `  { T } ) )  ->  y  =  ( I `  <. z ,  ( I `  <. X ,  F ,  z >. ) ,  T >. ) ) )
 
Theoremhdmap1eulemOLDN 30816* Lemma for hdmap1euOLDN 30818. TODO: combine with hdmap1euOLDN 30818 or at least share some hypotheses. (Contributed by NM, 15-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  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( J `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  T  e.  V )   &    |-  L  =  ( x  e.  _V  |->  if (
 ( 2nd `  x )  =  .0.  ,  Q ,  ( iota_ h  e.  D ( ( M `  ( N `  { ( 2nd `  x ) }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( ( 1st `  ( 1st `  x ) )  .-  ( 2nd `  x ) ) }
 ) )  =  ( J `  { (
 ( 2nd `  ( 1st `  x ) ) R h ) } )
 ) ) ) )   =>    |-  ( ph  ->  E! y  e.  D  A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T } )  ->  y  =  ( I `  <. z ,  ( I `  <. X ,  F ,  z >. ) ,  T >. ) ) )
 
Theoremhdmap1eu 30817* Convert mapdh9a 30781 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( 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 >. ) ) )
 
Theoremhdmap1euOLDN 30818* Convert mapdh9aOLDN 30782 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  E! y  e.  D  A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T } )  ->  y  =  ( I `  <. z ,  ( I `  <. X ,  F ,  z >. ) ,  T >. ) ) )
 
Theoremhdmap1neglem1N 30819 Lemma for hdmapneg 30840. TODO: Not used; delete. (Contributed by NM, 23-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  ( inv g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  (
 Base `  C )   &    |-  S  =  ( inv g `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( L `  { F } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( I `  <. X ,  F ,  Y >. )  =  G )   =>    |-  ( ph  ->  ( I `  <. ( R `  X ) ,  ( S `  F ) ,  ( R `  Y ) >. )  =  ( S `  G ) )
 
Theoremhdmapffval 30820* Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   =>    |-  ( K  e.  X  ->  (HDMap `  K )  =  ( w  e.  H  |->  { a  |  [. <. (  _I  |`  ( Base `  K )
 ) ,  (  _I  |`  ( ( LTrn `  K ) `  w ) )
 >.  /  e ]. [. (
 ( DVecH `  K ) `  w )  /  u ].
 [. ( Base `  u )  /  v ]. [. (
 (HDMap1 `  K ) `  w )  /  i ]. a  e.  (
 t  e.  v  |->  (
 iota_ y  e.  ( Base `  ( (LCDual `  K ) `  w ) )
 A. z  e.  v  ( -.  z  e.  (
 ( ( LSpan `  u ) `  { e }
 )  u.  ( (
 LSpan `  u ) `  { t } )
 )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  K ) `  w ) `  e ) ,  z >. ) ,  t >. ) ) ) ) } ) )
 
Theoremhdmapfval 30821* Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  A  /\  W  e.  H ) )   =>    |-  ( ph  ->  S  =  ( t  e.  V  |->  ( iota_ y  e.  D A. z  e.  V  ( -.  z  e.  (
 ( N `  { E } )  u.  ( N `  { t }
 ) )  ->  y  =  ( I `  <. z ,  ( I `  <. E ,  ( J `  E ) ,  z >. ) ,  t >. ) ) ) ) )
 
Theoremhdmapval 30822* Value of map from vectors to functionals in the closed kernel dual space. This is the function sigma on line 27 above part 9 in [Baer] p. 48. We select a convenient fixed reference vector  E to be  <. 0 ,  1 >. (corresponding to vector u on p. 48 line 7) whose span is the lattice isomorphism map of the fiducial atom  P  =  ( ( oc `  K
) `  W ) (see dvheveccl 30103). 
( J `  E
) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 30760 shows in Baer's notation (Fu)* = Gu'). Baer's independent vectors v and w on line 7 correspond to our  z that the  A. z  e.  V ranges over. The middle term  ( I `  <. E ,  ( J `
 E ) ,  z >. ) provides isolation to allow  E and  T to assume the same value without conflict. Closure is shown by hdmapcl 30824. If a separate auxiliary vector is known, hdmapval2 30826 provides a version without quantification. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  A  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  ( S `  T )  =  ( iota_ y  e.  D A. z  e.  V  ( -.  z  e.  ( ( N `  { E } )  u.  ( N `  { T } ) )  ->  y  =  ( I `  <. z ,  ( I `  <. E ,  ( J `  E ) ,  z >. ) ,  T >. ) ) ) )
 
TheoremhdmapfnN 30823 Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  S  Fn  V )
 
Theoremhdmapcl 30824 Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  ( S `  T )  e.  D )
 
Theoremhdmapval2lem 30825* Lemma for hdmapval2 30826. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  V )   &    |-  ( ph  ->  F  e.  D )   =>    |-  ( ph  ->  (
 ( S `  T )  =  F  <->  A. z  e.  V  ( -.  z  e.  (
 ( N `  { E } )  u.  ( N `  { T }
 ) )  ->  F  =  ( I `  <. z ,  ( I `  <. E ,  ( J `  E ) ,  z >. ) ,  T >. ) ) ) )
 
Theoremhdmapval2 30826 Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two  =/= hypothesis? Consider hdmaplem1 30762 through hdmaplem4 30765, which would become obsolete. (Contributed by NM, 15-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  V )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( ( N `  { E } )  u.  ( N `  { T } ) ) )   =>    |-  ( ph  ->  ( S `  T )  =  ( I `  <. X ,  ( I `  <. E ,  ( J `  E ) ,  X >. ) ,  T >. ) )
 
Theoremhdmapval0 30827 Value of map from vectors to functionals at zero. Note: we use dvh3dim 30437 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 30838 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  Q  =  ( 0g
 `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ( S `  .0.  )  =  Q )
 
Theoremhdmapeveclem 30828 Lemma for hdmapevec 30829. TODO: combine with hdmapevec 30829 if it shortens overall. (Contributed by NM, 16-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  (
 Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( ( N `  { E } )  u.  ( N `  { E } ) ) )   =>    |-  ( ph  ->  ( S `  E )  =  ( J `  E ) )
 
Theoremhdmapevec 30829 Value of map from vectors to functionals at the reference vector  E. (Contributed by NM, 16-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ( S `  E )  =  ( J `  E ) )
 
Theoremhdmapevec2 30830 The inner product of the reference vector  E with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of [Holland95] p. 14 line 32,  [ e , e  ]  =/=  0 is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  .1.  =  ( 1r `  R )   =>    |-  ( ph  ->  ( ( S `  E ) `  E )  =  .1.  )
 
Theoremhdmapval3lemN 30831 Value of map from vectors to functionals at arguments not colinear with the reference vector 
E. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( N `  { T } )  =/=  ( N `  { E }
 ) )   &    |-  ( ph  ->  T  e.  ( V  \  { ( 0g `  U ) } )
 )   &    |-  ( ph  ->  x  e.  V )   &    |-  ( ph  ->  -.  x  e.  ( N `
  { E ,  T } ) )   =>    |-  ( ph  ->  ( S `  T )  =  ( I `  <. E ,  ( J `
  E ) ,  T >. ) )
 
Theoremhdmapval3N 30832 Value of map from vectors to functionals at arguments not colinear with the reference vector  E. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( N `  { T } )  =/=  ( N `  { E }
 ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  ( S `  T )  =  ( I `  <. E ,  ( J `
  E ) ,  T >. ) )
 
Theoremhdmap10lem 30833 Lemma for hdmap10 30834. (Contributed by NM, 17-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  E  =  <. (  _I  |`  ( Base `  K ) ) ,  (  _I  |`  ( (
 LTrn `  K ) `  W ) ) >.   &    |-  .0.  =  ( 0g `  U )   &    |-  D  =  ( Base `  C )   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( M `  ( N `  { T } ) )  =  ( L `  { ( S `  T ) }
 ) )
 
Theoremhdmap10 30834 Part 10 in [Baer] p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  ( M `  ( N `
  { T }
 ) )  =  ( L `  { ( S `  T ) }
 ) )
 
Theoremhdmap11lem1 30835 Lemma for hdmapadd 30837. (Contributed by NM, 26-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( +g  `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  E  =  <. (  _I  |`  ( Base `  K )
 ) ,  (  _I  |`  ( ( LTrn `  K ) `  W ) )
 >.   &    |- 
 .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  D  =  ( Base `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   &    |-  ( ph  ->  z  e.  V )   &    |-  ( ph  ->  -.  z  e.  ( N `  { X ,  Y } ) )   &    |-  ( ph  ->  ( N ` 
 { z } )  =/=  ( N `  { E } ) )   =>    |-  ( ph  ->  ( S `  ( X 
 .+  Y ) )  =  ( ( S `
  X )  .+b  ( S `  Y ) ) )
 
Theoremhdmap11lem2 30836 Lemma for hdmapadd 30837. (Contributed by NM, 26-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( +g  `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  E  =  <. (  _I  |`  ( Base `  K )
 ) ,  (  _I  |`  ( ( LTrn `  K ) `  W ) )
 >.   &    |- 
 .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  D  =  ( Base `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  J  =  ( (HVMap `  K ) `  W )   &    |-  I  =  ( (HDMap1 `  K ) `  W )   =>    |-  ( ph  ->  ( S `  ( X 
 .+  Y ) )  =  ( ( S `
  X )  .+b  ( S `  Y ) ) )
 
Theoremhdmapadd 30837 Part 11 in [Baer] p. 48 line 35, (a+b)S = aS+bS in their notation (S = sigma). (Contributed by NM, 22-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( +g  `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  ( S `  ( X  .+  Y ) )  =  ( ( S `  X )  .+b  ( S `
  Y ) ) )
 
Theoremhdmapeq0 30838 Part of proof of part 12 in [Baer] p. 49 line 3. (Contributed by NM, 22-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  Q  =  ( 0g
 `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  ( ( S `  T )  =  Q  <->  T  =  .0.  ) )
 
Theoremhdmapnzcl 30839 Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  Q  =  ( 0g
 `  C )   &    |-  D  =  ( Base `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( S `  T )  e.  ( D  \  { Q }
 ) )
 
Theoremhdmapneg 30840 Part of proof of part 12 in [Baer] p. 49 line 4. The sigma map of a negative is the negative of the sigma map. (Contributed by NM, 24-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  M  =  ( inv g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  I  =  ( inv g `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  ( S `  ( M `  T ) )  =  ( I `  ( S `  T ) ) )
 
Theoremhdmapsub 30841 Part of proof of part 12 in [Baer] p. 49 line 5, (a-b)S = aS-bS in their notation (S = sigma). (Contributed by NM, 26-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  N  =  ( -g `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  ( S `  ( X 
 .-  Y ) )  =  ( ( S `
  X ) N ( S `  Y ) ) )
 
Theoremhdmap11 30842 Part of proof of part 12 in [Baer] p. 49 line 4, aS=bS iff a=b in their notation (S = sigma). The sigma map is one-to-one. (Contributed by NM, 26-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  (
 ( S `  X )  =  ( S `  Y )  <->  X  =  Y ) )
 
Theoremhdmaprnlem1N 30843 Part of proof of part 12 in [Baer] p. 49 line 10, Gu'  =/= Gs. Our  ( N `  { v } ) is Baer's T. (Contributed by NM, 26-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   =>    |-  ( ph  ->  ( L `  { ( S `  u ) }
 )  =/=  ( L ` 
 { s } )
 )
 
Theoremhdmaprnlem3N 30844 Part of proof of part 12 in [Baer] p. 49 line 15, T  =/= P. Our  ( `' M `  ( L `  {
( ( S `  u )  .+b  s
) } ) ) is Baer's P, where P* = G(u'+s). (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   =>    |-  ( ph  ->  ( N `  { v } )  =/=  ( `' M `  ( L `
  { ( ( S `  u ) 
 .+b  s ) }
 ) ) )
 
Theoremhdmaprnlem3uN 30845 Part of proof of part 12 in [Baer] p. 49. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   =>    |-  ( ph  ->  ( N `  { u } )  =/=  ( `' M `  ( L `
  { ( ( S `  u ) 
 .+b  s ) }
 ) ) )
 
Theoremhdmaprnlem4tN 30846 Lemma for hdmaprnN 30858. TODO: This lemma doesn't quite pay for itself even though used 4 times. Maybe prove this directly instead. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   =>    |-  ( ph  ->  t  e.  V )
 
Theoremhdmaprnlem4N 30847 Part of proof of part 12 in [Baer] p. 49 line 19. (T* =) (Ft)* = Gs. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( M `  ( N `  { t } )
 )  =  ( L `
  { s }
 ) )
 
Theoremhdmaprnlem6N 30848 Part of proof of part 12 in [Baer] p. 49 line 18, G(u'+s) = G(u'+t). (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  U )   &    |-  ( ph  ->  ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )   =>    |-  ( ph  ->  ( L `  { (
 ( S `  u )  .+b  s ) }
 )  =  ( L `
  { ( ( S `  u ) 
 .+b  ( S `  t ) ) }
 ) )
 
Theoremhdmaprnlem7N 30849 Part of proof of part 12 in [Baer] p. 49 line 19, s-St  e. G(u'+s) = P*. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  U )   &    |-  ( ph  ->  ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )   =>    |-  ( ph  ->  ( s ( -g `  C ) ( S `  t ) )  e.  ( L `  { (
 ( S `  u )  .+b  s ) }
 ) )
 
Theoremhdmaprnlem8N 30850 Part of proof of part 12 in [Baer] p. 49 line 19, s-St  e. (Ft)* = T*. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  U )   &    |-  ( ph  ->  ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )   =>    |-  ( ph  ->  ( s ( -g `  C ) ( S `  t ) )  e.  ( M `  ( N `  { t }
 ) ) )
 
Theoremhdmaprnlem9N 30851 Part of proof of part 12 in [Baer] p. 49 line 21, s=S(t). TODO: we seem to be going back and forth with mapd11 30630 and mapdcnv11N 30650. Use better hypotheses and/or theorems? (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  t  e.  (
 ( N `  { v } )  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  U )   &    |-  ( ph  ->  ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )   =>    |-  ( ph  ->  s  =  ( S `  t ) )
 
Theoremhdmaprnlem3eN 30852* Lemma for hdmaprnN 30858. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  .+  =  ( +g  `  U )   =>    |-  ( ph  ->  E. t  e.  (
 ( N `  { v } )  \  {  .0.  } ) ( L `  { ( ( S `
  u )  .+b  s ) } )  =  ( M `  ( N `  { ( u 
 .+  t ) }
 ) ) )
 
Theoremhdmaprnlem10N 30853* Lemma for hdmaprnN 30858. Show  s is in the range of  S. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  .+  =  ( +g  `  U )   =>    |-  ( ph  ->  E. t  e.  V  ( S `  t )  =  s )
 
Theoremhdmaprnlem11N 30854* Lemma for hdmaprnN 30858. Show  s is in the range of  S. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  s  e.  ( D  \  { Q } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `
  { v }
 ) )  =  ( L `  { s } ) )   &    |-  ( ph  ->  u  e.  V )   &    |-  ( ph  ->  -.  u  e.  ( N `  { v } ) )   &    |-  D  =  ( Base `  C )   &    |-  Q  =  ( 0g `  C )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .+b  =  ( +g  `  C )   &    |-  .+  =  ( +g  `  U )   =>    |-  ( ph  ->  s  e.  ran  S )
 
Theoremhdmaprnlem15N 30855* Lemma for hdmaprnN 30858. Eliminate  u. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .0.  =  ( 0g `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  s  e.  ( D  \  {  .0.  } ) )   &    |-  ( ph  ->  v  e.  V )   &    |-  ( ph  ->  ( M `  ( N `  { v } )
 )  =  ( L `
  { s }
 ) )   =>    |-  ( ph  ->  s  e.  ran  S )
 
Theoremhdmaprnlem16N 30856 Lemma for hdmaprnN 30858. Eliminate  v. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .0.  =  ( 0g `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  s  e.  ( D  \  {  .0.  } ) )   =>    |-  ( ph  ->  s  e.  ran  S )
 
Theoremhdmaprnlem17N 30857 Lemma for hdmaprnN 30858. Include zero. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .0.  =  ( 0g `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  s  e.  D )   =>    |-  ( ph  ->  s  e.  ran  S )
 
TheoremhdmaprnN 30858 Part of proof of part 12 in [Baer] p. 49 line 21, As=B. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ran  S  =  D )
 
Theoremhdmapf1oN 30859 Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 30837, this shows the map is an automorphism from the additive group of vectors to the additive group of functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  S : V -1-1-onto-> D )
 
Theoremhdmap14lem1a 30860 Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  F  e.  B )   &    |- 
 .0.  =  ( 0g `  R )   &    |-  ( ph  ->  F  =/=  .0.  )   =>    |-  ( ph  ->  ( L `  { ( S `  X ) }
 )  =  ( L `
  { ( S `
  ( F  .x.  X ) ) } )
 )
 
Theoremhdmap14lem2a 30861* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  .0. so it can be used in hdmap14lem10 30871. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  ( LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  F  e.  B )   =>    |-  ( ph  ->  E. g  e.  A  ( S `  ( F  .x.  X ) )  =  ( g 
 .xb  ( S `  X ) ) )
 
Theoremhdmap14lem1 30862 Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  ( L ` 
 { ( S `  X ) } )  =  ( L `  { ( S `  ( F  .x.  X ) ) } )
 )
 
Theoremhdmap14lem2N 30863* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include  F  =  Z so it can be used in hdmap14lem10 30871. (Contributed by NM, 31-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  E. g  e.  ( A  \  { Q } ) ( S `
  ( F  .x.  X ) )  =  ( g  .xb  ( S `  X ) ) )
 
Theoremhdmap14lem3 30864* Prior to part 14 in [Baer] p. 49, line 26. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  E! g  e.  ( A  \  { Q } ) ( S `
  ( F  .x.  X ) )  =  ( g  .xb  ( S `  X ) ) )
 
Theoremhdmap14lem4a 30865* Simplify  ( A  \  { Q } ) in hdmap14lem3 30864 to provide a slightly simpler definition later. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  ( E! g  e.  ( A  \  { Q } )
 ( S `  ( F  .x.  X ) )  =  ( g  .xb  ( S `  X ) )  <->  E! g  e.  A  ( S `  ( F 
 .x.  X ) )  =  ( g  .xb  ( S `  X ) ) ) )
 
Theoremhdmap14lem4 30866* Simplify  ( A  \  { Q } ) in hdmap14lem3 30864 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 30865 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 30865 into this one. (Contributed by NM, 31-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  ( B  \  { Z } ) )   =>    |-  ( ph  ->  E! g  e.  A  ( S `  ( F  .x.  X ) )  =  ( g 
 .xb  ( S `  X ) ) )
 
Theoremhdmap14lem6 30867* Case where  F is zero. (Contributed by NM, 1-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  Z  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  L  =  (
 LSpan `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  Q  =  ( 0g `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  =  Z )   =>    |-  ( ph  ->  E! g  e.  A  ( S `  ( F 
 .x.  X ) )  =  ( g  .xb  ( S `  X ) ) )
 
Theoremhdmap14lem7 30868* Combine cases of  F. TODO: Can this be done at once in hdmap14lem3 30864, in order to get rid of hdmap14lem6 30867? Perhaps modify lspsneu 15711 to become  E! k  e.  K instead of  E! k  e.  ( K  \  {  .0.  } )? (Contributed by NM, 1-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  (
 Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  F  e.  B )   =>    |-  ( ph  ->  E! g  e.  A  ( S `  ( F  .x.  X ) )  =  ( g  .xb  ( S `  X ) ) )
 
Theoremhdmap14lem8 30869 Part of proof of part 14 in [Baer] p. 49 lines 33-35. (Contributed by NM, 1-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( +g  `  C )   &    |-  .xb  =  ( .s `  C )   &    |-  P  =  (Scalar `  C )   &    |-  A  =  ( Base `  P )   &    |-  S  =  ( (HDMap `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  F  e.  B )   &    |-  ( ph  ->  G  e.  A )   &    |-  ( ph  ->  I  e.  A )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  X ) )  =  ( G  .xb  ( S `  X ) ) )   &    |-  ( ph  ->  ( S `  ( F 
 .x.  Y ) )  =  ( I  .xb  ( S `  Y ) ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  J  e.  A )   &    |-  ( ph  ->  ( S `  ( F  .x.  ( X 
 .+  Y ) ) )  =  ( J 
 .xb  ( S `  ( X  .+  Y ) ) ) )   =>    |-  ( ph  ->  ( ( J  .xb  ( S `  X ) ) 
 .+b  ( J  .xb  ( S `  Y ) ) )  =  ( ( G  .xb  ( S `  X ) ) 
 .+b  ( I  .xb  ( S `  Y ) ) ) )
 
Theoremhdmap14lem9 30870 Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 1-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R