HomeHome Metamath Proof Explorer
Theorem List (p. 305 of 310)
< 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-30913)
 

Theorem List for Metamath Proof Explorer - 30401-30500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdochsatshpb 30401 The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  Y  =  (LSHyp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  Q  e.  S )   =>    |-  ( ph  ->  ( Q  e.  A  <->  (  ._|_  `  Q )  e.  Y )
 )
 
Theoremdochsnshp 30402 The orthocomplement of a nonzero singleton is a hyperplane. (Contributed by NM, 3-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  Y  =  (LSHyp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( 
 ._|_  `  { X }
 )  e.  Y )
 
Theoremdochshpsat 30403 A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  Y  =  (LSHyp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  Y )   =>    |-  ( ph  ->  ( (  ._|_  `  (  ._|_  `  X ) )  =  X  <->  (  ._|_  `  X )  e.  A )
 )
 
Theoremdochkrsat 30404 The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  (
 (  ._|_  `  ( L `  G ) )  =/=  {  .0.  }  <->  (  ._|_  `  ( L `  G ) )  e.  A ) )
 
Theoremdochkrsat2 30405 The orthocomplement of a kernel is an atom iff the double orthocomplement is not the vector space. (Contributed by NM, 1-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( (  ._|_  `  (  ._|_  `  ( L `  G ) ) )  =/= 
 V 
 <->  (  ._|_  `  ( L `
  G ) )  e.  A ) )
 
Theoremdochsat0 30406 The orthocomplement of a kernel is either an atom or zero. (Contributed by NM, 29-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .0.  =  ( 0g `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  (
 (  ._|_  `  ( L `  G ) )  e.  A  \/  (  ._|_  `  ( L `  G ) )  =  {  .0.  } ) )
 
Theoremdochkrsm 30407 The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 30363 can be used to convert sum to join.) (Contributed by NM, 29-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  I  =  ( ( DIsoH `  K ) `  W )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ran  I )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( X  .(+)  (  ._|_  `  ( L `  G ) ) )  e.  ran  I
 )
 
Theoremdochexmidat 30408 Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .(+)  =  ( LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( (  ._|_  `  { X } )  .(+)  ( N `
  { X }
 ) )  =  V )
 
Theoremdochexmidlem1 30409 Lemma for dochexmid 30417. Holland's proof implicitly requires  q  =/=  r, which we prove here. (Contributed by NM, 14-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  p  e.  A )   &    |-  ( ph  ->  q  e.  A )   &    |-  ( ph  ->  r  e.  A )   &    |-  ( ph  ->  q  C_  (  ._|_  `  X ) )   &    |-  ( ph  ->  r  C_  X )   =>    |-  ( ph  ->  q  =/=  r )
 
Theoremdochexmidlem2 30410 Lemma for dochexmid 30417. (Contributed by NM, 14-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  p  e.  A )   &    |-  ( ph  ->  q  e.  A )   &    |-  ( ph  ->  r  e.  A )   &    |-  ( ph  ->  q  C_  (  ._|_  `  X ) )   &    |-  ( ph  ->  r  C_  X )   &    |-  ( ph  ->  p  C_  ( r  .(+)  q ) )   =>    |-  ( ph  ->  p  C_  ( X  .(+)  (  ._|_  `  X ) ) )
 
Theoremdochexmidlem3 30411 Lemma for dochexmid 30417. Use atom exchange lsatexch1 27995 to swap  p and  q. (Contributed by NM, 14-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  p  e.  A )   &    |-  ( ph  ->  q  e.  A )   &    |-  ( ph  ->  r  e.  A )   &    |-  ( ph  ->  q  C_  (  ._|_  `  X ) )   &    |-  ( ph  ->  r  C_  X )   &    |-  ( ph  ->  q  C_  ( r  .(+)  p ) )   =>    |-  ( ph  ->  p  C_  ( X  .(+)  (  ._|_  `  X ) ) )
 
Theoremdochexmidlem4 30412 Lemma for dochexmid 30417. (Contributed by NM, 15-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  p  e.  A )   &    |-  ( ph  ->  q  e.  A )   &    |-  .0.  =  ( 0g `  U )   &    |-  M  =  ( X  .(+) 
 p )   &    |-  ( ph  ->  X  =/=  {  .0.  }
 )   &    |-  ( ph  ->  q  C_  ( (  ._|_  `  X )  i^i  M ) )   =>    |-  ( ph  ->  p  C_  ( X  .(+)  (  ._|_  `  X ) ) )
 
Theoremdochexmidlem5 30413 Lemma for dochexmid 30417. (Contributed by NM, 15-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  p  e.  A )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  M  =  ( X  .(+)  p )   &    |-  ( ph  ->  X  =/=  {  .0.  } )   &    |-  ( ph  ->  -.  p  C_  ( X  .(+) 
 (  ._|_  `  X )
 ) )   =>    |-  ( ph  ->  (
 (  ._|_  `  X )  i^i  M )  =  {  .0.  } )
 
Theoremdochexmidlem6 30414 Lemma for dochexmid 30417. (Contributed by NM, 15-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  p  e.  A )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  M  =  ( X  .(+)  p )   &    |-  ( ph  ->  X  =/=  {  .0.  } )   &    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  X ) )  =  X )   &    |-  ( ph  ->  -.  p  C_  ( X  .(+)  (  ._|_  `  X ) ) )   =>    |-  ( ph  ->  M  =  X )
 
Theoremdochexmidlem7 30415 Lemma for dochexmid 30417. Contradict dochexmidlem6 30414. (Contributed by NM, 15-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  p  e.  A )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  M  =  ( X  .(+)  p )   &    |-  ( ph  ->  X  =/=  {  .0.  } )   &    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  X ) )  =  X )   &    |-  ( ph  ->  -.  p  C_  ( X  .(+)  (  ._|_  `  X ) ) )   =>    |-  ( ph  ->  M  =/=  X )
 
Theoremdochexmidlem8 30416 Lemma for dochexmid 30417. The contradiction of dochexmidlem6 30414 and dochexmidlem7 30415 shows that there can be no atom  p that is not in  X  +  ( 
._|_  `  X ), which is therefore the whole atom space. (Contributed by NM, 15-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( LSubSp `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  =/=  {  .0.  } )   &    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  X ) )  =  X )   =>    |-  ( ph  ->  ( X  .(+)  (  ._|_  `  X ) )  =  V )
 
Theoremdochexmid 30417 Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 30326. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables  X,  M,  p,  q,  r in place of Hollands' l, m, P, Q, L respectively. (pexmidALTN 28926 analog.) (Contributed by NM, 15-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  S  =  ( LSubSp `  U )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  S )   &    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  X ) )  =  X )   =>    |-  ( ph  ->  ( X  .(+)  (  ._|_  `  X ) )  =  V )
 
Theoremdochsnkrlem1 30418 Lemma for dochsnkr 30421. (Contributed by NM, 1-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  ( (  ._|_  `  ( L `  G ) )  \  {  .0.  } ) )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  G ) ) )  =/=  V )
 
Theoremdochsnkrlem2 30419 Lemma for dochsnkr 30421. (Contributed by NM, 1-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  ( (  ._|_  `  ( L `  G ) )  \  {  .0.  } ) )   &    |-  A  =  (LSAtoms `  U )   =>    |-  ( ph  ->  (  ._|_  `  ( L `  G ) )  e.  A )
 
Theoremdochsnkrlem3 30420 Lemma for dochsnkr 30421. (Contributed by NM, 2-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  ( (  ._|_  `  ( L `  G ) )  \  {  .0.  } ) )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  G ) ) )  =  ( L `
  G ) )
 
Theoremdochsnkr 30421 A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems) (Contributed by NM, 2-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  ( (  ._|_  `  ( L `  G ) )  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( L `  G )  =  (  ._|_  `  { X } ) )
 
Theoremdochsnkr2 30422* Kernel of the explicit functional 
G determined by a nonzero vector  X. Compare the more general lshpkr 28066. (Contributed by NM, 27-Oct-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |- 
 .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (Scalar `  U )   &    |-  R  =  ( Base `  D )   &    |-  G  =  ( 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 `  G )  =  (  ._|_  `  { X } ) )
 
Theoremdochsnkr2cl 30423* The  X determining functional  G belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |- 
 .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  L  =  (LKer `  U )   &    |-  D  =  (Scalar `  U )   &    |-  R  =  ( Base `  D )   &    |-  G  =  ( 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 `  G ) )  \  {  .0.  } ) )
 
Theoremdochflcl 30424* Closure of the explicit functional 
G determined by a nonzero vector  X. Compare the more general lshpkrcl 28065. (Contributed by NM, 27-Oct-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |- 
 .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  F  =  (LFnl `  U )   &    |-  D  =  (Scalar `  U )   &    |-  R  =  ( Base `  D )   &    |-  G  =  ( 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  ->  G  e.  F )
 
Theoremdochfl1 30425* The value of the explicit functional  G is 1 at the  X that determines it. (Contributed by NM, 27-Oct-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  D  =  (Scalar `  U )   &    |-  R  =  (
 Base `  D )   &    |-  .1.  =  ( 1r `  D )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  }
 ) )   &    |-  G  =  ( v  e.  V  |->  (
 iota_ k  e.  R E. w  e.  (  ._|_  `  { X }
 ) v  =  ( w  .+  ( k 
 .x.  X ) ) ) )   =>    |-  ( ph  ->  ( G `  X )  =  .1.  )
 
Theoremdochfln0 30426 The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  N  =  ( 0g `  R )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  ( (  ._|_  `  ( L `  G ) )  \  {  .0.  } ) )   =>    |-  ( ph  ->  ( G `  X )  =/= 
 N )
 
Theoremdochkr1 30427* A non-zero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 28019. (Contributed by NM, 2-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  .0.  =  ( 0g `  U )   &    |- 
 .1.  =  ( 1r `  R )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  ( L `  G ) ) )  =/=  V )   =>    |-  ( ph  ->  E. x  e.  ( (  ._|_  `  ( L `  G ) ) 
 \  {  .0.  }
 ) ( G `  x )  =  .1.  )
 
Theoremdochkr1OLDN 30428* A non-zero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 28019. (Contributed by NM, 2-Jan-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  R  =  (Scalar `  U )   &    |-  .0.  =  ( 0g `  R )   &    |- 
 .1.  =  ( 1r `  R )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  ( 
 ._|_  `  (  ._|_  `  ( L `  G ) ) )  =/=  V )   =>    |-  ( ph  ->  E. x  e.  (  ._|_  `  ( L `  G ) ) ( G `  x )  =  .1.  )
 
16.22.15  Construction of involution and inner product from a Hilbert lattice
 
SyntaxclpoN 30429 Extend class notation with all polarities of a left module or left vector space.
 class LPol
 
Definitiondf-lpolN 30430* Define the set of all polarities of a left module or left vector space. A polarity is a kind of complementation operation on a subspace. The double polarity of a subspace is a closure operation. Based on Definition 3.2 of [Holland95] p. 214 for projective geometry polarities. For convenience, we open up the domain to include all vector subsets and not just subspaces, but any more restricted polarity can be converted to this one by taking the span of its argument. (Contributed by NM, 24-Nov-2014.)
 |- LPol  =  ( w  e.  _V  |->  { o  e.  ( (
 LSubSp `  w )  ^m  ~P ( Base `  w )
 )  |  ( ( o `  ( Base `  w ) )  =  { ( 0g `  w ) }  /\  A. x A. y ( ( x  C_  ( Base `  w )  /\  y  C_  ( Base `  w )  /\  x  C_  y
 )  ->  ( o `  y )  C_  (
 o `  x )
 )  /\  A. x  e.  (LSAtoms `  w )
 ( ( o `  x )  e.  (LSHyp `  w )  /\  (
 o `  ( o `  x ) )  =  x ) ) }
 )
 
TheoremlpolsetN 30431* The set of polarities of a left module or left vector space. (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  S  =  ( LSubSp `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  A  =  (LSAtoms `  W )   &    |-  H  =  (LSHyp `  W )   &    |-  P  =  (LPol `  W )   =>    |-  ( W  e.  X  ->  P  =  { o  e.  ( S  ^m  ~P V )  |  (
 ( o `  V )  =  {  .0.  } 
 /\  A. x A. y
 ( ( x  C_  V  /\  y  C_  V  /\  x  C_  y ) 
 ->  ( o `  y
 )  C_  ( o `  x ) )  /\  A. x  e.  A  ( ( o `  x )  e.  H  /\  ( o `  (
 o `  x )
 )  =  x ) ) } )
 
TheoremislpolN 30432* The predicate "is a polarity". (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  S  =  ( LSubSp `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  A  =  (LSAtoms `  W )   &    |-  H  =  (LSHyp `  W )   &    |-  P  =  (LPol `  W )   =>    |-  ( W  e.  X  ->  (  ._|_  e.  P  <->  ( 
 ._|_  : ~P V --> S  /\  ( (  ._|_  `  V )  =  {  .0.  } 
 /\  A. x A. y
 ( ( x  C_  V  /\  y  C_  V  /\  x  C_  y ) 
 ->  (  ._|_  `  y
 )  C_  (  ._|_  `  x ) )  /\  A. x  e.  A  ( (  ._|_  `  x )  e.  H  /\  (  ._|_  `  (  ._|_  `  x ) )  =  x ) ) ) ) )
 
TheoremislpoldN 30433* Properties that determine a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  S  =  ( LSubSp `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  A  =  (LSAtoms `  W )   &    |-  H  =  (LSHyp `  W )   &    |-  P  =  (LPol `  W )   &    |-  ( ph  ->  W  e.  X )   &    |-  ( ph  ->  ._|_  : ~P V --> S )   &    |-  ( ph  ->  ( 
 ._|_  `  V )  =  {  .0.  } )   &    |-  (
 ( ph  /\  ( x 
 C_  V  /\  y  C_  V  /\  x  C_  y ) )  ->  (  ._|_  `  y )  C_  (  ._|_  `  x ) )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  (  ._|_  `  x )  e.  H )   &    |-  (
 ( ph  /\  x  e.  A )  ->  (  ._|_  `  (  ._|_  `  x ) )  =  x )   =>    |-  ( ph  ->  ._|_  e.  P )
 
TheoremlpolfN 30434 Functionality of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  S  =  ( LSubSp `  W )   &    |-  P  =  (LPol `  W )   &    |-  ( ph  ->  W  e.  X )   &    |-  ( ph  ->  ._|_  e.  P )   =>    |-  ( ph  ->  ._|_  : ~P V
 --> S )
 
TheoremlpolvN 30435 The polarity of the whole space is the zero subspace. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  .0.  =  ( 0g `  W )   &    |-  P  =  (LPol `  W )   &    |-  ( ph  ->  W  e.  X )   &    |-  ( ph  ->  ._|_  e.  P )   =>    |-  ( ph  ->  (  ._|_  `  V )  =  {  .0.  } )
 
TheoremlpolconN 30436 Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
 |-  V  =  ( Base `  W )   &    |-  P  =  (LPol `  W )   &    |-  ( ph  ->  W  e.  X )   &    |-  ( ph  ->  ._|_  e.  P )   &    |-  ( ph  ->  X  C_  V )   &    |-  ( ph  ->  Y 
 C_  V )   &    |-  ( ph  ->  X  C_  Y )   =>    |-  ( ph  ->  (  ._|_  `  Y )  C_  (  ._|_  `  X )
 )
 
TheoremlpolsatN 30437 The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
 |-  A  =  (LSAtoms `  W )   &    |-  H  =  (LSHyp `  W )   &    |-  P  =  (LPol `  W )   &    |-  ( ph  ->  W  e.  X )   &    |-  ( ph  ->  ._|_  e.  P )   &    |-  ( ph  ->  Q  e.  A )   =>    |-  ( ph  ->  (  ._|_  `  Q )  e.  H )
 
TheoremlpolpolsatN 30438 Property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
 |-  A  =  (LSAtoms `  W )   &    |-  P  =  (LPol `  W )   &    |-  ( ph  ->  W  e.  X )   &    |-  ( ph  ->  ._|_  e.  P )   &    |-  ( ph  ->  Q  e.  A )   =>    |-  ( ph  ->  (  ._|_  `  (  ._|_  `  Q ) )  =  Q )
 
TheoremdochpolN 30439 The subspace orthocomplement for the  DVecH vector space is a polarity. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  P  =  (LPol `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  ._|_  e.  P )
 
Theoremlcfl1lem 30440* Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.)
 |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   =>    |-  ( G  e.  C 
 <->  ( G  e.  F  /\  (  ._|_  `  (  ._|_  `  ( L `  G ) ) )  =  ( L `  G ) ) )
 
Theoremlcfl1 30441* Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.)
 |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( G  e.  C  <->  (  ._|_  `  (  ._|_  `  ( L `  G ) ) )  =  ( L `  G ) ) )
 
Theoremlcfl2 30442* Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( G  e.  C  <->  ( (  ._|_  `  (  ._|_  `  ( L `
  G ) ) )  =/=  V  \/  ( L `  G )  =  V ) ) )
 
Theoremlcfl3 30443* Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( G  e.  C  <->  ( (  ._|_  `  ( L `  G ) )  e.  A  \/  ( L `  G )  =  V )
 ) )
 
Theoremlcfl4N 30444* Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  Y  =  (LSHyp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( G  e.  C  <->  ( (  ._|_  `  (  ._|_  `  ( L `
  G ) ) )  e.  Y  \/  ( L `  G )  =  V ) ) )
 
Theoremlcfl5 30445* Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  I  =  ( ( DIsoH `  K ) `  W )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( G  e.  C  <->  ( L `  G )  e.  ran  I ) )
 
Theoremlcfl5a 30446 Property of a functional with a closed kernel. TODO: Make lcfl5 30445 etc. obsolete and rewrite w/out 
C hypothesis? (Contributed by NM, 29-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  I  =  ( ( DIsoH `  K ) `  W )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( (  ._|_  `  (  ._|_  `  ( L `  G ) ) )  =  ( L `  G ) 
 <->  ( L `  G )  e.  ran  I ) )
 
Theoremlcfl6lem 30447* Lemma for lcfl6 30449. A functional  G (whose kernel is closed by dochsnkr 30421) is comletely determined by a vector  X in the orthocomplement in its kernel at which the functional value is 1. Note that the  \  {  .0.  } in the  X hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .+  =  ( +g  `  U )   &    |-  .x.  =  ( .s `  U )   &    |-  S  =  (Scalar `  U )   &    |- 
 .1.  =  ( 1r `  S )   &    |-  R  =  (
 Base `  S )   &    |-  .0.  =  ( 0g `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  ( ph  ->  G  e.  F )   &    |-  ( ph  ->  X  e.  ( (  ._|_  `  ( L `  G ) )  \  {  .0.  } ) )   &    |-  ( ph  ->  ( G `  X )  =  .1.  )   =>    |-  ( ph  ->  G  =  ( v  e.  V  |->  ( iota_ k  e.  R E. w  e.  (  ._|_  `  { X } ) v  =  ( w  .+  (
 k  .x.  X )
 ) ) ) )
 
Theoremlcfl7lem 30448* Lemma for lcfl7N 30450. If two functionals  G and  J are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-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 )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H )
 )   &    |-  G  =  ( v  e.  V  |->  ( iota_ k  e.  R E. w  e.  (  ._|_  `  { X } ) v  =  ( w  .+  (
 k  .x.  X )
 ) ) )   &    |-  J  =  ( v  e.  V  |->  ( iota_ k  e.  R E. w  e.  (  ._|_  `  { Y }
 ) v  =  ( w  .+  ( k 
 .x.  Y ) ) ) )   &    |-  ( ph  ->  X  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  Y  e.  ( V  \  {  .0.  } ) )   &    |-  ( ph  ->  G  =  J )   =>    |-  ( ph  ->  X  =  Y )
 
Theoremlcfl6 30449* Property of a functional with a closed kernel. Note that  ( L `  G )  =  V means the functional is zero by lkr0f 28043. (Contributed by NM, 3-Jan-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 )   &    |-  C  =  {
 f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( G  e.  C  <->  ( ( L `
  G )  =  V  \/  E. x  e.  ( V  \  {  .0.  } ) G  =  ( v  e.  V  |->  ( iota_ k  e.  R E. w  e.  (  ._|_  `  { x }
 ) v  =  ( w  .+  ( k 
 .x.  x ) ) ) ) ) ) )
 
Theoremlcfl7N 30450* Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that  ( L `  G )  =  V means the functional is zero by lkr0f 28043. (Contributed by NM, 4-Jan-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 )   &    |-  C  =  {
 f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `
  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( G  e.  C  <->  ( ( L `
  G )  =  V  \/  E! x  e.  ( V  \  {  .0.  } ) G  =  ( v  e.  V  |->  ( iota_ k  e.  R E. w  e.  (  ._|_  `  { x }
 ) v  =  ( w  .+  ( k 
 .x.  x ) ) ) ) ) ) )
 
Theoremlcfl8 30451* 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 )   &    |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  G  e.  F )   =>    |-  ( ph  ->  ( G  e.  C  <->  E. x  e.  V  ( L `  G )  =  (  ._|_  `  { x } ) ) )
 
Theoremlcfl8a 30452* 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 30453* 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 30454 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 30455* 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 30456 Lemma for lclkr 30482. Use lshpat 28005 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 30457 Lemma for lclkr 30482. (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 30458 Lemma for lclkr 30482. (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 30459 Lemma for lclkr 30482. (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 30460 Lemma for lclkr 30482. 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 30461 Lemma for lclkr 30482. 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 30462 Lemma for lclkr 30482. 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 30463 Lemma for lclkr 30482. 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 30464 Lemma for lclkr 30482. 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 30465 Lemma for lclkr 30482. 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 30466 Lemma for lclkr 30482. 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 30467 Lemma for lclkr 30482. 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 30468 Lemma for lclkr 30482. 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 30469 Lemma for lclkr 30482. (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 30470 Lemma for lclkr 30482. 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 30471 Lemma for lclkr 30482. 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 30472 Lemma for lclkr 30482. 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 30473 Lemma for lclkr 30482. 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 30474 Lemma for lclkr 30482. 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 30475 Lemma for lclkr 30482. 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 30476 Lemma for lclkr 30482. lclkrlem2t 30475 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 30477 Lemma for lclkr 30482. When the hypotheses of lclkrlem2u 30476 and lclkrlem2u 30476 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 30417, which requires the orthomodular law dihoml4 30326 (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 30478 Lemma for lclkr 30482. This is the same as lclkrlem2u 30476 and lclkrlem2u 30476 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 30479 Lemma for lclkr 30482. Eliminate by cases the hypotheses of lclkrlem2u 30476, lclkrlem2u 30476 and lclkrlem2w 30478. (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 30480 Lemma for lclkr 30482. 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 30481* The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 30456 through lclkrlem2y 30480 are used for the proof. Here we express lclkrlem2y 30480 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 30482* 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 30483* 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 30484* 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 30485* 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 30486* 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 30487* 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 30488* 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 30482 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 30482 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 30489* 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 30577. (Contributed by NM, 12-Mar-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  S  =  ( LSubSp `  U )   &    |-  F  =  (LFnl `  U )   &    |-  L  =  (LKer `