HomeHome Metamath Proof Explorer
Theorem List (p. 305 of 309)
< 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-21328)
  Hilbert Space Explorer  Hilbert Space Explorer
(21329-22851)
  Users' Mathboxes  Users' Mathboxes
(22852-30843)
 

Theorem List for Metamath Proof Explorer - 30401-30500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlclkrlem2p 30401 Lemma for lclkr 30412. 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 30402 Lemma for lclkr 30412. 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 30403 Lemma for lclkr 30412. 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 30404 Lemma for lclkr 30412. 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 30405 Lemma for lclkr 30412. 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 30406 Lemma for lclkr 30412. lclkrlem2t 30405 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 30407 Lemma for lclkr 30412. When the hypotheses of lclkrlem2u 30406 and lclkrlem2u 30406 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 30347, which requires the orthomodular law dihoml4 30256 (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 30408 Lemma for lclkr 30412. This is the same as lclkrlem2u 30406 and lclkrlem2u 30406 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 30409 Lemma for lclkr 30412. Eliminate by cases the hypotheses of lclkrlem2u 30406, lclkrlem2u 30406 and lclkrlem2w 30408. (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 30410 Lemma for lclkr 30412. 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 30411* The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 30386 through lclkrlem2y 30410 are used for the proof. Here we express lclkrlem2y 30410 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 30412* 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 30413* 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 30414* 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 30415* 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 30416* 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 30417* 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 30418* 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 30412 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 30412 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 30419* 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 30507. (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 30420* 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 30421 Lemma for lcfr 30464. 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 30422 Lemma for lcfr 30464. (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 30423 Lemma for lcfr 30464. (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 30424* Lemma for lcfr 30464. (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 30425* Lemma for lcfr 30464. 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 30426* Lemma for lcfr 30464. 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 30427* Lemma for lcfr 30464. 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 30428* Lemma for lcf1o 30430 and lcfr 30464. (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 30429* Lemma for lcf1o 30430. (This part has undesirable $d's on  J and  ph that we remove in lcf1o 30430.) 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 30430* 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 30431* Lemma for lcfr 30464. (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 30432* Lemma for lcfr 30464. (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 30433* Lemma for lcfr 30464. (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 30434* Lemma for lcfr 30464. (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 30435* Lemma for lcfr 30464. (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 30436* Lemma for lcfr 30464. (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 30437* Lemma for lcfr 30464. (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 30438 Lemma for lcfr 30464. 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 30439 Lemma for lcfr 30464. (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 30440 Lemma for lcfr 30464. (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 30441 Lemma for lcfr 30464. (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 30442 Lemma for lcfr 30464. (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 30443 Lemma for lcfr 30464. (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 30444 Lemma for lcfr 30464. 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 30445* Lemma for lcfr 30464. (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 30446* Lemma for lcfr 30464. Special case of lcfrlem35 30456 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 30447* Lemma for lcfr 30464. Special case of lcfrlem36 30457 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 30448* Lemma for lcfr 30464. Special case of lcfrlem37 30458 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 30449* Lemma for lcfr 30464. 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 30450* Lemma for lcfr 30464. (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 30451* Lemma for lcfr 30464. (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 30452* Lemma for lcfr 30464. (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 30453* Lemma for lcfr 30464. (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 30454* Lemma for lcfr 30464. (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 30455* Lemma for lcfr 30464. (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 30456* Lemma for lcfr 30464. (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 30457* Lemma for lcfr 30464. (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 30458* Lemma for lcfr 30464. (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 30459* Lemma for lcfr 30464. Combine lcfrlem27 30448 and lcfrlem37 30458. (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 30460* Lemma for lcfr 30464. 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 30461* Lemma for lcfr 30464. 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 30462* Lemma for lcfr 30464. 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 30463* Lemma for lcfr 30464. 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 30464* 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 30465 Extend class notation with vector space of functionals with closed kernels.
 class LCDual
 
Definitiondf-lcdual 30466* Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 30528. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 30504 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 )