HomeHome Metamath Proof Explorer
Theorem List (p. 308 of 311)
< 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-31058)
 

Theorem List for Metamath Proof Explorer - 30701-30800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlcdvsass 30701 Associative law for scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  L  =  ( Base `  R )   &    |-  .x.  =  ( .r `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  .xb  =  ( .s `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  L )   &    |-  ( ph  ->  Y  e.  L )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  (
 ( Y  .x.  X )  .xb  G )  =  ( X  .xb  ( Y  .xb  G ) ) )
 
Theoremlcd0 30702 The zero scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  .0.  =  ( 0g `  F )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  S  =  (Scalar `  C )   &    |-  O  =  ( 0g
 `  S )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  O  =  .0.  )
 
Theoremlcd1 30703 The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  .1.  =  ( 1r `  F )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  S  =  (Scalar `  C )   &    |-  I  =  ( 1r
 `  S )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  I  =  .1.  )
 
Theoremlcdneg 30704 The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 11-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  M  =  ( inv g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  S  =  (Scalar `  C )   &    |-  N  =  ( inv g `  S )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  N  =  M )
 
Theoremlcd0v 30705 The zero functional in the set of functionals with closed kernels. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  .0.  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  O  =  ( 0g
 `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  O  =  ( V  X.  {  .0.  } ) )
 
Theoremlcd0v2 30706 The zero functional in the set of functionals with closed kernels. (Contributed by NM, 27-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  D  =  (LDual `  U )   &    |-  .0.  =  ( 0g `  D )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  O  =  ( 0g
 `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  O  =  .0.  )
 
Theoremlcd0vvalN 30707 Value of the zero functional at any vector. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  .0.  =  ( 0g `  S )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  O  =  ( 0g
 `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  ( O `  X )  =  .0.  )
 
Theoremlcd0vcl 30708 Closure of the zero functional in the set of functionals with closed kernels. (Contributed by NM, 15-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  V  =  ( Base `  C )   &    |-  O  =  ( 0g `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  O  e.  V )
 
Theoremlcd0vs 30709 A scalar zero times a functional is the zero functional. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  R  =  (Scalar `  U )   &    |-  .0.  =  ( 0g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  V  =  ( Base `  C )   &    |-  .x.  =  ( .s `  C )   &    |-  O  =  ( 0g `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  V )   =>    |-  ( ph  ->  (  .0.  .x.  G )  =  O )
 
Theoremlcdvs0N 30710 A scalar times the zero functional is the zero functional. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  ( Base `  S )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .x.  =  ( .s `  C )   &    |-  .0.  =  ( 0g `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  R )   =>    |-  ( ph  ->  ( X  .x.  .0.  )  =  .0.  )
 
Theoremlcdvsub 30711 The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  (Scalar `  U )   &    |-  N  =  ( inv g `  S )   &    |-  .1.  =  ( 1r `  S )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  V  =  ( Base `  C )   &    |-  .+  =  ( +g  `  C )   &    |-  .x.  =  ( .s `  C )   &    |-  .-  =  ( -g `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  V )   &    |-  ( ph  ->  G  e.  V )   =>    |-  ( ph  ->  ( F  .-  G )  =  ( F  .+  (
 ( N `  .1.  )  .x.  G ) ) )
 
Theoremlcdvsubval 30712 The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 11-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  S  =  ( -g `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .-  =  ( -g `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  G  e.  D )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  (
 ( F  .-  G ) `  X )  =  ( ( F `  X ) S ( G `  X ) ) )
 
Theoremlcdlss 30713* Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  S  =  ( LSubSp `  C )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  T  =  ( LSubSp `  D )   &    |-  B  =  { f  e.  F  |  ( O `  ( O `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  S  =  ( T  i^i  ~P B ) )
 
Theoremlcdlss2N 30714 Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  S  =  ( LSubSp `  C )   &    |-  V  =  ( Base `  C )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  D  =  (LDual `  U )   &    |-  T  =  ( LSubSp `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  S  =  ( T  i^i  ~P V ) )
 
Theoremlcdlsp 30715 Span in the set of functionals with closed kernels. (Contributed by NM, 28-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  D  =  (LDual `  U )   &    |-  M  =  ( LSpan `  D )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  N  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G 
 C_  F )   =>    |-  ( ph  ->  ( N `  G )  =  ( M `  G ) )
 
TheoremlcdlkreqN 30716 Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  L  =  (LKer `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .0.  =  ( 0g `  C )   &    |-  N  =  ( LSpan `  C )   &    |-  V  =  (
 Base `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  I  e.  V )   &    |-  ( ph  ->  G  e.  ( N `  { I }
 ) )   &    |-  ( ph  ->  G  =/=  .0.  )   =>    |-  ( ph  ->  ( L `  G )  =  ( L `  I ) )
 
Theoremlcdlkreq2N 30717 Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  ( Base `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  L  =  (LKer `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  V  =  (
 Base `  C )   &    |-  .x.  =  ( .s `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  A  e.  ( R  \  {  .0.  }
 ) )   &    |-  ( ph  ->  I  e.  V )   &    |-  ( ph  ->  G  =  ( A  .x.  I )
 )   =>    |-  ( ph  ->  ( L `  G )  =  ( L `  I
 ) )
 
Syntaxcmpd 30718 Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels.
 class mapd
 
Definitiondf-mapd 30719* Extend class notation with a one-to-one onto (mapd1o 30742), order-preserving (mapdord 30732) map, called a projectivity (definition of projectivity in [Baer] p. 40), from subspaces of vector space H to those subspaces of the dual space having functionals with closed kernels. (Contributed by NM, 25-Jan-2015.)
 |- mapd  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( s  e.  ( LSubSp `  (
 ( DVecH `  k ) `  w ) )  |->  { f  e.  (LFnl `  ( ( DVecH `  k
 ) `  w )
 )  |  ( ( ( ( ocH `  k
 ) `  w ) `  ( ( ( ocH `  k ) `  w ) `  ( (LKer `  ( ( DVecH `  k
 ) `  w )
 ) `  f )
 ) )  =  ( (LKer `  ( ( DVecH `  k ) `  w ) ) `  f )  /\  ( ( ( ocH `  k
 ) `  w ) `  ( (LKer `  (
 ( DVecH `  k ) `  w ) ) `  f ) )  C_  s ) } )
 ) )
 
Theoremmapdffval 30720* Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.)
 |-  H  =  ( LHyp `  K )   =>    |-  ( K  e.  X  ->  (mapd `  K )  =  ( w  e.  H  |->  ( s  e.  ( LSubSp `  ( ( DVecH `  K ) `  w ) ) 
 |->  { f  e.  (LFnl `  ( ( DVecH `  K ) `  w ) )  |  ( ( ( ( ocH `  K ) `  w ) `  ( ( ( ocH `  K ) `  w ) `  ( (LKer `  ( ( DVecH `  K ) `  w ) ) `
  f ) ) )  =  ( (LKer `  ( ( DVecH `  K ) `  w ) ) `
  f )  /\  ( ( ( ocH `  K ) `  w ) `  ( (LKer `  ( ( DVecH `  K ) `  w ) ) `
  f ) ) 
 C_  s ) }
 ) ) )
 
Theoremmapdfval 30721* Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   =>    |-  ( ( K  e.  X  /\  W  e.  H )  ->  M  =  ( s  e.  S  |->  { f  e.  F  |  ( ( O `  ( O `  ( L `
  f ) ) )  =  ( L `
  f )  /\  ( O `  ( L `
  f ) ) 
 C_  s ) }
 ) )
 
Theoremmapdval 30722* Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  X  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  S )   =>    |-  ( ph  ->  ( M `  T )  =  { f  e.  F  |  ( ( O `  ( O `
  ( L `  f ) ) )  =  ( L `  f )  /\  ( O `
  ( L `  f ) )  C_  T ) } )
 
Theoremmapdvalc 30723* Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  X  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  S )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   =>    |-  ( ph  ->  ( M `  T )  =  { f  e.  C  |  ( O `
  ( L `  f ) )  C_  T } )
 
Theoremmapdval2N 30724* Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  S )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   =>    |-  ( ph  ->  ( M `  T )  =  { f  e.  C  |  E. v  e.  T  ( O `  ( L `  f ) )  =  ( N `
  { v }
 ) } )
 
Theoremmapdval3N 30725* Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  S )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   =>    |-  ( ph  ->  ( M `  T )  =  U_ v  e.  T  { f  e.  C  |  ( O `
  ( L `  f ) )  =  ( N `  { v } ) } )
 
Theoremmapdval4N 30726* Value of projectivity from vector space H to dual space. TODO: 1. This is shorter than others - make it the official def? (but is not as obvious that it is  C_  C) 2. The unneeded direction of lcfl8a 30597 has awkward  E.- add another thm with only one direction of it? 3. Swap  O `  {
v } and  L `  f? (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  S )   =>    |-  ( ph  ->  ( M `  T )  =  { f  e.  F  |  E. v  e.  T  ( O `  { v } )  =  ( L `  f
 ) } )
 
Theoremmapdval5N 30727* Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  T  e.  S )   =>    |-  ( ph  ->  ( M `  T )  =  U_ v  e.  T  { f  e.  F  |  ( O `
  { v }
 )  =  ( L `
  f ) }
 )
 
Theoremmapdordlem1a 30728* Lemma for mapdord 30732. (Contributed by NM, 27-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  Y  =  (LSHyp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  T  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  e.  Y }   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ( J  e.  T  <->  ( J  e.  C  /\  ( O `  ( O `  ( L `
  J ) ) )  e.  Y ) ) )
 
Theoremmapdordlem1bN 30729* Lemma for mapdord 30732. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.)
 |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   =>    |-  ( J  e.  C 
 <->  ( J  e.  F  /\  ( O `  ( O `  ( L `  J ) ) )  =  ( L `  J ) ) )
 
Theoremmapdordlem1 30730* Lemma for mapdord 30732. (Contributed by NM, 27-Jan-2015.)
 |-  T  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  e.  Y }   =>    |-  ( J  e.  T 
 <->  ( J  e.  F  /\  ( O `  ( O `  ( L `  J ) ) )  e.  Y ) )
 
Theoremmapdordlem2 30731* Lemma for mapdord 30732. Ordering property of projectivity  M. TODO: This was proved using some hacked-up older proofs. Maybe simplify; get rid of the 
T hypothesis. (Contributed by NM, 27-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  F  =  (LFnl `  U )   &    |-  J  =  (LSHyp `  U )   &    |-  L  =  (LKer `  U )   &    |-  T  =  {
 g  e.  F  |  ( O `  ( O `
  ( L `  g ) ) )  e.  J }   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   =>    |-  ( ph  ->  ( ( M `  X )  C_  ( M `  Y )  <->  X  C_  Y ) )
 
Theoremmapdord 30732 Ordering property of the map defined by df-mapd 30719. Property (b) of [Baer] p. 40. (Contributed by NM, 27-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  (
 ( M `  X )  C_  ( M `  Y )  <->  X  C_  Y ) )
 
Theoremmapd11 30733 The map defined by df-mapd 30719 is one-to-one. Property (c) of [Baer] p. 40. (Contributed by NM, 12-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  (
 ( M `  X )  =  ( M `  Y )  <->  X  =  Y ) )
 
TheoremmapddlssN 30734 The mapping of a subspace of vector space H to the dual space is a subspace of the dual space. TODO: Make this obsolete, use mapdcl2 30750 instead. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  D  =  (LDual `  U )   &    |-  T  =  ( LSubSp `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  R  e.  S )   =>    |-  ( ph  ->  ( M `  R )  e.  T )
 
Theoremmapdsn 30735* Value of the map defined by df-mapd 30719 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  {
 f  e.  F  |  ( O `  { X } )  C_  ( L `
  f ) }
 )
 
Theoremmapdsn2 30736* Value of the map defined by df-mapd 30719 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  ( L `  G )  =  ( O `  { X }
 ) )   =>    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  { f  e.  F  |  ( L `
  G )  C_  ( L `  f ) } )
 
Theoremmapdsn3 30737 Value of the map defined by df-mapd 30719 at the span of a singleton. (Contributed by NM, 17-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  P  =  ( LSpan `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  G )  =  ( O `  { X } ) )   =>    |-  ( ph  ->  ( M `  ( N `
  { X }
 ) )  =  ( P `  { G } ) )
 
Theoremmapd1dim2lem1N 30738* Value of the map defined by df-mapd 30719 at an atom. (Contributed by NM, 10-Feb-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  Q  e.  A )   =>    |-  ( ph  ->  ( M `  Q )  =  { f  e.  F  |  E. v  e.  Q  ( O `  { v } )  =  ( L `  f
 ) } )
 
Theoremmapdrvallem2 30739* Lemma for ~? mapdrval . TODO: very long antecendents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  T  =  ( LSubSp `  D )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  R  e.  T )   &    |-  ( ph  ->  R  C_  C )   &    |-  Q  =  U_ h  e.  R  ( O `  ( L `  h ) )   &    |-  V  =  (
 Base `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  Y  =  ( 0g
 `  D )   =>    |-  ( ph  ->  { f  e.  C  |  ( O `  ( L `
  f ) ) 
 C_  Q }  C_  R )
 
Theoremmapdrvallem3 30740* Lemma for ~? mapdrval . (Contributed by NM, 2-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  T  =  ( LSubSp `  D )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  R  e.  T )   &    |-  ( ph  ->  R  C_  C )   &    |-  Q  =  U_ h  e.  R  ( O `  ( L `  h ) )   &    |-  V  =  (
 Base `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  Y  =  ( 0g
 `  D )   =>    |-  ( ph  ->  { f  e.  C  |  ( O `  ( L `
  f ) ) 
 C_  Q }  =  R )
 
Theoremmapdrval 30741* Given a dual subspace  R (of functionals with closed kernels), reconstruct the subspace 
Q that maps to it. (Contributed by NM, 12-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  T  =  ( LSubSp `  D )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  R  e.  T )   &    |-  ( ph  ->  R  C_  C )   &    |-  Q  =  U_ h  e.  R  ( O `  ( L `  h ) )   =>    |-  ( ph  ->  ( M `  Q )  =  R )
 
Theoremmapd1o 30742* The map defined by df-mapd 30719 is one-to-one and onto the set of dual subspaces of functionals with closed kernels. This shows  M satisfies part of the definition of projectivity of [Baer] p. 40. TODO: change theorems leading to this (lcfr 30679, mapdrval 30741, lclkrs 30633, lclkr 30627,...) to use  T  i^i  ~P C? TODO: maybe get rid of $d's for  g vs.  K U W,. propagate to mapdrn 30743 and any others. (Contributed by NM, 12-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  T  =  ( LSubSp `  D )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  M : S -1-1-onto-> ( T  i^i  ~P C ) )
 
Theoremmapdrn 30743* Range of the map defined by df-mapd 30719. (Contributed by NM, 12-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  T  =  ( LSubSp `  D )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ran  M  =  ( T  i^i  ~P C ) )
 
TheoremmapdunirnN 30744* Union of the range of the map defined by df-mapd 30719. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  U. ran  M  =  C )
 
Theoremmapdrn2 30745 Range of the map defined by df-mapd 30719. TODO: this seems to be needed a lot in hdmaprnlem3eN 30955 etc. Would it be better to change df-mapd 30719 theorems to use  LSubSp `  C instead of  ran  M? (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  T  =  ( LSubSp `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ran  M  =  T )
 
Theoremmapdcnvcl 30746 Closure of the converse of the map defined by df-mapd 30719. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   =>    |-  ( ph  ->  ( `' M `  X )  e.  S )
 
Theoremmapdcl 30747 Closure the value of the map defined by df-mapd 30719. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   =>    |-  ( ph  ->  ( M `  X )  e.  ran  M )
 
Theoremmapdcnvid1N 30748 Converse of the value of the map defined by df-mapd 30719. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   =>    |-  ( ph  ->  ( `' M `  ( M `
  X ) )  =  X )
 
Theoremmapdsord 30749 Strong ordering property of themap defined by df-mapd 30719. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  (
 ( M `  X )  C.  ( M `  Y )  <->  X  C.  Y ) )
 
Theoremmapdcl2 30750 The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  T  =  ( LSubSp `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  R  e.  S )   =>    |-  ( ph  ->  ( M `  R )  e.  T )
 
Theoremmapdcnvid2 30751 Value of the converse of the map defined by df-mapd 30719. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   =>    |-  ( ph  ->  ( M `  ( `' M `  X ) )  =  X )
 
TheoremmapdcnvordN 30752 Ordering property of the converse of the map defined by df-mapd 30719. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   &    |-  ( ph  ->  Y  e.  ran  M )   =>    |-  ( ph  ->  (
 ( `' M `  X )  C_  ( `' M `  Y )  <->  X  C_  Y ) )
 
Theoremmapdcnv11N 30753 The converse of the map defined by df-mapd 30719 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   &    |-  ( ph  ->  Y  e.  ran  M )   =>    |-  ( ph  ->  (
 ( `' M `  X )  =  ( `' M `  Y )  <->  X  =  Y )
 )
 
Theoremmapdcv 30754 Covering property of the converse of the map defined by df-mapd 30719. (Contributed by NM, 14-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  C  =  (  <oLL  `
  U )   &    |-  D  =  ( (LCDual `  K ) `  W )   &    |-  E  =  (  <oLL  `
  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  ( X C Y  <->  ( M `  X ) E ( M `  Y ) ) )
 
Theoremmapdincl 30755 Closure of dual subspace intersection for the map defined by df-mapd 30719. (Contributed by NM, 12-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   &    |-  ( ph  ->  Y  e.  ran  M )   =>    |-  ( ph  ->  ( X  i^i  Y )  e. 
 ran  M )
 
Theoremmapdin 30756 Subspace intersection is preserved by the map defined by df-mapd 30719. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  ( M `  ( X  i^i  Y ) )  =  ( ( M `  X )  i^i  ( M `  Y ) ) )
 
Theoremmapdlsmcl 30757 Closure of dual subspace sum for the map defined by df-mapd 30719. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   &    |-  ( ph  ->  Y  e.  ran  M )   =>    |-  ( ph  ->  ( X  .(+)  Y )  e. 
 ran  M )
 
Theoremmapdlsm 30758 Subspace sum is preserved by the map defined by df-mapd 30719. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( LSSum `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  ( M `  ( X  .(+)  Y ) )  =  ( ( M `  X )  .+b  ( M `  Y ) ) )
 
Theoremmapd0 30759 Projectivity map of the zero subspace. Part of property (f) in [Baer] p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  O  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |- 
 .0.  =  ( 0g `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   =>    |-  ( ph  ->  ( M `  { O }
 )  =  {  .0.  } )
 
TheoremmapdcnvatN 30760 Atoms are preserved by the map defined by df-mapd 30719. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  B  =  (LSAtoms `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  Q  e.  B )   =>    |-  ( ph  ->  ( `' M `  Q )  e.  A )
 
Theoremmapdat 30761 Atoms are preserved by the map defined by df-mapd 30719. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  B  =  (LSAtoms `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  Q  e.  A )   =>    |-  ( ph  ->  ( M `  Q )  e.  B )
 
Theoremmapdspex 30762* The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  B  =  ( Base `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  E. g  e.  B  ( M `  ( N `
  { X }
 ) )  =  ( J `  { g } ) )
 
Theoremmapdn0 30763 Transfer non-zero property from domain to range of projectivity mapd. (Contributed by NM, 12-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )   &    |-  .0.  =  ( 0g `  U )   &    |-  Z  =  ( 0g
 `  C )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  F  e.  ( D  \  { Z } ) )
 
Theoremmapdncol 30764 Transfer non-colinearity from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  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 )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  G  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { Y } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   =>    |-  ( ph  ->  ( J `  { F } )  =/=  ( J `  { G }
 ) )
 
Theoremmapdindp 30765 Transfer (part of) vector independence condition from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  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 )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  G  e.  D )   &    |-  ( ph  ->  ( M `  ( N `  { Y } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  E  e.  D )   &    |-  ( ph  ->  ( M `  ( N `
  { Z }
 ) )  =  ( J `  { E } ) )   &    |-  ( ph  ->  -.  X  e.  ( N `  { Y ,  Z } ) )   =>    |-  ( ph  ->  -.  F  e.  ( J `  { G ,  E } ) )
 
Theoremmapdpglem1 30766 Lemma for mapdpg 30800. Baer p. 44, last line: "(F(x-y))* =< (Fx)*+(Fy)*." (Contributed by NM, 15-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   =>    |-  ( ph  ->  ( M `  ( N `
  { ( X 
 .-  Y ) }
 ) )  C_  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )
 
Theoremmapdpglem2 30767* Lemma for mapdpg 30800. Baer p. 45, lines 1 and 2: "we have (F(x-y))* = Gt where t necessarily belongs to (Fx)*+(Fy)*." (We scope $d  t ph locally to avoid clashes with later substitutions into  ph.) (Contributed by NM, 15-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   =>    |-  ( ph  ->  E. t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) ( M `  ( N `  { ( X  .-  Y ) }
 ) )  =  ( J `  { t } ) )
 
Theoremmapdpglem2a 30768* Lemma for mapdpg 30800. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   =>    |-  ( ph  ->  t  e.  F )
 
Theoremmapdpglem3 30769* Lemma for mapdpg 30800. Baer p. 45, line 3: "infer...the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope $d  g w z
ph locally to avoid clashes with later substitutions into  ph.) (Contributed by NM, 18-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   =>    |-  ( ph  ->  E. g  e.  B  E. z  e.  ( M `  ( N `  { Y } ) ) t  =  ( ( g 
 .x.  G ) R z ) )
 
Theoremmapdpglem4N 30770* Lemma for mapdpg 30800. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   =>    |-  ( ph  ->  ( X  .-  Y )  =/= 
 Q )
 
Theoremmapdpglem5N 30771* Lemma for mapdpg 30800. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   =>    |-  ( ph  ->  t  =/=  ( 0g `  C ) )
 
Theoremmapdpglem6 30772* Lemma for mapdpg 30800. Baer p. 45, line 4: "If g were 0, then t would be in (Fy)*..." (Contributed by NM, 18-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  g  =  .0.  )   =>    |-  ( ph  ->  t  e.  ( M `  ( N `  { Y }
 ) ) )
 
Theoremmapdpglem8 30773* Lemma for mapdpg 30800. Baer p. 45, line 4: "...so that (F(x-y))* =< (Fy)*. This would imply that F(x-y) =< F(y)..." (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  g  =  .0.  )   =>    |-  ( ph  ->  ( N `  { ( X 
 .-  Y ) }
 )  C_  ( N ` 
 { Y } )
 )
 
Theoremmapdpglem9 30774* Lemma for mapdpg 30800. Baer p. 45, line 4: "...so that x would consequently belong to Fy." (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  g  =  .0.  )   =>    |-  ( ph  ->  X  e.  ( N `  { Y } ) )
 
Theoremmapdpglem10 30775* Lemma for mapdpg 30800. Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  g  =  .0.  )   =>    |-  ( ph  ->  ( N `  { X }
 )  =  ( N `
  { Y }
 ) )
 
Theoremmapdpglem11 30776* Lemma for mapdpg 30800. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   =>    |-  ( ph  ->  g  =/=  .0.  )
 
Theoremmapdpglem12 30777* Lemma for mapdpg 30800. TODO: Can some commonality with mapdpglem6 30772 through mapdpglem11 30776 be exploited? Also, some consolidation of small lemmas here could be done. (Contributed by NM, 18-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  ( ph  ->  z  =  ( 0g `  C ) )   =>    |-  ( ph  ->  t  e.  ( M `  ( N `  { X }
 ) ) )
 
Theoremmapdpglem13 30778* Lemma for mapdpg 30800. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  ( ph  ->  z  =  ( 0g `  C ) )   =>    |-  ( ph  ->  ( N `  { ( X 
 .-  Y ) }
 )  C_  ( N ` 
 { X } )
 )
 
Theoremmapdpglem14 30779* Lemma for mapdpg 30800. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  ( ph  ->  z  =  ( 0g `  C ) )   =>    |-  ( ph  ->  Y  e.  ( N `  { X } ) )
 
Theoremmapdpglem15 30780* Lemma for mapdpg 30800. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  ( ph  ->  z  =  ( 0g `  C ) )   =>    |-  ( ph  ->  ( N `  { X }
 )  =  ( N `
  { Y }
 ) )
 
Theoremmapdpglem16 30781* Lemma for mapdpg 30800. Baer p. 45, line 7: "Likewise we see that z =/= 0." (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   =>    |-  ( ph  ->  z  =/=  ( 0g `  C ) )
 
Theoremmapdpglem17N 30782* Lemma for mapdpg 30800. Baer p. 45, line 7: "Hence we may form y' = g^-1 z." (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  E  =  ( ( ( invr `  A ) `  g )  .x.  z
 )   =>    |-  ( ph  ->  E  e.  F )
 
Theoremmapdpglem18 30783* Lemma for mapdpg 30800. Baer p. 45, line 7: "Then y =/= 0..." (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  E  =  ( ( ( invr `  A ) `  g )  .x.  z
 )   =>    |-  ( ph  ->  E  =/=  ( 0g `  C ) )
 
Theoremmapdpglem19 30784* Lemma for mapdpg 30800. Baer p. 45, line 8: "...is in (Fy)*..." (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  E  =  ( ( ( invr `  A ) `  g )  .x.  z
 )   =>    |-  ( ph  ->  E  e.  ( M `  ( N `  { Y }
 ) ) )
 
Theoremmapdpglem20 30785* Lemma for mapdpg 30800. Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  E  =  ( ( ( invr `  A ) `  g )  .x.  z
 )   =>    |-  ( ph  ->  ( M `  ( N `  { Y } ) )  =  ( J `  { E } ) )
 
Theoremmapdpglem21 30786* Lemma for mapdpg 30800. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  E  =  ( ( ( invr `  A ) `  g )  .x.  z
 )   =>    |-  ( ph  ->  (
 ( ( invr `  A ) `  g )  .x.  t )  =  ( G R E ) )
 
Theoremmapdpglem22 30787* Lemma for mapdpg 30800. Baer p. 45, line 9: "(F(x-y))* = ... = G(x'-y')." (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  R  =  ( -g `  C )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  Q  =  ( 0g `  U )   &    |-  ( ph  ->  ( N `  { X }
 )  =/=  ( N ` 
 { Y } )
 )   &    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { t }
 ) )   &    |-  .0.  =  ( 0g `  A )   &    |-  ( ph  ->  g  e.  B )   &    |-  ( ph  ->  z  e.  ( M `  ( N `  { Y } ) ) )   &    |-  ( ph  ->  t  =  ( ( g  .x.  G ) R z ) )   &    |-  ( ph  ->  X  =/=  Q )   &    |-  ( ph  ->  Y  =/=  Q )   &    |-  E  =  ( ( ( invr `  A ) `  g )  .x.  z
 )   =>    |-  ( ph  ->  ( M `  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R E ) }
 ) )
 
Theoremmapdpglem23 30788* Lemma for mapdpg 30800. Baer p. 45, line 10: "and so y' meets all our requirements." Our  h is Baer's y'. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  F  =  ( Base `  C )   &    |-  ( ph  ->  t  e.  (
 ( M `  ( N `  { X }
 ) )  .(+)  ( M `
  ( N `  { Y } ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  (
 Base `  A )   &    |-  .x.  =  ( .s `  C