HomeHome Metamath Proof Explorer
Theorem List (p. 351 of 402)
< 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-26569)
  Hilbert Space Explorer  Hilbert Space Explorer
(26570-28092)
  Users' Mathboxes  Users' Mathboxes
(28093-40161)
 

Theorem List for Metamath Proof Explorer - 35001-35100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdochexmidlem5 35001 Lemma for dochexmid 35005. (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 35002 Lemma for dochexmid 35005. (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 35003 Lemma for dochexmid 35005. Contradict dochexmidlem6 35002. (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 35004 Lemma for dochexmid 35005. The contradiction of dochexmidlem6 35002 and dochexmidlem7 35003 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 35005 Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 34914. 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 33512 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 35006 Lemma for dochsnkr 35009. (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 35007 Lemma for dochsnkr 35009. (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 35008 Lemma for dochsnkr 35009. (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 35009 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 35010* Kernel of the explicit functional 
G determined by a nonzero vector  X. Compare the more general lshpkr 32652. (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 35011* 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 35012* Closure of the explicit functional 
G determined by a nonzero vector  X. Compare the more general lshpkrcl 32651. (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 35013* 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 35014 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 35015* 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 32605. (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 35016* 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 32605. (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.  )
 
21.21.14  Construction of involution and inner product from a Hilbert lattice
 
SyntaxclpoN 35017 Extend class notation with all polarities of a left module or left vector space.
 class LPol
 
Definitiondf-lpolN 35018* 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 35019* 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 35020* 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 35021* 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 35022 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 35023 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 35024 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 35025 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 35026 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 35027 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 35028* 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 35029* 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 35030* 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 35031* 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 35032* 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 35033* 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 35034 Property of a functional with a closed kernel. TODO: Make lcfl5 35033 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 35035* Lemma for lcfl6 35037. A functional  G (whose kernel is closed by dochsnkr 35009) 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 35036* Lemma for lcfl7N 35038. 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 35037* Property of a functional with a closed kernel. Note that  ( L `  G )  =  V means the functional is zero by lkr0f 32629. (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 35038* 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 32629. (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 35039* 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 35040* 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 35041* 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 35042 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 35043* 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 35044 Lemma for lclkr 35070. Use lshpat 32591 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 35045 Lemma for lclkr 35070. (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 35046 Lemma for lclkr 35070. (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 35047 Lemma for lclkr 35070. (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 35048 Lemma for lclkr 35070. 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 35049 Lemma for lclkr 35070. 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 35050 Lemma for lclkr 35070. 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 35051 Lemma for lclkr 35070. 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 35052 Lemma for lclkr 35070. 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 35053 Lemma for lclkr 35070. 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 35054 Lemma for lclkr 35070. 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 35055 Lemma for lclkr 35070. 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 35056 Lemma for lclkr 35070. 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 35057 Lemma for lclkr 35070. (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 35058 Lemma for lclkr 35070. 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 35059 Lemma for lclkr 35070. 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 35060 Lemma for lclkr 35070. 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 35061 Lemma for lclkr 35070. 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 35062 Lemma for lclkr 35070. 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 35063 Lemma for lclkr 35070. 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 35064 Lemma for lclkr 35070. lclkrlem2t 35063 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 35065 Lemma for lclkr 35070. When the hypotheses of lclkrlem2u 35064 and lclkrlem2u 35064 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 35005, which requires the orthomodular law dihoml4 34914 (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 35066 Lemma for lclkr 35070. This is the same as lclkrlem2u 35064 and lclkrlem2u 35064 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 35067 Lemma for lclkr 35070. Eliminate by cases the hypotheses of lclkrlem2u 35064, lclkrlem2u 35064 and lclkrlem2w 35066. (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 35068 Lemma for lclkr 35070. 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 35069* The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 35044 through lclkrlem2y 35068 are used for the proof. Here we express lclkrlem2y 35068 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 35070* 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 35071* 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 35072* 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 35073* 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 35074* 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 35075* 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 35076* 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 35070 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 35070 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 35077* 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 35165. (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 35078* 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 35079 Lemma for lcfr 35122. 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 35080 Lemma for lcfr 35122. (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 35081 Lemma for lcfr 35122. (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 35082* Lemma for lcfr 35122. (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 35083* Lemma for lcfr 35122. 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 35084* Lemma for lcfr 35122. 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 35085* Lemma for lcfr 35122. 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 35086* Lemma for lcf1o 35088 and lcfr 35122. (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 35087* Lemma for lcf1o 35088. (This part has undesirable $d's on  J and  ph that we remove in lcf1o 35088.) 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 )   &    |-  ._|_