HomeHome Metamath Proof Explorer
Theorem List (p. 368 of 374)
< 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-25658)
  Hilbert Space Explorer  Hilbert Space Explorer
(25659-27183)
  Users' Mathboxes  Users' Mathboxes
(27184-37324)
 

Theorem List for Metamath Proof Explorer - 36701-36800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlcfl8a 36701* Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( (  ._|_  `  (  ._|_  `  ( L `  G ) ) )  =  ( L `  G ) 
 <-> 
 E. x  e.  V  ( L `  G )  =  (  ._|_  `  { x } ) ) )
 
Theoremlcfl8b 36702* Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  Y  =  ( 0g `  D )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `
  f ) ) )  =  ( L `
  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  ( C  \  { Y } ) )   =>    |-  ( ph  ->  E. x  e.  ( V  \  {  .0.  } ) (  ._|_  `  ( L `  G ) )  =  ( N `  { x }
 ) )
 
Theoremlcfl9a 36703 Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  (  ._|_  `  { X }
 )  C_  ( L `  G ) )   =>    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  ( L `  G ) ) )  =  ( L `
  G ) )
 
Theoremlclkrlem1 36704* The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  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 ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  G  e.  C )   =>    |-  ( ph  ->  ( X  .x.  G )  e.  C )
 
Theoremlclkrlem2a 36705 Lemma for lclkr 36731. Use lshpat 34254 to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  (  ._|_  ` 
 { X } )  =/=  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  -.  X  e.  (  ._|_  `  { B }
 ) )   =>    |-  ( ph  ->  (
 ( ( N `  { X } )  .(+)  ( N `  { Y } ) )  i^i  (  ._|_  `  { B } ) )  e.  A )
 
Theoremlclkrlem2b 36706 Lemma for lclkr 36731. (Contributed by NM, 17-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  (  ._|_  ` 
 { X } )  =/=  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  `  { B } )  \/  -.  Y  e.  (  ._|_  `  { B } ) ) )   =>    |-  ( ph  ->  ( (
 ( N `  { X } )  .(+)  ( N `
  { Y }
 ) )  i^i  (  ._|_  `  { B }
 ) )  e.  A )
 
Theoremlclkrlem2c 36707 Lemma for lclkr 36731. (Contributed by NM, 16-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  (  ._|_  ` 
 { X } )  =/=  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  `  { B } )  \/  -.  Y  e.  (  ._|_  `  { B } ) ) )   &    |-  J  =  (LSHyp `  U )   =>    |-  ( ph  ->  (
 ( (  ._|_  `  { X } )  i^i  (  ._|_  ` 
 { Y } )
 )  .(+)  ( N `  { B } ) )  e.  J )
 
Theoremlclkrlem2d 36708 Lemma for lclkr 36731. (Contributed by NM, 16-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  (  ._|_  ` 
 { X } )  =/=  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  `  { B } )  \/  -.  Y  e.  (  ._|_  `  { B } ) ) )   &    |-  I  =  ( ( DIsoH `  K ) `  W )   =>    |-  ( ph  ->  (
 ( (  ._|_  `  { X } )  i^i  (  ._|_  ` 
 { Y } )
 )  .(+)  ( N `  { B } ) )  e.  ran  I )
 
Theoremlclkrlem2e 36709 Lemma for lclkr 36731. The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X }
 ) )   &    |-  ( ph  ->  ( L `  E )  =  ( L `  G ) )   =>    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2f 36710 Lemma for lclkr 36731. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  J  =  (LSHyp `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X }
 ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( ( E 
 .+  G ) `  B )  =  Q )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  ` 
 { B } )  \/  -.  Y  e.  (  ._|_  `  { B }
 ) ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( L `  E )  =/=  ( L `  G ) )   &    |-  ( ph  ->  ( L `  ( E  .+  G ) )  e.  J )   =>    |-  ( ph  ->  (
 ( ( L `  E )  i^i  ( L `
  G ) ) 
 .(+)  ( N `  { B } ) )  C_  ( L `  ( E 
 .+  G ) ) )
 
Theoremlclkrlem2g 36711 Lemma for lclkr 36731. Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  J  =  (LSHyp `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X }
 ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( ( E 
 .+  G ) `  B )  =  Q )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  ` 
 { B } )  \/  -.  Y  e.  (  ._|_  `  { B }
 ) ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( L `  E )  =/=  ( L `  G ) )   &    |-  ( ph  ->  ( L `  ( E  .+  G ) )  e.  J )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2h 36712 Lemma for lclkr 36731. Eliminate the  ( L `  ( E 
.+  G ) )  e.  J hypothesis. (Contributed by NM, 16-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  J  =  (LSHyp `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X }
 ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( ( E 
 .+  G ) `  B )  =  Q )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  ` 
 { B } )  \/  -.  Y  e.  (  ._|_  `  { B }
 ) ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  ( L `  E )  =/=  ( L `  G ) )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `
  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2i 36713 Lemma for lclkr 36731. Eliminate the  ( L `  E )  =/=  ( L `  G ) hypothesis. (Contributed by NM, 17-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  J  =  (LSHyp `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X }
 ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( ( E 
 .+  G ) `  B )  =  Q )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  ` 
 { B } )  \/  -.  Y  e.  (  ._|_  `  { B }
 ) ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `
  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2j 36714 Lemma for lclkr 36731. Kernel closure when  Y is zero. (Contributed by NM, 18-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  J  =  (LSHyp `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X }
 ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( ( E 
 .+  G ) `  B )  =  Q )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  ` 
 { B } )  \/  -.  Y  e.  (  ._|_  `  { B }
 ) ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  =  .0.  )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2k 36715 Lemma for lclkr 36731. Kernel closure when  X is zero. (Contributed by NM, 18-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  J  =  (LSHyp `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X }
 ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( ( E 
 .+  G ) `  B )  =  Q )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  ` 
 { B } )  \/  -.  Y  e.  (  ._|_  `  { B }
 ) ) )   &    |-  ( ph  ->  X  =  .0.  )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2l 36716 Lemma for lclkr 36731. Eliminate the  X  =/=  .0.,  Y  =/=  .0. hypotheses. (Contributed by NM, 18-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  (Scalar `  U )   &    |-  Q  =  ( 0g `  S )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  N  =  (
 LSpan `  U )   &    |-  F  =  (LFnl `  U )   &    |-  J  =  (LSHyp `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  B  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X }
 ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y } ) )   &    |-  ( ph  ->  ( ( E 
 .+  G ) `  B )  =  Q )   &    |-  ( ph  ->  ( -.  X  e.  (  ._|_  ` 
 { B } )  \/  -.  Y  e.  (  ._|_  `  { B }
 ) ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2m 36717 Lemma for lclkr 36731. Construct a vector  B that makes the sum of functionals zero. Combine with  B  e.  V to shorten overall proof. (Contributed by NM, 17-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  U  e.  LVec )   &    |-  B  =  ( X  .-  ( (
 ( ( E  .+  G ) `  X )  .X.  ( I `  ( ( E  .+  G ) `  Y ) ) )  .x.  Y ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =/= 
 .0.  )   =>    |-  ( ph  ->  ( B  e.  V  /\  ( ( E  .+  G ) `  B )  =  .0.  )
 )
 
Theoremlclkrlem2n 36718 Lemma for lclkr 36731. (Contributed by NM, 12-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  U  e.  LVec )   &    |-  ( ph  ->  ( ( E  .+  G ) `  X )  =  .0.  )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =  .0.  )   =>    |-  ( ph  ->  ( N `  { X ,  Y } )  C_  ( L `  ( E  .+  G ) ) )
 
Theoremlclkrlem2o 36719 Lemma for lclkr 36731. When  B is nonzero, the vectors  X and  Y can't both belong to the hyperplane generated by  B. (Contributed by NM, 17-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  H  =  (
 LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  B  =  ( X  .-  ( (
 ( ( E  .+  G ) `  X )  .X.  ( I `  ( ( E  .+  G ) `  Y ) ) )  .x.  Y ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =/= 
 .0.  )   &    |-  ( ph  ->  B  =/=  ( 0g `  U ) )   =>    |-  ( ph  ->  ( -.  X  e.  (  ._|_  `  { B }
 )  \/  -.  Y  e.  (  ._|_  `  { B } ) ) )
 
Theoremlclkrlem2p 36720 Lemma for lclkr 36731. When  B is zero,  X and  Y must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  H  =  (
 LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  B  =  ( X  .-  ( (
 ( ( E  .+  G ) `  X )  .X.  ( I `  ( ( E  .+  G ) `  Y ) ) )  .x.  Y ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =/= 
 .0.  )   &    |-  ( ph  ->  B  =  ( 0g `  U ) )   =>    |-  ( ph  ->  ( 
 ._|_  `  { Y }
 )  C_  (  ._|_  ` 
 { X } )
 )
 
Theoremlclkrlem2q 36721 Lemma for lclkr 36731. The sum has a closed kernel when  B is nonzero. (Contributed by NM, 18-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  H  =  (
 LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X } ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y }
 ) )   &    |-  B  =  ( X  .-  ( (
 ( ( E  .+  G ) `  X )  .X.  ( I `  ( ( E  .+  G ) `  Y ) ) )  .x.  Y ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =/= 
 .0.  )   &    |-  ( ph  ->  B  =/=  ( 0g `  U ) )   =>    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2r 36722 Lemma for lclkr 36731. When  B is zero, i.e. when  X and  Y are colinear, the intersection of the kernels of  E and  G equal the kernel of  G, so the kernels of  G and the sum are comparable. (Contributed by NM, 18-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  H  =  (
 LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X } ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y }
 ) )   &    |-  B  =  ( X  .-  ( (
 ( ( E  .+  G ) `  X )  .X.  ( I `  ( ( E  .+  G ) `  Y ) ) )  .x.  Y ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =/= 
 .0.  )   &    |-  ( ph  ->  B  =  ( 0g `  U ) )   =>    |-  ( ph  ->  ( L `  G ) 
 C_  ( L `  ( E  .+  G ) ) )
 
Theoremlclkrlem2s 36723 Lemma for lclkr 36731. Thus, the sum has a closed kernel when  B is zero. (Contributed by NM, 18-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  H  =  (
 LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X } ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y }
 ) )   &    |-  B  =  ( X  .-  ( (
 ( ( E  .+  G ) `  X )  .X.  ( I `  ( ( E  .+  G ) `  Y ) ) )  .x.  Y ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =/= 
 .0.  )   &    |-  ( ph  ->  B  =  ( 0g `  U ) )   =>    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2t 36724 Lemma for lclkr 36731. We eliminate all hypotheses with  B here. (Contributed by NM, 18-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  H  =  (
 LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X } ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y }
 ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =/= 
 .0.  )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2u 36725 Lemma for lclkr 36731. lclkrlem2t 36724 with  X and  Y swapped. (Contributed by NM, 18-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  H  =  (
 LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X } ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y }
 ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  X )  =/= 
 .0.  )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2v 36726 Lemma for lclkr 36731. When the hypotheses of lclkrlem2u 36725 and lclkrlem2u 36725 are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid 36666, which requires the orthomodular law dihoml4 36575 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  H  =  (
 LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X } ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y }
 ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  X )  =  .0.  )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =  .0.  )   =>    |-  ( ph  ->  ( L `  ( E  .+  G ) )  =  V )
 
Theoremlclkrlem2w 36727 Lemma for lclkr 36731. This is the same as lclkrlem2u 36725 and lclkrlem2u 36725 with the inequality hypotheses negated. When the sum of two functionals is zero at each generating vector, the kernel is the vector space and therefore closed. (Contributed by NM, 16-Jan-2015.)
 |-  V  =  ( Base `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .X.  =  ( .r `  S )   &    |-  .0.  =  ( 0g `  S )   &    |-  I  =  ( invr `  S )   &    |-  .-  =  ( -g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  N  =  ( LSpan `  U )   &    |-  L  =  (LKer `  U )   &    |-  H  =  (
 LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X } ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y }
 ) )   &    |-  ( ph  ->  ( ( E  .+  G ) `  X )  =  .0.  )   &    |-  ( ph  ->  ( ( E  .+  G ) `  Y )  =  .0.  )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2x 36728 Lemma for lclkr 36731. Eliminate by cases the hypotheses of lclkrlem2u 36725, lclkrlem2u 36725 and lclkrlem2w 36727. (Contributed by NM, 18-Jan-2015.)
 |-  L  =  (LKer `  U )   &    |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( L `  E )  =  (  ._|_  `  { X }
 ) )   &    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { Y } ) )   =>    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  ( L `  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2y 36729 Lemma for lclkr 36731. Restate the hypotheses for  E and  G to say their kernels are closed, in order to eliminate the generating vectors  X and  Y. (Contributed by NM, 18-Jan-2015.)
 |-  L  =  (LKer `  U )   &    |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  E  e.  F )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  E ) ) )  =  ( L `
  E ) )   &    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `
  G ) ) )  =  ( L `
  G ) )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `
  ( E  .+  G ) ) ) )  =  ( L `
  ( E  .+  G ) ) )
 
Theoremlclkrlem2 36730* The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 36705 through lclkrlem2y 36729 are used for the proof. Here we express lclkrlem2y 36729 in terms of membership in the set  C of functionals with closed kernels. (Contributed by NM, 18-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  .+  =  ( +g  `  D )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  E  e.  C )   &    |-  ( ph  ->  G  e.  C )   =>    |-  ( ph  ->  ( E  .+  G )  e.  C )
 
Theoremlclkr 36731* The set of functionals with closed kernels is a subspace. Part of proof of Theorem 3.6 of [Holland95] p. 218, line 20, stating "The fM that arise this way generate a subspace F of E'". Our proof was suggested by Mario Carneiro, 5-Jan-2015. (Contributed by NM, 18-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (LDual `  U )   &    |-  S  =  ( LSubSp `  D )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  C  e.  S )
 
Theoremlcfls1lem 36732* 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 36733* 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 36734* 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 36735* 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 36736* 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 36737* 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 36731 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 36731 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 36738* 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 36826. (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 36739* 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 36740 Lemma for lcfr 36783. 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 36741 Lemma for lcfr 36783. (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 36742 Lemma for lcfr 36783. (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 36743* Lemma for lcfr 36783. (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 36744* Lemma for lcfr 36783. 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 36745* Lemma for lcfr 36783. 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 36746* Lemma for lcfr 36783. 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 36747* Lemma for lcf1o 36749 and lcfr 36783. (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 36748* Lemma for lcf1o 36749. (This part has undesirable $d's on  J and  ph that we remove in lcf1o 36749.) 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 36749* 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 36750* Lemma for lcfr 36783. (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 36751* Lemma for lcfr 36783. (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 36752* Lemma for lcfr 36783. (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 36753* Lemma for lcfr 36783. (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 36754* Lemma for lcfr 36783. (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 36755* Lemma for lcfr 36783. (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 36756* Lemma for lcfr 36783. (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 36757 Lemma for lcfr 36783. 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 36758 Lemma for lcfr 36783. (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 36759 Lemma for lcfr 36783. (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 36760 Lemma for lcfr 36783. (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 36761 Lemma for lcfr 36783. (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 36762 Lemma for lcfr 36783. (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 36763 Lemma for lcfr 36783. 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 36764* Lemma for lcfr 36783. (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 36765* Lemma for lcfr 36783. Special case of lcfrlem35 36775 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 36766* Lemma for lcfr 36783. Special case of lcfrlem36 36776 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 36767* Lemma for lcfr 36783. Special case of lcfrlem37 36777 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 36768* Lemma for lcfr 36783. 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 36769* Lemma for lcfr 36783. (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 )