HomeHome Metamath Proof Explorer
Theorem List (p. 371 of 377)
< 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-25707)
  Hilbert Space Explorer  Hilbert Space Explorer
(25708-27232)
  Users' Mathboxes  Users' Mathboxes
(27233-37662)
 

Theorem List for Metamath Proof Explorer - 37001-37100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlcfls1lem 37001* Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.)
 |-  C  =  { f  e.  F  |  ( (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f )  /\  (  ._|_  `  ( L `  f
 ) )  C_  Q ) }   =>    |-  ( G  e.  C  <->  ( G  e.  F  /\  (  ._|_  `  (  ._|_  `  ( L `  G ) ) )  =  ( L `
  G )  /\  (  ._|_  `  ( L `  G ) )  C_  Q ) )
 
Theoremlcfls1N 37002* Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.)
 |-  C  =  { f  e.  F  |  ( (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f )  /\  (  ._|_  `  ( L `  f
 ) )  C_  Q ) }   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( G  e.  C  <->  ( (  ._|_  `  (  ._|_  `  ( L `
  G ) ) )  =  ( L `
  G )  /\  (  ._|_  `  ( L `  G ) )  C_  Q ) ) )
 
Theoremlcfls1c 37003* Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.)
 |-  C  =  { f  e.  F  |  ( (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f )  /\  (  ._|_  `  ( L `  f
 ) )  C_  Q ) }   &    |-  D  =  {
 f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }   =>    |-  ( G  e.  C  <->  ( G  e.  D  /\  (  ._|_  `  ( L `  G ) ) 
 C_  Q ) )
 
Theoremlclkrslem1 37004* The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace  Q is closed under scalar product. (Contributed by NM, 27-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .x.  =  ( .s `  D )   &    |-  C  =  { f  e.  F  |  ( ( 
 ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f )  /\  (  ._|_  `  ( L `  f ) )  C_  Q ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  Q  e.  S )   &    |-  ( ph  ->  G  e.  C )   &    |-  ( ph  ->  X  e.  B )   =>    |-  ( ph  ->  ( X  .x.  G )  e.  C )
 
Theoremlclkrslem2 37005* The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace  Q is closed under scalar product. (Contributed by NM, 28-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  R  =  (Scalar `  U )   &    |-  B  =  ( Base `  R )   &    |-  .x.  =  ( .s `  D )   &    |-  C  =  { f  e.  F  |  ( ( 
 ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f )  /\  (  ._|_  `  ( L `  f ) )  C_  Q ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  Q  e.  S )   &    |-  ( ph  ->  G  e.  C )   &    |- 
 .+  =  ( +g  `  D )   &    |-  ( ph  ->  E  e.  C )   =>    |-  ( ph  ->  ( E  .+  G )  e.  C )
 
Theoremlclkrs 37006* The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace  R is a subspace of the dual space. TODO: This proof repeats large parts of the lclkr 37000 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 37000 a special case of this? (Contributed by NM, 29-Jan-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 )  /\  (  ._|_  `  ( L `  f
 ) )  C_  R ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  R  e.  S )   =>    |-  ( ph  ->  C  e.  T )
 
Theoremlclkrs2 37007* The set of functionals with closed kernels and majorizing the orthocomplement of a given subspace  Q is a subspace of the dual space containing functionals with closed kernels. Note that  R is the value given by mapdval 37095. (Contributed by NM, 12-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 ) }   &    |-  R  =  { g  e.  F  |  ( (  ._|_  `  (  ._|_  `  ( L `  g ) ) )  =  ( L `  g )  /\  (  ._|_  `  ( L `  g
 ) )  C_  Q ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  Q  e.  S )   =>    |-  ( ph  ->  ( R  e.  T  /\  R  C_  C ) )
 
TheoremlcfrvalsnN 37008* Reconstruction from the dual space span of a singleton. (Contributed by NM, 19-Feb-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  N  =  ( LSpan `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  Q  =  U_ f  e.  R  (  ._|_  `  ( L `  f ) )   &    |-  R  =  ( N `  { G } )   =>    |-  ( ph  ->  Q  =  (  ._|_  `  ( L `  G ) ) )
 
Theoremlcfrlem1 37009 Lemma for lcfr 37052. Note that  X is z in Mario's notes. (Contributed by NM, 27-Feb-2015.)
 |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  (
 invr `  S )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .x.  =  ( .s `  D )   &    |-  .-  =  ( -g `  D )   &    |-  ( ph  ->  U  e.  LVec )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  ( G `  X )  =/=  .0.  )   &    |-  H  =  ( E  .-  (
 ( ( I `  ( G `  X ) )  .X.  ( E `  X ) )  .x.  G ) )   =>    |-  ( ph  ->  ( H `  X )  =  .0.  )
 
Theoremlcfrlem2 37010 Lemma for lcfr 37052. (Contributed by NM, 27-Feb-2015.)
 |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  (
 invr `  S )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .x.  =  ( .s `  D )   &    |-  .-  =  ( -g `  D )   &    |-  ( ph  ->  U  e.  LVec )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  ( G `  X )  =/=  .0.  )   &    |-  H  =  ( E  .-  (
 ( ( I `  ( G `  X ) )  .X.  ( E `  X ) )  .x.  G ) )   &    |-  L  =  (LKer `  U )   =>    |-  ( ph  ->  (
 ( L `  E )  i^i  ( L `  G ) )  C_  ( L `  H ) )
 
Theoremlcfrlem3 37011 Lemma for lcfr 37052. (Contributed by NM, 27-Feb-2015.)
 |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  (
 invr `  S )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .x.  =  ( .s `  D )   &    |-  .-  =  ( -g `  D )   &    |-  ( ph  ->  U  e.  LVec )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  ( G `  X )  =/=  .0.  )   &    |-  H  =  ( E  .-  (
 ( ( I `  ( G `  X ) )  .X.  ( E `  X ) )  .x.  G ) )   &    |-  L  =  (LKer `  U )   =>    |-  ( ph  ->  X  e.  ( L `  H ) )
 
Theoremlcfrlem4 37012* Lemma for lcfr 37052. (Contributed by NM, 10-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( LSubSp `  D )   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  Q )   &    |-  ( ph  ->  X  e.  E )   =>    |-  ( ph  ->  X  e.  V )
 
Theoremlcfrlem5 37013* Lemma for lcfr 37052. The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace  Q is closed under scalar product. TODO: share hypotheses with others. Use more consistent variable names here or elsewhere when possible. (Contributed by NM, 5-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  S  =  ( LSubSp `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  R  e.  S )   &    |-  Q  =  U_ f  e.  R  (  ._|_  `  ( L `  f ) )   &    |-  ( ph  ->  X  e.  Q )   &    |-  C  =  (Scalar `  U )   &    |-  B  =  ( Base `  C )   &    |-  .x.  =  ( .s `  U )   &    |-  ( ph  ->  A  e.  B )   =>    |-  ( ph  ->  ( A  .x.  X )  e.  Q )
 
Theoremlcfrlem6 37014* Lemma for lcfr 37052. Closure of vector sum with colinear vectors. TODO: Move down  N definition so top hypotheses can be shared. (Contributed by NM, 10-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( LSubSp `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  Q )   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  X  e.  E )   &    |-  ( ph  ->  Y  e.  E )   &    |-  ( ph  ->  ( N `  { X } )  =  ( N `  { Y }
 ) )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  E )
 
Theoremlcfrlem7 37015* Lemma for lcfr 37052. Closure of vector sum when one vector is zero. TODO: share hypotheses with others. (Contributed by NM, 11-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Q  =  ( LSubSp `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  Q )   &    |-  E  =  U_ g  e.  G  (  ._|_  `  ( L `  g ) )   &    |-  ( ph  ->  X  e.  E )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  ( ph  ->  Y  =  .0.  )   =>    |-  ( ph  ->  ( X  .+  Y )  e.  E )
 
Theoremlcfrlem8 37016* Lemma for lcf1o 37018 and lcfr 37052. (Contributed by NM, 21-Feb-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 ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( J `  X )  =  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { X }
 ) v  =  ( w  .+  ( k 
 .x.  X ) ) ) ) )
 
Theoremlcfrlem9 37017* Lemma for lcf1o 37018. (This part has undesirable $d's on  J and  ph that we remove in lcf1o 37018.) TODO: ugly proof; maybe have better subtheorems or abbreviate some  iota_
k expansions with  J `  z? TODO: Some redundant $d's? (Contributed by NM, 22-Feb-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 ) )   =>    |-  ( ph  ->  J : ( V  \  {  .0.  } ) -1-1-onto-> ( C 
 \  { Q }
 ) )
 
Theoremlcf1o 37018* Define a function  J that provides a bijection from nonzero vectors  V to nonzero functionals with closed kernels  C. (Contributed by NM, 22-Feb-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 ) )   =>    |-  ( ph  ->  J : ( V  \  {  .0.  } ) -1-1-onto-> ( C 
 \  { Q }
 ) )
 
Theoremlcfrlem10 37019* Lemma for lcfr 37052. (Contributed by NM, 23-Feb-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 ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( J `  X )  e.  F )
 
Theoremlcfrlem11 37020* Lemma for lcfr 37052. (Contributed by NM, 23-Feb-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 ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( L `  ( J `  X ) )  =  (  ._|_  `  { X } ) )
 
Theoremlcfrlem12N 37021* Lemma for lcfr 37052. (Contributed by NM, 23-Feb-2015.) (New usage is discouraged.)
 |-  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 ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  B  =  ( 0g `  S )   &    |-  ( ph  ->  Y  e.  (  ._|_  `  { X }
 ) )   =>    |-  ( ph  ->  (
 ( J `  X ) `  Y )  =  B )
 
Theoremlcfrlem13 37022* Lemma for lcfr 37052. (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 ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  ( J `  X )  e.  ( C  \  { Q } ) )
 
Theoremlcfrlem14 37023* Lemma for lcfr 37052. (Contributed by NM, 10-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 ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  N  =  (
 LSpan `  U )   =>    |-  ( ph  ->  ( 
 ._|_  `  ( L `  ( J `  X ) ) )  =  ( N `  { X } ) )
 
Theoremlcfrlem15 37024* Lemma for lcfr 37052. (Contributed by NM, 9-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 ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   =>    |-  ( ph  ->  X  e.  (  ._|_  `  ( L `  ( J `  X ) ) ) )
 
Theoremlcfrlem16 37025* Lemma for lcfr 37052. (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 37026 Lemma for lcfr 37052. 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 37027 Lemma for lcfr 37052. (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 37028 Lemma for lcfr 37052. (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 37029 Lemma for lcfr 37052. (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 37030 Lemma for lcfr 37052. (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 37031 Lemma for lcfr 37052. (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 37032 Lemma for lcfr 37052. 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 37033* Lemma for lcfr 37052. (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 37034* Lemma for lcfr 37052. Special case of lcfrlem35 37044 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 37035* Lemma for lcfr 37052. Special case of lcfrlem36 37045 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 37036* Lemma for lcfr 37052. Special case of lcfrlem37 37046 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 37037* Lemma for lcfr 37052. 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 37038* Lemma for lcfr 37052. (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 37039* Lemma for lcfr 37052. (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 37040* Lemma for lcfr 37052. (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 37041* Lemma for lcfr 37052. (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 37042* Lemma for lcfr 37052. (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 37043* Lemma for lcfr 37052. (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 37044* Lemma for lcfr 37052. (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 37045* Lemma for lcfr 37052. (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 37046* Lemma for lcfr 37052. (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 37047* Lemma for lcfr 37052. Combine lcfrlem27 37036 and lcfrlem37 37046. (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 37048* Lemma for lcfr 37052. 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 37049* Lemma for lcfr 37052. 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 37050* Lemma for lcfr 37052. 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 37051* Lemma for lcfr 37052. 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 37052* 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 37053 Extend class notation with vector space of functionals with closed kernels.
 class LCDual
 
Definitiondf-lcdual 37054* Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 37116. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 37092 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 37055* 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 37056* 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 37057* 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 37058 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 37059 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 37060* 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 37061 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 37062 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 37063 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 37064 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 37065 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 37066 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 37067 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 37068 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 37069 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 37070 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 37071 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 37072 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 37073 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 37074 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 37075 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 37076 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 37077 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 37078 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 37079 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 37080 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 37081 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 37082 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 37083 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 37084 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 )   &    |-  (