HomeHome Metamath Proof Explorer
Theorem List (p. 378 of 386)
< 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-26036)
  Hilbert Space Explorer  Hilbert Space Explorer
(26037-27561)
  Users' Mathboxes  Users' Mathboxes
(27562-38552)
 

Theorem List for Metamath Proof Explorer - 37701-37800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlcfrlem16 37701* Lemma for lcfr 37728. (Contributed by NM, 8-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  ( Base `  S )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( 0g `  D )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `
  f ) ) )  =  ( L `
  f ) }   &    |-  J  =  ( x  e.  ( V  \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  P  =  ( LSubSp `  D )   &    |-  ( ph  ->  G  e.  P )   &    |-  ( ph  ->  G  C_  C )   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  X  e.  ( E  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( J `  X )  e.  G )
 
Theoremlcfrlem17 37702 Lemma for lcfr 37728. Condition needed more than once. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  ( V  \  {  .0.  } ) )
 
Theoremlcfrlem18 37703 Lemma for lcfr 37728. (Contributed by NM, 24-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   =>    |-  ( ph  ->  (  ._|_  `  { X ,  Y } )  =  ( (  ._|_  `  { X } )  i^i  (  ._|_  ` 
 { Y } )
 ) )
 
Theoremlcfrlem19 37704 Lemma for lcfr 37728. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   =>    |-  ( ph  ->  ( -.  X  e.  (  ._|_  ` 
 { ( X  .+  Y ) } )  \/  -.  Y  e.  (  ._|_  `  { ( X 
 .+  Y ) }
 ) ) )
 
Theoremlcfrlem20 37705 Lemma for lcfr 37728. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  ( ph  ->  -.  X  e.  (  ._|_  ` 
 { ( X  .+  Y ) } )
 )   =>    |-  ( ph  ->  (
 ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )  e.  A )
 
Theoremlcfrlem21 37706 Lemma for lcfr 37728. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   =>    |-  ( ph  ->  (
 ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )  e.  A )
 
Theoremlcfrlem22 37707 Lemma for lcfr 37728. (Contributed by NM, 24-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   =>    |-  ( ph  ->  B  e.  A )
 
Theoremlcfrlem23 37708 Lemma for lcfr 37728. TODO: this proof was built from other proof pieces that may change  N `  { X ,  Y } into subspace sum and back unnecessarily, or similar things. (Contributed by NM, 1-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .(+)  =  ( LSSum `  U )   =>    |-  ( ph  ->  (
 (  ._|_  `  { X ,  Y } )  .(+)  B )  =  (  ._|_  `  { ( X  .+  Y ) }
 ) )
 
Theoremlcfrlem24 37709* Lemma for lcfr 37728. (Contributed by NM, 24-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   =>    |-  ( ph  ->  (  ._|_  `  { X ,  Y } )  =  ( ( L `  ( J `  X ) )  i^i  ( L `  ( J `  Y ) ) ) )
 
Theoremlcfrlem25 37710* Lemma for lcfr 37728. Special case of lcfrlem35 37720 when  ( ( J `
 Y ) `  I ) is zero. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =  Q )   &    |-  ( ph  ->  I  =/=  .0.  )   =>    |-  ( ph  ->  ( 
 ._|_  `  { ( X 
 .+  Y ) }
 )  =  ( L `
  ( J `  Y ) ) )
 
Theoremlcfrlem26 37711* Lemma for lcfr 37728. Special case of lcfrlem36 37721 when  ( ( J `
 Y ) `  I ) is zero. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =  Q )   &    |-  ( ph  ->  I  =/=  .0.  )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  (  ._|_  `  ( L `  ( J `  Y ) ) ) )
 
Theoremlcfrlem27 37712* Lemma for lcfr 37728. Special case of lcfrlem37 37722 when  ( ( J `
 Y ) `  I ) is zero. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =  Q )   &    |-  ( ph  ->  I  =/=  .0.  )   &    |-  ( ph  ->  G  e.  ( LSubSp `
  D ) )   &    |-  ( ph  ->  G  C_  { f  e.  (LFnl `  U )  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) } )   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  X  e.  E )   &    |-  ( ph  ->  Y  e.  E )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  E )
 
Theoremlcfrlem28 37713* Lemma for lcfr 37728. TODO: This can be a hypothesis since the zero version of  ( J `  Y ) `  I needs it. (Contributed by NM, 9-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   =>    |-  ( ph  ->  I  =/=  .0.  )
 
Theoremlcfrlem29 37714* Lemma for lcfr 37728. (Contributed by NM, 9-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   &    |-  F  =  (
 invr `  S )   =>    |-  ( ph  ->  ( ( F `  (
 ( J `  Y ) `  I ) ) ( .r `  S ) ( ( J `
  X ) `  I ) )  e.  R )
 
Theoremlcfrlem30 37715* Lemma for lcfr 37728. (Contributed by NM, 6-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   &    |-  F  =  (
 invr `  S )   &    |-  .-  =  ( -g `  D )   &    |-  C  =  ( ( J `  X )  .-  ( ( ( F `
  ( ( J `
  Y ) `  I ) ) ( .r `  S ) ( ( J `  X ) `  I
 ) ) ( .s
 `  D ) ( J `  Y ) ) )   =>    |-  ( ph  ->  C  e.  (LFnl `  U )
 )
 
Theoremlcfrlem31 37716* Lemma for lcfr 37728. (Contributed by NM, 10-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   &    |-  F  =  (
 invr `  S )   &    |-  .-  =  ( -g `  D )   &    |-  C  =  ( ( J `  X )  .-  ( ( ( F `
  ( ( J `
  Y ) `  I ) ) ( .r `  S ) ( ( J `  X ) `  I
 ) ) ( .s
 `  D ) ( J `  Y ) ) )   &    |-  ( ph  ->  ( ( J `  X ) `  I )  =/= 
 Q )   &    |-  ( ph  ->  C  =  ( 0g `  D ) )   =>    |-  ( ph  ->  ( N `  { X } )  =  ( N `  { Y }
 ) )
 
Theoremlcfrlem32 37717* Lemma for lcfr 37728. (Contributed by NM, 10-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   &    |-  F  =  (
 invr `  S )   &    |-  .-  =  ( -g `  D )   &    |-  C  =  ( ( J `  X )  .-  ( ( ( F `
  ( ( J `
  Y ) `  I ) ) ( .r `  S ) ( ( J `  X ) `  I
 ) ) ( .s
 `  D ) ( J `  Y ) ) )   &    |-  ( ph  ->  ( ( J `  X ) `  I )  =/= 
 Q )   =>    |-  ( ph  ->  C  =/=  ( 0g `  D ) )
 
Theoremlcfrlem33 37718* Lemma for lcfr 37728. (Contributed by NM, 10-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   &    |-  F  =  (
 invr `  S )   &    |-  .-  =  ( -g `  D )   &    |-  C  =  ( ( J `  X )  .-  ( ( ( F `
  ( ( J `
  Y ) `  I ) ) ( .r `  S ) ( ( J `  X ) `  I
 ) ) ( .s
 `  D ) ( J `  Y ) ) )   &    |-  ( ph  ->  ( ( J `  X ) `  I )  =  Q )   =>    |-  ( ph  ->  C  =/=  ( 0g `  D ) )
 
Theoremlcfrlem34 37719* Lemma for lcfr 37728. (Contributed by NM, 10-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   &    |-  F  =  (
 invr `  S )   &    |-  .-  =  ( -g `  D )   &    |-  C  =  ( ( J `  X )  .-  ( ( ( F `
  ( ( J `
  Y ) `  I ) ) ( .r `  S ) ( ( J `  X ) `  I
 ) ) ( .s
 `  D ) ( J `  Y ) ) )   =>    |-  ( ph  ->  C  =/=  ( 0g `  D ) )
 
Theoremlcfrlem35 37720* Lemma for lcfr 37728. (Contributed by NM, 2-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   &    |-  F  =  (
 invr `  S )   &    |-  .-  =  ( -g `  D )   &    |-  C  =  ( ( J `  X )  .-  ( ( ( F `
  ( ( J `
  Y ) `  I ) ) ( .r `  S ) ( ( J `  X ) `  I
 ) ) ( .s
 `  D ) ( J `  Y ) ) )   =>    |-  ( ph  ->  (  ._|_  `  { ( X 
 .+  Y ) }
 )  =  ( L `
  C ) )
 
Theoremlcfrlem36 37721* Lemma for lcfr 37728. (Contributed by NM, 6-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   &    |-  F  =  (
 invr `  S )   &    |-  .-  =  ( -g `  D )   &    |-  C  =  ( ( J `  X )  .-  ( ( ( F `
  ( ( J `
  Y ) `  I ) ) ( .r `  S ) ( ( J `  X ) `  I
 ) ) ( .s
 `  D ) ( J `  Y ) ) )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  (  ._|_  `  ( L `
  C ) ) )
 
Theoremlcfrlem37 37722* Lemma for lcfr 37728. (Contributed by NM, 8-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y }
 ) )   &    |-  B  =  ( ( N `  { X ,  Y } )  i^i  (  ._|_  `  { ( X  .+  Y ) }
 ) )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   &    |-  ( ph  ->  I  e.  B )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( ( J `  Y ) `  I )  =/= 
 Q )   &    |-  F  =  (
 invr `  S )   &    |-  .-  =  ( -g `  D )   &    |-  C  =  ( ( J `  X )  .-  ( ( ( F `
  ( ( J `
  Y ) `  I ) ) ( .r `  S ) ( ( J `  X ) `  I
 ) ) ( .s
 `  D ) ( J `  Y ) ) )   &    |-  ( ph  ->  G  e.  ( LSubSp `  D ) )   &    |-  ( ph  ->  G 
 C_  { f  e.  (LFnl `  U )  |  ( 
 ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }
 )   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  X  e.  E )   &    |-  ( ph  ->  Y  e.  E )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  E )
 
Theoremlcfrlem38 37723* Lemma for lcfr 37728. Combine lcfrlem27 37712 and lcfrlem37 37722. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( LSubSp `  D )   &    |-  C  =  { f  e.  (LFnl `  U )  |  ( 
 ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  Q )   &    |-  ( ph  ->  G  C_  C )   &    |-  ( ph  ->  X  e.  E )   &    |-  ( ph  ->  Y  e.  E )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  =/=  .0.  )   &    |-  ( ph  ->  Y  =/=  .0.  )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  B  =  ( ( N `  { X ,  Y }
 )  i^i  (  ._|_  ` 
 { ( X  .+  Y ) } )
 )   &    |-  ( ph  ->  I  e.  B )   &    |-  ( ph  ->  I  =/=  .0.  )   &    |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  ( Base `  S )   &    |-  J  =  ( x  e.  ( V 
 \  {  .0.  }
 )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
 k  .x.  x )
 ) ) ) )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  E )
 
Theoremlcfrlem39 37724* Lemma for lcfr 37728. Eliminate  J. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( LSubSp `  D )   &    |-  C  =  { f  e.  (LFnl `  U )  |  ( 
 ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  Q )   &    |-  ( ph  ->  G  C_  C )   &    |-  ( ph  ->  X  e.  E )   &    |-  ( ph  ->  Y  e.  E )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  =/=  .0.  )   &    |-  ( ph  ->  Y  =/=  .0.  )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   &    |-  B  =  ( ( N `  { X ,  Y }
 )  i^i  (  ._|_  ` 
 { ( X  .+  Y ) } )
 )   &    |-  ( ph  ->  I  e.  B )   &    |-  ( ph  ->  I  =/=  .0.  )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  E )
 
Theoremlcfrlem40 37725* Lemma for lcfr 37728. Eliminate  B and  I. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( LSubSp `  D )   &    |-  C  =  { f  e.  (LFnl `  U )  |  ( 
 ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  Q )   &    |-  ( ph  ->  G  C_  C )   &    |-  ( ph  ->  X  e.  E )   &    |-  ( ph  ->  Y  e.  E )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  =/=  .0.  )   &    |-  ( ph  ->  Y  =/=  .0.  )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  E )
 
Theoremlcfrlem41 37726* Lemma for lcfr 37728. Eliminate span condition. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( LSubSp `  D )   &    |-  C  =  { f  e.  (LFnl `  U )  |  ( 
 ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  Q )   &    |-  ( ph  ->  G  C_  C )   &    |-  ( ph  ->  X  e.  E )   &    |-  ( ph  ->  Y  e.  E )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  =/=  .0.  )   &    |-  ( ph  ->  Y  =/=  .0.  )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  E )
 
Theoremlcfrlem42 37727* Lemma for lcfr 37728. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( LSubSp `  D )   &    |-  C  =  { f  e.  (LFnl `  U )  |  ( 
 ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  Q )   &    |-  ( ph  ->  G  C_  C )   &    |-  ( ph  ->  X  e.  E )   &    |-  ( ph  ->  Y  e.  E )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  E )
 
Theoremlcfr 37728* Reconstruction of a subspace from a dual subspace of functionals with closed kernels. Our proof was suggested by Mario Carneiro, 20-Feb-2015. (Contributed by NM, 5-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  T  =  ( LSubSp `  D )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  Q  =  U_ g  e.  R  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  R  e.  T )   &    |-  ( ph  ->  R  C_  C )   =>    |-  ( ph  ->  Q  e.  S )
 
Syntaxclcd 37729 Extend class notation with vector space of functionals with closed kernels.
 class LCDual
 
Definitiondf-lcdual 37730* Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 37792. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 37768 using  ( Base `  (
(LCDual `  K ) `  W ) ). (Contributed by NM, 13-Mar-2015.)
 |- LCDual  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( (LDual `  ( ( DVecH `  k
 ) `  w )
 )s  { f  e.  (LFnl `  ( ( DVecH `  k
 ) `  w )
 )  |  ( ( ( ocH `  k
 ) `  w ) `  ( ( ( ocH `  k ) `  w ) `  ( (LKer `  ( ( DVecH `  k
 ) `  w )
 ) `  f )
 ) )  =  ( (LKer `  ( ( DVecH `  k ) `  w ) ) `  f ) } )
 ) )
 
Theoremlcdfval 37731* Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   =>    |-  ( K  e.  X  ->  (LCDual `  K )  =  ( w  e.  H  |->  ( (LDual `  ( ( DVecH `  K ) `  w ) )s  { f  e.  (LFnl `  ( ( DVecH `  K ) `  w ) )  |  ( ( ( ocH `  K ) `  w ) `  ( ( ( ocH `  K ) `  w ) `  (
 (LKer `  ( ( DVecH `  K ) `  w ) ) `  f ) ) )  =  ( (LKer `  ( ( DVecH `  K ) `  w ) ) `
  f ) }
 ) ) )
 
Theoremlcdval 37732* Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( K  e.  X  /\  W  e.  H ) )   =>    |-  ( ph  ->  C  =  ( Ds  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) } )
 )
 
Theoremlcdval2 37733* Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  ( ph  ->  ( K  e.  X  /\  W  e.  H ) )   &    |-  B  =  {
 f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }   =>    |-  ( ph  ->  C  =  ( Ds  B ) )
 
Theoremlcdlvec 37734 The dual vector space of functionals with closed kernels is a left vector space. (Contributed by NM, 14-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  C  e.  LVec )
 
Theoremlcdlmod 37735 The dual vector space of functionals with closed kernels is a left module. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  C  e.  LMod )
 
Theoremlcdvbase 37736* Vector base set of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  V  =  ( Base `  C )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  B  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  V  =  B )
 
Theoremlcdvbasess 37737 The vector base set of the closed kernel dual space is a set of functionals. (Contributed by NM, 15-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  V  =  ( Base `  C )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  V  C_  F )
 
Theoremlcdvbaselfl 37738 A vector in the base set of the closed kernel dual space is a functional. (Contributed by NM, 28-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  V  =  ( Base `  C )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  X  e.  F )
 
Theoremlcdvbasecl 37739 Closure of the value of a vector (functional) in the closed kernel dual space. (Contributed by NM, 28-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  ( Base `  S )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  E  =  ( Base `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  E )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  ( F `  X )  e.  R )
 
Theoremlcdvadd 37740 Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  .+b  =  .+  )
 
Theoremlcdvaddval 37741 The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  .+  =  ( +g  `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  D  =  ( Base `  C )   &    |-  .+b  =  ( +g  `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  F  e.  D )   &    |-  ( ph  ->  G  e.  D )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  (
 ( F  .+b  G ) `
  X )  =  ( ( F `  X )  .+  ( G `
  X ) ) )
 
Theoremlcdsca 37742 The ring of scalars of the closed kernel dual space. (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  O  =  (oppr `  F )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  R  =  (Scalar `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   =>    |-  ( ph  ->  R  =  O )
 
Theoremlcdsbase 37743 Base set of scalar ring for the closed kernel dual of a vector space. (Contributed by NM, 18-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  L  =  ( Base `  F )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  S  =  (Scalar `  C )   &    |-  R  =  ( Base `  S )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  R  =  L )
 
Theoremlcdsadd 37744 Scalar addition for the closed kernel vector space dual. (Contributed by NM, 6-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  .+  =  ( +g  `  F )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  S  =  (Scalar `  C )   &    |-  .+b  =  ( +g  `  S )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  .+b  =  .+  )
 
Theoremlcdsmul 37745 Scalar multiplication for the closed kernel vector space dual. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  L  =  ( Base `  F )   &    |-  .x.  =  ( .r `  F )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  S  =  (Scalar `  C )   &    |-  .xb  =  ( .r `  S )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  L )   &    |-  ( ph  ->  Y  e.  L )   =>    |-  ( ph  ->  ( X  .xb  Y )  =  ( Y  .x.  X ) )
 
Theoremlcdvs 37746 Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  D  =  (LDual `  U )   &    |-  .x.  =  ( .s `  D )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .xb  =  ( .s `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   =>    |-  ( ph  ->  .xb  =  .x.  )
 
Theoremlcdvsval 37747 Value of scalar product operation value for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  ( Base `  S )   &    |-  .x.  =  ( .r `  S )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  F  =  ( Base `  C )   &    |-  .xb  =  ( .s `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  R )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  A  e.  V )   =>    |-  ( ph  ->  (
 ( X  .xb  G ) `
  A )  =  ( ( G `  A )  .x.  X ) )
 
Theoremlcdvscl 37748 The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  (Scalar `  U )   &    |-  R  =  ( Base `  S )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  V  =  ( Base `  C )   &    |-  .x.  =  ( .s `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  R )   &    |-  ( ph  ->  G  e.  V )   =>    |-  ( ph  ->  ( X  .x.  G )  e.  V )
 
Theoremlcdlssvscl 37749 Closure of scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  R  =  ( Base `  F )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  V  =  ( Base `  C )   &    |-  .x.  =  ( .s `  C )   &    |-  S  =  ( LSubSp `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  L  e.  S )   &    |-  ( ph  ->  X  e.  R )   &    |-  ( ph  ->  Y  e.  L )   =>    |-  ( ph  ->  ( X  .x.  Y )  e.  L )
 
Theoremlcdvsass 37750 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 37751 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 37752 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 37753 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  =  ( invg `  R )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  S  =  (Scalar `  C )   &    |-  N  =  ( invg `  S )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  N  =  M )
 
Theoremlcd0v 37754 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 37755 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 37756 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 37757 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 37758 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 37759 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 37760 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  =  ( invg `  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 37761 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 37762* 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 37763 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 37764 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 37765 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 37766 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 37767 Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels.
 class mapd
 
Definitiondf-mapd 37768* Extend class notation with a one-to-one onto (mapd1o 37791), order-preserving (mapdord 37781) 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 37769* 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 37770* 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 37771* 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 37772* 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 37773* 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 37774* 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 37775* 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 37646 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 37776* 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 37777* Lemma for mapdord 37781. (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 37778* Lemma for mapdord 37781. (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 37779* Lemma for mapdord 37781. (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 37780* Lemma for mapdord 37781. 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 37781 Ordering property of the map defined by df-mapd 37768. 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 37782 The map defined by df-mapd 37768 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 37783 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 37799 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 37784* Value of the map defined by df-mapd 37768 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 37785* Value of the map defined by df-mapd 37768 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 37786 Value of the map defined by df-mapd 37768 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 37787* Value of the map defined by df-mapd 37768 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 37788* Lemma for mapdrval 37790. TODO: very long antecedents 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 37789* Lemma for mapdrval 37790. (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 37790* 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 37791* The map defined by df-mapd 37768 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 37728, mapdrval 37790, lclkrs 37682, lclkr 37676,...) to use  T  i^i  ~P C? TODO: maybe get rid of $d's for  g vs.  K U W,. propagate to mapdrn 37792 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 37792* Range of the map defined by df-mapd 37768. (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 37793* Union of the range of the map defined by df-mapd 37768. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `