HomeHome Metamath Proof Explorer
Theorem List (p. 347 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 - 34601-34700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlcfrlem26 34601* Lemma for lcfr 34618. Special case of lcfrlem36 34611 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 34602* Lemma for lcfr 34618. Special case of lcfrlem37 34612 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 34603* Lemma for lcfr 34618. 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 34604* Lemma for lcfr 34618. (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 34605* Lemma for lcfr 34618. (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 34606* Lemma for lcfr 34618. (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 34607* Lemma for lcfr 34618. (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 34608* Lemma for lcfr 34618. (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 34609* Lemma for lcfr 34618. (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 34610* Lemma for lcfr 34618. (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 34611* Lemma for lcfr 34618. (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 34612* Lemma for lcfr 34618. (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 34613* Lemma for lcfr 34618. Combine lcfrlem27 34602 and lcfrlem37 34612. (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 34614* Lemma for lcfr 34618. 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 34615* Lemma for lcfr 34618. 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 34616* Lemma for lcfr 34618. 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 34617* Lemma for lcfr 34618. 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 34618* 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 34619 Extend class notation with vector space of functionals with closed kernels.
 class LCDual
 
Definitiondf-lcdual 34620* Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 34682. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 34658 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 34621* 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 34622* 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 34623* 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 34624 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 34625 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 34626* 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 34627 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 34628 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 34629 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 34630 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 34631 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 34632 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 34633 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 34634 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 34635 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 34636 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 34637 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 34638 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 34639 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 34640 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 34641 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 34642 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 34643 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 34644 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 34645 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 34646 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 34647 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 34648 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 34649 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 34650 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 34651 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 34652* 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 34653 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 34654 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 34655 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 34656 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 34657 Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels.
 class mapd
 
Definitiondf-mapd 34658* Extend class notation with a one-to-one onto (mapd1o 34681), order-preserving (mapdord 34671) 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 34659* 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 34660* 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 34661* 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 34662* 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 34663* 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 34664* 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 34665* 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 34536 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 34666* 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 34667* Lemma for mapdord 34671. (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 34668* Lemma for mapdord 34671. (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 34669* Lemma for mapdord 34671. (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 34670* Lemma for mapdord 34671. 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 34671 Ordering property of the map defined by df-mapd 34658. 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 34672 The map defined by df-mapd 34658 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 34673 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 34689 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 34674* Value of the map defined by df-mapd 34658 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 34675* Value of the map defined by df-mapd 34658 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 34676 Value of the map defined by df-mapd 34658 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 34677* Value of the map defined by df-mapd 34658 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 34678* Lemma for mapdrval 34680. 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 34679* Lemma for mapdrval 34680. (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 34680* 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 34681* The map defined by df-mapd 34658 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 34618, mapdrval 34680, lclkrs 34572, lclkr 34566,...) to use  T  i^i  ~P C? TODO: maybe get rid of $d's for  g vs.  K U W,. propagate to mapdrn 34682 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 34682* Range of the map defined by df-mapd 34658. (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 34683* Union of the range of the map defined by df-mapd 34658. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  O  =  ( ( ocH `  K ) `  W )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  C  =  { g  e.  F  |  ( O `  ( O `  ( L `  g ) ) )  =  ( L `  g ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  U. ran  M  =  C )
 
Theoremmapdrn2 34684 Range of the map defined by df-mapd 34658. TODO: this seems to be needed a lot in hdmaprnlem3eN 34894 etc. Would it be better to change df-mapd 34658 theorems to use  LSubSp `  C instead of  ran  M? (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  T  =  ( LSubSp `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ran  M  =  T )
 
Theoremmapdcnvcl 34685 Closure of the converse of the map defined by df-mapd 34658. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   =>    |-  ( ph  ->  ( `' M `  X )  e.  S )
 
Theoremmapdcl 34686 Closure the value of the map defined by df-mapd 34658. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   =>    |-  ( ph  ->  ( M `  X )  e.  ran  M )
 
Theoremmapdcnvid1N 34687 Converse of the value of the map defined by df-mapd 34658. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   =>    |-  ( ph  ->  ( `' M `  ( M `
  X ) )  =  X )
 
Theoremmapdsord 34688 Strong ordering property of themap defined by df-mapd 34658. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  (
 ( M `  X )  C.  ( M `  Y )  <->  X  C.  Y ) )
 
Theoremmapdcl2 34689 The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  T  =  ( LSubSp `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  R  e.  S )   =>    |-  ( ph  ->  ( M `  R )  e.  T )
 
Theoremmapdcnvid2 34690 Value of the converse of the map defined by df-mapd 34658. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   =>    |-  ( ph  ->  ( M `  ( `' M `  X ) )  =  X )
 
TheoremmapdcnvordN 34691 Ordering property of the converse of the map defined by df-mapd 34658. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   &    |-  ( ph  ->  Y  e.  ran  M )   =>    |-  ( ph  ->  (
 ( `' M `  X )  C_  ( `' M `  Y )  <->  X  C_  Y ) )
 
Theoremmapdcnv11N 34692 The converse of the map defined by df-mapd 34658 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   &    |-  ( ph  ->  Y  e.  ran  M )   =>    |-  ( ph  ->  (
 ( `' M `  X )  =  ( `' M `  Y )  <->  X  =  Y )
 )
 
Theoremmapdcv 34693 Covering property of the converse of the map defined by df-mapd 34658. (Contributed by NM, 14-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  C  =  (  <oLL  `
  U )   &    |-  D  =  ( (LCDual `  K ) `  W )   &    |-  E  =  (  <oLL  `
  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  ( X C Y  <->  ( M `  X ) E ( M `  Y ) ) )
 
Theoremmapdincl 34694 Closure of dual subspace intersection for the map defined by df-mapd 34658. (Contributed by NM, 12-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   &    |-  ( ph  ->  Y  e.  ran  M )   =>    |-  ( ph  ->  ( X  i^i  Y )  e. 
 ran  M )
 
Theoremmapdin 34695 Subspace intersection is preserved by the map defined by df-mapd 34658. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  ( M `  ( X  i^i  Y ) )  =  ( ( M `  X )  i^i  ( M `  Y ) ) )
 
Theoremmapdlsmcl 34696 Closure of dual subspace sum for the map defined by df-mapd 34658. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  M )   &    |-  ( ph  ->  Y  e.  ran  M )   =>    |-  ( ph  ->  ( X  .(+)  Y )  e. 
 ran  M )
 
Theoremmapdlsm 34697 Subspace sum is preserved by the map defined by df-mapd 34658. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  .+b  =  ( LSSum `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  ( M `  ( X  .(+)  Y ) )  =  ( ( M `  X )  .+b  ( M `  Y ) ) )
 
Theoremmapd0 34698 Projectivity map of the zero subspace. Part of property (f) in [Baer] p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  O  =  ( 0g `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |- 
 .0.  =  ( 0g `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   =>    |-  ( ph  ->  ( M `  { O }
 )  =  {  .0.  } )
 
TheoremmapdcnvatN 34699 Atoms are preserved by the map defined by df-mapd 34658. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  B  =  (LSAtoms `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  Q  e.  B )   =>    |-  ( ph  ->  ( `' M `  Q )  e.  A )
 
Theoremmapdat 34700 Atoms are preserved by the map defined by df-mapd 34658. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  M  =  ( (mapd `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  C  =  ( (LCDual `  K ) `  W )   &    |-  B  =  (LSAtoms `  C )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  Q  e.  A )   =>    |-  ( ph  ->  ( M `  Q )  e.  B )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19500 196 19501-19600 197 19601-19700 198 19701-19800 199 19801-19900 200 19901-20000 201 20001-20100 202