HomeHome Metamath Proof Explorer
Theorem List (p. 318 of 323)
< 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-21500)
  Hilbert Space Explorer  Hilbert Space Explorer
(21501-23023)
  Users' Mathboxes  Users' Mathboxes
(23024-32227)
 

Theorem List for Metamath Proof Explorer - 31701-31800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdvh4dimat 31701* There is an atom that is outside the subspace sum of 3 others. (Contributed by NM, 25-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  P  e.  A )   &    |-  ( ph  ->  Q  e.  A )   &    |-  ( ph  ->  R  e.  A )   =>    |-  ( ph  ->  E. s  e.  A  -.  s  C_  ( ( P  .(+)  Q )  .(+)  R )
 )
 
Theoremdvh3dimatN 31702* There is an atom that is outside the subspace sum of 2 others. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  .(+)  =  (
 LSSum `  U )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  P  e.  A )   &    |-  ( ph  ->  Q  e.  A )   =>    |-  ( ph  ->  E. s  e.  A  -.  s  C_  ( P  .(+)  Q ) )
 
Theoremdvh2dimatN 31703* Given an atom, there exists another. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  P  e.  A )   =>    |-  ( ph  ->  E. s  e.  A  s  =/=  P )
 
Theoremdvh1dimat 31704* There exists an atom. (Contributed by NM, 25-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  E. s  s  e.  A )
 
Theoremdvh1dim 31705* There exists a nonzero vector. (Contributed by NM, 26-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   =>    |-  ( ph  ->  E. z  e.  V  z  =/=  .0.  )
 
Theoremdvh4dimlem 31706* Lemma for dvh4dimN 31710. (Contributed by NM, 22-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  =/=  .0.  )   &    |-  ( ph  ->  Y  =/=  .0.  )   &    |-  ( ph  ->  Z  =/=  .0.  )   =>    |-  ( ph  ->  E. z  e.  V  -.  z  e.  ( N `  { X ,  Y ,  Z }
 ) )
 
Theoremdvhdimlem 31707* Lemma for dvh2dim 31708 and dvh3dim 31709. TODO: make this obsolete and use dvh4dimlem 31706 directly? (Contributed by NM, 24-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |- 
 .0.  =  ( 0g `  U )   &    |-  ( ph  ->  X  =/=  .0.  )   &    |-  ( ph  ->  Y  =/=  .0.  )   =>    |-  ( ph  ->  E. z  e.  V  -.  z  e.  ( N `  { X ,  Y } ) )
 
Theoremdvh2dim 31708* There is a vector that is outside the span of another. (Contributed by NM, 25-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  E. z  e.  V  -.  z  e.  ( N ` 
 { X } )
 )
 
Theoremdvh3dim 31709* There is a vector that is outside the span of 2 others. (Contributed by NM, 24-Apr-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   =>    |-  ( ph  ->  E. z  e.  V  -.  z  e.  ( N `  { X ,  Y } ) )
 
Theoremdvh4dimN 31710* There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   =>    |-  ( ph  ->  E. z  e.  V  -.  z  e.  ( N `  { X ,  Y ,  Z }
 ) )
 
Theoremdvh3dim2 31711* There is a vector that is outside of 2 spans with a common vector. (Contributed by NM, 13-May-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   =>    |-  ( ph  ->  E. z  e.  V  ( -.  z  e.  ( N `  { X ,  Y } )  /\  -.  z  e.  ( N `
  { X ,  Z } ) ) )
 
Theoremdvh3dim3N 31712* There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 31711 everywhere. If this one is needed, make dvh3dim2 31711 into a lemma. (Contributed by NM, 21-May-2015.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  N  =  ( LSpan `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  E. z  e.  V  ( -.  z  e.  ( N `  { X ,  Y } )  /\  -.  z  e.  ( N ` 
 { Z ,  T } ) ) )
 
Theoremdochsnnz 31713 The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015.)
 |-  H  =  ( LHyp `  K )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  V  =  ( Base `  U )   &    |-  .0.  =  ( 0g `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  (  ._|_  `  { X }
 )  =/=  {  .0.  } )
 
Theoremdochsatshp 31714 The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014.) (Revised by Mario Carneiro, 1-Oct-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecH `  K ) `  W )   &    |-  ._|_  =  ( ( ocH `  K ) `  W )   &    |-  A  =  (LSAtoms `  U )   &    |-  Y  =  (LSHyp `  U )   &    |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )   &    |-  ( ph  ->  Q  e.  A )   =>    |-  ( ph  ->  ( 
 ._|_  `  Q )  e.  Y )
 
Theoremdochsatshpb 31715 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 31716 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 31717 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 31718 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 31719 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 31720 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 31721 The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 31677 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 31722 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 31723 Lemma for dochexmid 31731. 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 31724 Lemma for dochexmid 31731. (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 31725 Lemma for dochexmid 31731. Use atom exchange lsatexch1 29309 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 31726 Lemma for dochexmid 31731. (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 31727 Lemma for dochexmid 31731. (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 31728 Lemma for dochexmid 31731. (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 31729 Lemma for dochexmid 31731. Contradict dochexmidlem6 31728. (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 31730 Lemma for dochexmid 31731. The contradiction of dochexmidlem6 31728 and dochexmidlem7 31729 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 31731 Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 31640. 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 30240 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 31732 Lemma for dochsnkr 31735. (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 31733 Lemma for dochsnkr 31735. (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 31734 Lemma for dochsnkr 31735. (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 31735 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 31736* Kernel of the explicit functional 
G determined by a nonzero vector  X. Compare the more general lshpkr 29380. (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 31737* 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 31738* Closure of the explicit functional 
G determined by a nonzero vector  X. Compare the more general lshpkrcl 29379. (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 31739* 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 31740 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 31741* 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 29333. (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 31742* 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 29333. (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.  )
 
18.27.11  Construction of involution and inner product from a Hilbert lattice
 
SyntaxclpoN 31743 Extend class notation with all polarities of a left module or left vector space.
 class LPol
 
Definitiondf-lpolN 31744* 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 31745* 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 31746* 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 31747* 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 31748 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 31749 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 31750 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 31751 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 31752 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 31753 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 31754* 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 31755* 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 31756* 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 31757* 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 31758* 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 31759* 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 31760 Property of a functional with a closed kernel. TODO: Make lcfl5 31759 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 31761* Lemma for lcfl6 31763. A functional  G (whose kernel is closed by dochsnkr 31735) 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 31762* Lemma for lcfl7N 31764. 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 31763* Property of a functional with a closed kernel. Note that  ( L `  G )  =  V means the functional is zero by lkr0f 29357. (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 31764* 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 29357. (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 31765* 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 31766* 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 31767* 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 31768 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 31769* 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 31770 Lemma for lclkr 31796. Use lshpat 29319 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 31771 Lemma for lclkr 31796. (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 31772 Lemma for lclkr 31796. (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 31773 Lemma for lclkr 31796. (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 31774 Lemma for lclkr 31796. 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 31775 Lemma for lclkr 31796. 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 31776 Lemma for lclkr 31796. 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 31777 Lemma for lclkr 31796. 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 31778 Lemma for lclkr 31796. 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 31779 Lemma for lclkr 31796. 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 31780 Lemma for lclkr 31796. 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 31781 Lemma for lclkr 31796. 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 31782 Lemma for lclkr 31796. 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 31783 Lemma for lclkr 31796. (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 31784 Lemma for lclkr 31796. 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 31785 Lemma for lclkr 31796. 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 31786 Lemma for lclkr 31796. 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 31787 Lemma for lclkr 31796. 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 31788 Lemma for lclkr 31796. 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 31789 Lemma for lclkr 31796. 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 31790 Lemma for lclkr 31796. lclkrlem2t 31789 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 31791 Lemma for lclkr 31796. When the hypotheses of lclkrlem2u 31790 and lclkrlem2u 31790 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 31731, which requires the orthomodular law dihoml4 31640 (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 31792 Lemma for lclkr 31796. This is the same as lclkrlem2u 31790 and lclkrlem2u 31790 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 31793 Lemma for lclkr 31796. Eliminate by cases the hypotheses of lclkrlem2u 31790, lclkrlem2u 31790 and lclkrlem2w 31792. (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 )  = <