HomeHome Metamath Proof Explorer
Theorem List (p. 348 of 389)
< 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-26262)
  Hilbert Space Explorer  Hilbert Space Explorer
(26263-27786)
  Users' Mathboxes  Users' Mathboxes
(27787-38873)
 

Theorem List for Metamath Proof Explorer - 34701-34800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmapdspex 34701* 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 34702 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 34703 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 34704 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 34705 Lemma for mapdpg 34739. 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 34706* Lemma for mapdpg 34739. 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 34707* Lemma for mapdpg 34739. (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 34708* Lemma for mapdpg 34739. 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 34709* Lemma for mapdpg 34739. (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 34710* Lemma for mapdpg 34739. (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 34711* Lemma for mapdpg 34739. 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 34712* Lemma for mapdpg 34739. 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 34713* Lemma for mapdpg 34739. 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 34714* Lemma for mapdpg 34739. 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 34715* Lemma for mapdpg 34739. (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 34716* Lemma for mapdpg 34739. TODO: Can some commonality with mapdpglem6 34711 through mapdpglem11 34715 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 34717* Lemma for mapdpg 34739. (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 34718* Lemma for mapdpg 34739. (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 34719* Lemma for mapdpg 34739. (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 34720* Lemma for mapdpg 34739. 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 34721* Lemma for mapdpg 34739. 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 34722* Lemma for mapdpg 34739. 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 34723* Lemma for mapdpg 34739. 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 34724* Lemma for mapdpg 34739. 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 34725* Lemma for mapdpg 34739. (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 34726* Lemma for mapdpg 34739. 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 34727* Lemma for mapdpg 34739. 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 )   &    |-  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. h  e.  F  ( ( M `
  ( N `  { Y } ) )  =  ( J `  { h } )  /\  ( M `  ( N `
  { ( X 
 .-  Y ) }
 ) )  =  ( J `  { ( G R h ) }
 ) ) )
 
Theoremmapdpglem30a 34728 Lemma for mapdpg 34739. (Contributed by NM, 22-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   =>    |-  ( ph  ->  G  =/=  ( 0g `  C ) )
 
Theoremmapdpglem30b 34729 Lemma for mapdpg 34739. (Contributed by NM, 22-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( h  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) ) )   &    |-  ( ph  ->  ( i  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { i } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R i ) }
 ) ) ) )   =>    |-  ( ph  ->  i  =/=  ( 0g `  C ) )
 
Theoremmapdpglem25 34730 Lemma for mapdpg 34739. Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( h  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) ) )   &    |-  ( ph  ->  ( i  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { i } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R i ) }
 ) ) ) )   =>    |-  ( ph  ->  ( ( J `  { h }
 )  =  ( J `
  { i }
 )  /\  ( J ` 
 { ( G R h ) } )  =  ( J `  { ( G R i ) }
 ) ) )
 
Theoremmapdpglem26 34731* Lemma for mapdpg 34739. Baer p. 45 line 14: "Consequently there exist numbers u,v in G neither of which is 0 such that y = uy'' and..." (We scope $d  u ph locally to avoid clashes with later substitutions into 
ph.) (Contributed by NM, 22-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( h  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) ) )   &    |-  ( ph  ->  ( i  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { i } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R i ) }
 ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  ( Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  O  =  ( 0g `  A )   =>    |-  ( ph  ->  E. u  e.  ( B  \  { O } ) h  =  ( u  .x.  i
 ) )
 
Theoremmapdpglem27 34732* Lemma for mapdpg 34739. Baer p. 45 line 16: "v(x'-y'') = x'-y'" (with equality swapped). (Contributed by NM, 22-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( h  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) ) )   &    |-  ( ph  ->  ( i  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { i } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R i ) }
 ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  ( Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  O  =  ( 0g `  A )   =>    |-  ( ph  ->  E. v  e.  ( B  \  { O } ) ( G R h )  =  ( v  .x.  ( G R i ) ) )
 
Theoremmapdpglem29 34733* Lemma for mapdpg 34739. Baer p. 45 line 16: "But Gx' and Gy'' are distinct points and so x' and y'' are independent elements in B. (Contributed by NM, 22-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( h  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) ) )   &    |-  ( ph  ->  ( i  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { i } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R i ) }
 ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  ( Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  O  =  ( 0g `  A )   &    |-  ( ph  ->  v  e.  B )   &    |-  ( ph  ->  h  =  ( u  .x.  i ) )   &    |-  ( ph  ->  ( G R h )  =  (
 v  .x.  ( G R i ) ) )   =>    |-  ( ph  ->  ( J `  { G }
 )  =/=  ( J ` 
 { i } )
 )
 
Theoremmapdpglem28 34734* Lemma for mapdpg 34739. Baer p. 45 line 18: "vx'-vy'' = x'-uy''". (Contributed by NM, 22-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( h  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) ) )   &    |-  ( ph  ->  ( i  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { i } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R i ) }
 ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  ( Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  O  =  ( 0g `  A )   &    |-  ( ph  ->  v  e.  B )   &    |-  ( ph  ->  h  =  ( u  .x.  i ) )   &    |-  ( ph  ->  ( G R h )  =  (
 v  .x.  ( G R i ) ) )   =>    |-  ( ph  ->  (
 ( v  .x.  G ) R ( v  .x.  i ) )  =  ( G R ( u  .x.  i )
 ) )
 
Theoremmapdpglem30 34735* Lemma for mapdpg 34739. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 34734, using lvecindp2 18107) that v = 1 and v = u...". TODO: would it be shorter to have only the  v  =  ( 1r `  A ) part and use mapdpglem28.u2 in mapdpglem31 34736? (Contributed by NM, 22-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( h  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) ) )   &    |-  ( ph  ->  ( i  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { i } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R i ) }
 ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  ( Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  O  =  ( 0g `  A )   &    |-  ( ph  ->  v  e.  B )   &    |-  ( ph  ->  h  =  ( u  .x.  i ) )   &    |-  ( ph  ->  ( G R h )  =  (
 v  .x.  ( G R i ) ) )   &    |-  ( ph  ->  u  e.  B )   =>    |-  ( ph  ->  ( v  =  ( 1r
 `  A )  /\  v  =  u )
 )
 
Theoremmapdpglem31 34736* Lemma for mapdpg 34739. Baer p. 45 line 19: "...and we have consequently that y' = y'', as we claimed." (Contributed by NM, 23-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   &    |-  ( ph  ->  ( h  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) ) )   &    |-  ( ph  ->  ( i  e.  F  /\  ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { i } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R i ) }
 ) ) ) )   &    |-  A  =  (Scalar `  U )   &    |-  B  =  ( Base `  A )   &    |-  .x.  =  ( .s `  C )   &    |-  O  =  ( 0g `  A )   &    |-  ( ph  ->  v  e.  B )   &    |-  ( ph  ->  h  =  ( u  .x.  i ) )   &    |-  ( ph  ->  ( G R h )  =  (
 v  .x.  ( G R i ) ) )   &    |-  ( ph  ->  u  e.  B )   =>    |-  ( ph  ->  h  =  i )
 
Theoremmapdpglem24 34737* Lemma for mapdpg 34739. Existence part - consolidate hypotheses in mapdpglem23 34727. (Contributed by NM, 21-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   =>    |-  ( ph  ->  E. h  e.  F  ( ( M `  ( N `  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) )
 
Theoremmapdpglem32 34738* Lemma for mapdpg 34739. Uniqueness part - consolidate hypotheses in mapdpglem31 34736. (Contributed by NM, 23-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   =>    |-  ( ( ph  /\  ( h  e.  F  /\  i  e.  F )  /\  ( ( ( M `  ( N `
  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) )  /\  (
 ( M `  ( N `  { Y }
 ) )  =  ( J `  { i } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R i ) }
 ) ) ) ) 
 ->  h  =  i
 )
 
Theoremmapdpg 34739* Part 1 of proof of the first fundamental theorem of projective geometry. Part (1) in [Baer] p. 44. Our notation corresponds to Baer's as follows:  M for *,  N `  { } for F(),  J `  { } for G(),  X for x,  G for x',  Y for y,  h for y'. TODO: Rename variables per mapdhval 34757. (Contributed by NM, 22-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .-  =  ( -g `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  R  =  ( -g `  C )   &    |-  J  =  ( LSpan `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { G } ) )   =>    |-  ( ph  ->  E! h  e.  F  ( ( M `  ( N `  { Y }
 ) )  =  ( J `  { h } )  /\  ( M `
  ( N `  { ( X  .-  Y ) } )
 )  =  ( J `
  { ( G R h ) }
 ) ) )
 
Theorembaerlem3lem1 34740 Lemma for baerlem3 34746. (Contributed by NM, 9-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  R  =  (Scalar `  W )   &    |-  B  =  (
 Base `  R )   &    |-  .+^  =  (
 +g  `  R )   &    |-  L  =  ( -g `  R )   &    |-  Q  =  ( 0g
 `  R )   &    |-  I  =  ( invg `  R )   &    |-  ( ph  ->  a  e.  B )   &    |-  ( ph  ->  b  e.  B )   &    |-  ( ph  ->  d  e.  B )   &    |-  ( ph  ->  e  e.  B )   &    |-  ( ph  ->  j  =  ( ( a  .x.  Y )  .+  ( b  .x.  Z ) ) )   &    |-  ( ph  ->  j  =  ( ( d  .x.  ( X  .-  Y ) ) 
 .+  ( e  .x.  ( X  .-  Z ) ) ) )   =>    |-  ( ph  ->  j  =  ( a  .x.  ( Y  .-  Z ) ) )
 
Theorembaerlem5alem1 34741 Lemma for baerlem5a 34747. (Contributed by NM, 13-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  R  =  (Scalar `  W )   &    |-  B  =  (
 Base `  R )   &    |-  .+^  =  (
 +g  `  R )   &    |-  L  =  ( -g `  R )   &    |-  Q  =  ( 0g
 `  R )   &    |-  I  =  ( invg `  R )   &    |-  ( ph  ->  a  e.  B )   &    |-  ( ph  ->  b  e.  B )   &    |-  ( ph  ->  d  e.  B )   &    |-  ( ph  ->  e  e.  B )   &    |-  ( ph  ->  j  =  ( ( a  .x.  ( X  .-  Y ) ) 
 .+  ( b  .x.  Z ) ) )   &    |-  ( ph  ->  j  =  ( ( d  .x.  ( X  .-  Z ) ) 
 .+  ( e  .x.  Y ) ) )   =>    |-  ( ph  ->  j  =  ( a  .x.  ( X  .-  ( Y 
 .+  Z ) ) ) )
 
Theorembaerlem5blem1 34742 Lemma for baerlem5b 34748. (Contributed by NM, 9-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  R  =  (Scalar `  W )   &    |-  B  =  (
 Base `  R )   &    |-  .+^  =  (
 +g  `  R )   &    |-  L  =  ( -g `  R )   &    |-  Q  =  ( 0g
 `  R )   &    |-  I  =  ( invg `  R )   &    |-  ( ph  ->  a  e.  B )   &    |-  ( ph  ->  b  e.  B )   &    |-  ( ph  ->  d  e.  B )   &    |-  ( ph  ->  e  e.  B )   &    |-  ( ph  ->  j  =  ( ( a  .x.  Y )  .+  ( b  .x.  Z ) ) )   &    |-  ( ph  ->  j  =  ( ( d  .x.  ( X  .-  ( Y  .+  Z ) ) ) 
 .+  ( e  .x.  X ) ) )   =>    |-  ( ph  ->  j  =  ( ( I `
  d )  .x.  ( Y  .+  Z ) ) )
 
Theorembaerlem3lem2 34743 Lemma for baerlem3 34746. (Contributed by NM, 9-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  R  =  (Scalar `  W )   &    |-  B  =  (
 Base `  R )   &    |-  .+^  =  (
 +g  `  R )   &    |-  L  =  ( -g `  R )   &    |-  Q  =  ( 0g
 `  R )   &    |-  I  =  ( invg `  R )   =>    |-  ( ph  ->  ( N `  { ( Y 
 .-  Z ) }
 )  =  ( ( ( N `  { Y } )  .(+)  ( N `
  { Z }
 ) )  i^i  (
 ( N `  { ( X  .-  Y ) }
 )  .(+)  ( N `  { ( X  .-  Z ) } )
 ) ) )
 
Theorembaerlem5alem2 34744 Lemma for baerlem5a 34747. (Contributed by NM, 9-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  R  =  (Scalar `  W )   &    |-  B  =  (
 Base `  R )   &    |-  .+^  =  (
 +g  `  R )   &    |-  L  =  ( -g `  R )   &    |-  Q  =  ( 0g
 `  R )   &    |-  I  =  ( invg `  R )   =>    |-  ( ph  ->  ( N `  { ( X 
 .-  ( Y  .+  Z ) ) }
 )  =  ( ( ( N `  { ( X  .-  Y ) }
 )  .(+)  ( N `  { Z } ) )  i^i  ( ( N `
  { ( X 
 .-  Z ) }
 )  .(+)  ( N `  { Y } ) ) ) )
 
Theorembaerlem5blem2 34745 Lemma for baerlem5b 34748. (Contributed by NM, 13-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   &    |- 
 .x.  =  ( .s `  W )   &    |-  R  =  (Scalar `  W )   &    |-  B  =  (
 Base `  R )   &    |-  .+^  =  (
 +g  `  R )   &    |-  L  =  ( -g `  R )   &    |-  Q  =  ( 0g
 `  R )   &    |-  I  =  ( invg `  R )   =>    |-  ( ph  ->  ( N `  { ( Y 
 .+  Z ) }
 )  =  ( ( ( N `  { Y } )  .(+)  ( N `
  { Z }
 ) )  i^i  (
 ( N `  { ( X  .-  ( Y  .+  Z ) ) }
 )  .(+)  ( N `  { X } ) ) ) )
 
Theorembaerlem3 34746 An equality that holds when  X,  Y,  Z are independent (non-colinear) vectors. Part (3) in [Baer] p. 45. TODO fix ref. (Contributed by NM, 9-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( N ` 
 { ( Y  .-  Z ) } )  =  ( ( ( N `
  { Y }
 )  .(+)  ( N `  { Z } ) )  i^i  ( ( N `
  { ( X 
 .-  Y ) }
 )  .(+)  ( N `  { ( X  .-  Z ) } )
 ) ) )
 
Theorembaerlem5a 34747 An equality that holds when  X,  Y,  Z are independent (non-colinear) vectors. First equation of part (5) in [Baer] p. 46. (Contributed by NM, 10-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   =>    |-  ( ph  ->  ( N `  { ( X 
 .-  ( Y  .+  Z ) ) }
 )  =  ( ( ( N `  { ( X  .-  Y ) }
 )  .(+)  ( N `  { Z } ) )  i^i  ( ( N `
  { ( X 
 .-  Z ) }
 )  .(+)  ( N `  { Y } ) ) ) )
 
Theorembaerlem5b 34748 An equality that holds when  X,  Y,  Z are independent (non-colinear) vectors. Second equation of part (5) in [Baer] p. 46. (Contributed by NM, 13-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   =>    |-  ( ph  ->  ( N `  { ( Y 
 .+  Z ) }
 )  =  ( ( ( N `  { Y } )  .(+)  ( N `
  { Z }
 ) )  i^i  (
 ( N `  { ( X  .-  ( Y  .+  Z ) ) }
 )  .(+)  ( N `  { X } ) ) ) )
 
Theorembaerlem5amN 34749 An equality that holds when  X,  Y,  Z are independent (non-colinear) vectors. Subtraction version of first equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 34751 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   =>    |-  ( ph  ->  ( N `  { ( X 
 .-  ( Y  .-  Z ) ) }
 )  =  ( ( ( N `  { ( X  .-  Y ) }
 )  .(+)  ( N `  { Z } ) )  i^i  ( ( N `
  { ( X 
 .+  Z ) }
 )  .(+)  ( N `  { Y } ) ) ) )
 
Theorembaerlem5bmN 34750 An equality that holds when  X,  Y,  Z are independent (non-colinear) vectors. Subtraction version of second equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 34751 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   =>    |-  ( ph  ->  ( N `  { ( Y 
 .-  Z ) }
 )  =  ( ( ( N `  { Y } )  .(+)  ( N `
  { Z }
 ) )  i^i  (
 ( N `  { ( X  .-  ( Y  .-  Z ) ) }
 )  .(+)  ( N `  { X } ) ) ) )
 
Theorembaerlem5abmN 34751 An equality that holds when  X,  Y,  Z are independent (non-colinear) vectors. Subtraction versions of first and second equations of part (5) in [Baer] p. 46, conjoined to share commonality in their proofs. TODO: Delete if not be needed. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  .-  =  ( -g `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  .(+)  =  ( LSSum `  W )   &    |-  N  =  (
 LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  -.  X  e.  ( N `
  { Y ,  Z } ) )   &    |-  ( ph  ->  ( N `  { Y } )  =/=  ( N `  { Z } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Z  e.  ( V  \  {  .0.  } ) )   &    |-  .+  =  ( +g  `  W )   =>    |-  ( ph  ->  (
 ( N `  { ( X  .-  ( Y  .-  Z ) ) }
 )  =  ( ( ( N `  { ( X  .-  Y ) }
 )  .(+)  ( N `  { Z } ) )  i^i  ( ( N `
  { ( X 
 .+  Z ) }
 )  .(+)  ( N `  { Y } ) ) )  /\  ( N `
  { ( Y 
 .-  Z ) }
 )  =  ( ( ( N `  { Y } )  .(+)  ( N `
  { Z }
 ) )  i^i  (
 ( N `  { ( X  .-  ( Y  .-  Z ) ) }
 )  .(+)  ( N `  { X } ) ) ) ) )
 
Theoremmapdindp0 34752 Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
 |-  V  =  ( Base `  W )   &    |-  .+  =  ( +g  `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  N  =  ( LSpan `  W )   &    |-  ( ph  ->  W  e.  LVec )   &    |-  ( ph  ->  X  e.  ( V