:: Spaces of Pencils, {G}rassmann Spaces, and Generalized {V}eronese
:: Spaces
::  by Adam Naumowicz
::
:: Received November 8, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, ARYTM_3, XXREAL_0, ARYTM_1, FINSET_1, CARD_1,
      SUBSET_1, TARSKI, XBOOLE_0, VECTSP_1, RLSUB_1, STRUCT_0, SUPINF_2,
      RLSUB_2, RLVECT_5, SETFAM_1, ZFMISC_1, RLVECT_3, RELAT_1, PRE_TOPC,
      PENCIL_1, PENCIL_4;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, CARD_1, NUMBERS, XCMPLX_0,
      XXREAL_0, ORDINAL1, NAT_1, NAT_D, SETFAM_1, DOMAIN_1, STRUCT_0, FINSET_1,
      PRE_TOPC, PENCIL_1, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_7,
      MATRLIN, VECTSP_9;
 constructors REALSET1, VECTSP_5, VECTSP_7, VECTSP_9, PENCIL_1, NAT_D;
 registrations SUBSET_1, FINSET_1, XXREAL_0, XREAL_0, STRUCT_0, MATRLIN,
      VECTSP_9, PENCIL_1, ORDINAL1, CARD_1;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
 definitions TARSKI, XBOOLE_0, STRUCT_0, PENCIL_1, VECTSP_4, RLVECT_1;
 theorems XBOOLE_0, ZFMISC_1, NAT_1, TARSKI, PENCIL_1, CARD_1, XBOOLE_1,
      CARD_2, STRUCT_0, SUBSET_1, VECTSP_5, VECTSP_9, VECTSP_4, RLVECT_1,
      VECTSP_7, VECTSP10, VECTSP_1, EULER_1, XREAL_1, XXREAL_0, ORDINAL1,
      NAT_D, FINSEQ_4;
 schemes XBOOLE_0, SUBSET_1;

begin :: Spaces of pencils

theorem Th1:
  for k,n being Nat st k < n & 3 <= n holds k+1 < n or 2 <= k
proof
  let k,n be Nat such that
A1: k < n and
A2: 3 <= n;
  assume
A3: k+1 >= n;
  k+1 <= n by A1,NAT_1:13;
  then 3 <= k+1 by A2,A3,XXREAL_0:1;
  then 3-1 <= k+1-1 by XREAL_1:9;
  hence thesis;
end;

Lm1:
  for X being finite set for n being Nat st n <= card X ex Y being
  Subset of X st card Y = n by FINSEQ_4:72;

theorem Th2:
  for F being Field for V being VectSp of F for W being Subspace of
  V holds W is Subspace of (Omega).V
proof
  let F be Field;
  let V be VectSp of F;
  let W be Subspace of V;
  thus the carrier of W c= the carrier of (Omega).V by VECTSP_4:def 2;
  thus 0.W = 0.V by VECTSP_4:def 2
    .= 0.(Omega).V;
  thus thesis by VECTSP_4:def 2;
end;

theorem Th3:
  for F being Field for V being VectSp of F for W being Subspace of
  (Omega).V holds W is Subspace of V
proof
  let F be Field;
  let V be VectSp of F;
  let W be Subspace of (Omega).V;
  thus the carrier of W c= the carrier of V by VECTSP_4:def 2;
  thus 0.W = 0.(Omega).V by VECTSP_4:def 2
    .= 0.V;
  thus thesis by VECTSP_4:def 2;
end;

theorem Th4:
  for F being Field for V being VectSp of F for W being Subspace of
  V holds (Omega).W is Subspace of V
proof
  let F be Field;
  let V be VectSp of F;
  let W be Subspace of V;
  thus the carrier of (Omega).W c= the carrier of V by VECTSP_4:def 2;
  thus 0.(Omega).W = 0.W .= 0.V by VECTSP_4:def 2;
  thus thesis by VECTSP_4:def 2;
end;

theorem Th5:
  for F being Field for V,W being VectSp of F holds (Omega).W is
  Subspace of V implies W is Subspace of V
proof
  let F be Field;
  let V,W be VectSp of F;
  assume
A1: (Omega).W is Subspace of V;
  hence the carrier of W c= the carrier of V by VECTSP_4:def 2;
  thus 0.W = 0.(Omega).W .= 0.V by A1,VECTSP_4:def 2;
  thus thesis by A1,VECTSP_4:def 2;
end;

definition
  let F be Field;
  let V be VectSp of F;
  let W1,W2 be Subspace of V;
  func segment(W1,W2) -> Subset of Subspaces(V) means
  :Def1:
  for W being
  strict Subspace of V holds W in it iff W1 is Subspace of W & W is Subspace of
  W2 if W1 is Subspace of W2 otherwise it={};
  consistency;
  existence
  proof
    hereby
      defpred P[set] means for W being Subspace of V st W=$1 holds W1 is
      Subspace of W & W is Subspace of W2;
      set A=Subspaces(V);
      assume W1 is Subspace of W2;
      consider X being Subset of A such that
A1:   for x being set holds x in X iff x in A & P[x] from SUBSET_1:sch
      1;
      take X;
      let W be strict Subspace of V;
      thus W in X implies W1 is Subspace of W & W is Subspace of W2 by A1;
      assume W1 is Subspace of W & W is Subspace of W2;
      then
A2:   P[W];
      W in Subspaces(V) by VECTSP_5:def 3;
      hence W in X by A1,A2;
    end;
    hereby
      reconsider W={} as Subset of Subspaces(V) by XBOOLE_1:2;
      assume not W1 is Subspace of W2;
      take W;
      thus W={};
    end;
  end;
  uniqueness
  proof
    let S,T be Subset of Subspaces(V);
    now
      assume W1 is Subspace of W2;
      assume that
A3:   for W being strict Subspace of V holds W in S iff W1 is Subspace
      of W & W is Subspace of W2 and
A4:   for W being strict Subspace of V holds W in T iff W1 is Subspace
      of W & W is Subspace of W2;
      now
        let x be set;
        thus x in S implies x in T
        proof
          assume
A5:       x in S;
          then consider x1 being strict Subspace of V such that
A6:       x1=x by VECTSP_5:def 3;
          x1 in S iff W1 is Subspace of x1 & x1 is Subspace of W2 by A3;
          hence thesis by A4,A5,A6;
        end;
        assume
A7:     x in T;
        then consider x1 being strict Subspace of V such that
A8:     x1=x by VECTSP_5:def 3;
        x1 in T iff W1 is Subspace of x1 & x1 is Subspace of W2 by A4;
        hence x in S by A3,A7,A8;
      end;
      hence S=T by TARSKI:1;
    end;
    hence thesis;
  end;
end;

theorem Th6:
  for F being Field for V being VectSp of F for W1,W2,W3,W4 being
  Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega).W1=
  (Omega).W3 & (Omega).W2=(Omega).W4 holds segment(W1,W2) = segment(W3,W4)
proof
  let F be Field;
  let V be VectSp of F;
  let W1,W2,W3,W4 be Subspace of V;
  assume that
A1: W1 is Subspace of W2 and
A2: W3 is Subspace of W4 and
A3: (Omega).W1=(Omega).W3 and
A4: (Omega).W2=(Omega).W4;
  thus segment(W1,W2) c= segment(W3,W4)
  proof
    let a be set;
    assume
A5: a in segment(W1,W2);
    then ex A1 being strict Subspace of V st A1=a by VECTSP_5:def 3;
    then reconsider A=a as strict Subspace of V;
    A is Subspace of W2 by A1,A5,Def1;
    then A is Subspace of (Omega).W2 by Th2;
    then
A6: A is Subspace of W4 by A4,Th3;
    W1 is Subspace of A by A1,A5,Def1;
    then (Omega).W1 is Subspace of A by Th4;
    then W3 is Subspace of A by A3,Th5;
    hence thesis by A2,A6,Def1;
  end;
  let a be set;
  assume
A7: a in segment(W3,W4);
  then ex A1 being strict Subspace of V st A1=a by VECTSP_5:def 3;
  then reconsider A=a as strict Subspace of V;
  A is Subspace of W4 by A2,A7,Def1;
  then A is Subspace of (Omega).W4 by Th2;
  then
A8: A is Subspace of W2 by A4,Th3;
  W3 is Subspace of A by A2,A7,Def1;
  then (Omega).W3 is Subspace of A by Th4;
  then W1 is Subspace of A by A3,Th5;
  hence thesis by A1,A8,Def1;
end;

definition
  let F be Field;
  let V be VectSp of F;
  let W1,W2 be Subspace of V;
  func pencil(W1,W2) -> Subset of Subspaces(V) equals
  segment(W1,W2) \ {
  (Omega).W1,(Omega).W2};
  coherence;
end;

theorem
  for F being Field for V being VectSp of F for W1,W2,W3,W4 being
  Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega).W1=
(Omega).W3 & (Omega).W2=(Omega).W4 holds pencil(W1,W2) = pencil(W3,W4) by Th6;

definition
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let W1,W2 be Subspace of V;
  let k be Nat;
  func pencil(W1,W2,k) -> Subset of (k Subspaces_of V) equals
  pencil (W1,W2)
  /\ (k Subspaces_of V);
  coherence by XBOOLE_1:17;
end;

theorem Th8:
  for F being Field for V being finite-dimensional VectSp of F for
k being Nat for W1,W2,W being Subspace of V st W in pencil(W1,W2,k) holds W1 is
  Subspace of W & W is Subspace of W2
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let k be Nat;
  let W1,W2,W be Subspace of V;
  assume
A1: W in pencil(W1,W2,k);
  then
A2: ex X being strict Subspace of V st W=X & dim X=k by VECTSP_9:def 2;
  W in pencil(W1,W2) by A1,XBOOLE_0:def 4;
  then
A3: W in segment(W1,W2) by XBOOLE_0:def 5;
  then W1 is Subspace of W2 by Def1;
  hence thesis by A2,A3,Def1;
end;

theorem
  for F being Field for V being finite-dimensional VectSp of F for k
  being Nat for W1,W2,W3,W4 being Subspace of V st W1 is Subspace of W2 & W3 is
Subspace of W4 & (Omega).W1=(Omega).W3 & (Omega).W2=(Omega).W4 holds pencil(W1,
  W2,k) = pencil(W3,W4,k) by Th6;

definition
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let k be Nat;
  func k Pencils_of V -> Subset-Family of (k Subspaces_of V) means
  :Def4:
  for
X being set holds X in it iff ex W1,W2 being Subspace of V st W1 is Subspace of
  W2 & dim W1+1=k & dim W2=k+1 & X=pencil(W1,W2,k);
  existence
  proof
    defpred P[set] means ex W1,W2 being Subspace of V st W1 is Subspace of W2
    & dim W1+1=k & dim W2=k+1 & $1=pencil(W1,W2,k);
    set A = bool (k Subspaces_of V);
    consider X being set such that
A1: for x being set holds x in X iff x in A & P[x] from XBOOLE_0:sch 1;
    X c= A
    proof
      let a be set;
      assume a in X;
      hence thesis by A1;
    end;
    then reconsider X as Subset-Family of (k Subspaces_of V);
    take X;
    let x be set;
    thus x in X implies ex W1,W2 being Subspace of V st W1 is Subspace of W2 &
    dim W1+1=k & dim W2=k+1 & x=pencil(W1,W2,k) by A1;
    given W1,W2 being Subspace of V such that
A2: W1 is Subspace of W2 & dim W1+1=k & dim W2=k+1 & x=pencil(W1,W2,k);
    thus thesis by A1,A2;
  end;
  uniqueness
  proof
    let S,T be Subset-Family of (k Subspaces_of V) such that
A3: for X being set holds X in S iff ex W1,W2 being Subspace of V st
    W1 is Subspace of W2 & dim W1+1=k & dim W2=k+1 & X=pencil(W1,W2,k) and
A4: for X being set holds X in T iff ex W1,W2 being Subspace of V st
    W1 is Subspace of W2 & dim W1+1=k & dim W2=k+1 & X=pencil(W1,W2,k);
    now
      let x be set;
      thus x in S implies x in T
      proof
        assume x in S;
        then
        ex W1,W2 being Subspace of V st W1 is Subspace of W2 & dim W1+1=k
        & dim W2=k+1 & x=pencil(W1,W2,k) by A3;
        hence thesis by A4;
      end;
      assume x in T;
      then
      ex W1,W2 being Subspace of V st W1 is Subspace of W2 & dim W1+1=k &
      dim W2=k+1 & x=pencil(W1,W2,k) by A4;
      hence x in S by A3;
    end;
    hence thesis by TARSKI:1;
  end;
end;

theorem Th10:
  for F being Field for V being finite-dimensional VectSp of F for
  k being Nat st 1 <= k & k < dim V holds k Pencils_of V is non empty
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let k be Nat;
  assume that
A1: 1 <= k and
A2: k < dim V;
  k+1 <= dim V by A2,NAT_1:13;
  then consider W2 being strict Subspace of V such that
A3: dim W2 = k+1 by VECTSP_9:35;
  k-'1<=k by NAT_D:35;
  then k-'1 <= dim W2 by A3,NAT_1:13;
  then consider W1 being strict Subspace of W2 such that
A4: dim W1 = k-'1 by VECTSP_9:35;
  reconsider W19=W1 as Subspace of V by VECTSP_4:26;
  dim W1+1=k by A1,A4,XREAL_1:235;
  then pencil(W19,W2,k) in k Pencils_of V by A3,Def4;
  hence thesis;
end;

theorem Th11:
  for F being Field for V being finite-dimensional VectSp of F for
W1,W2,P,Q being Subspace of V for k being Nat st dim W1+1=k & dim W2=k+1 & P in
  pencil(W1,W2,k) & Q in pencil(W1,W2,k) & P<>Q holds P/\Q = (Omega).W1 & P+Q =
  (Omega).W2
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let W1,W2,P0,Q0 be Subspace of V;
  let k be Nat such that
A1: dim W1+1=k and
A2: dim W2=k+1 and
A3: P0 in pencil(W1,W2,k) and
A4: Q0 in pencil(W1,W2,k) and
A5: P0<>Q0;
  consider Q being strict Subspace of V such that
A6: Q=Q0 and
A7: dim Q = k by A4,VECTSP_9:def 2;
A8: W1 is Subspace of Q by A4,A6,Th8;
  consider P being strict Subspace of V such that
A9: P=P0 and
A10: dim P = k by A3,VECTSP_9:def 2;
  W1 is Subspace of P by A3,A9,Th8;
  then
A11: W1 is Subspace of (P/\Q) by A8,VECTSP_5:19;
  P/\Q is Subspace of P by VECTSP_5:15;
  then
A12: dim(P/\Q)<=k by A10,VECTSP_9:25;
  per cases by A1,A12,A11,NAT_1:9,VECTSP_9:25;
  suppose
A13: dim W1 = dim (P/\Q);
    then (Omega).W1 = (Omega).(P/\Q) by A11,VECTSP_9:28;
    hence P0/\Q0 = (Omega).W1 by A9,A6;
    P is Subspace of W2 & Q is Subspace of W2 by A3,A4,A9,A6,Th8;
    then
A14: P+Q is Subspace of W2 by VECTSP_5:34;
    dim(P+Q)+dim W1-dim W1 = dim P + dim Q - dim W1 by A13,VECTSP_9:32;
    then (Omega).(W2) = (Omega).(P+Q) by A1,A2,A10,A7,A14,VECTSP_9:28;
    hence thesis by A9,A6;
  end;
  suppose
A15: dim (P/\Q)=k;
    P/\Q is Subspace of Q by VECTSP_5:15;
    then
A16: (Omega).(P/\Q) = (Omega).Q by A7,A15,VECTSP_9:28;
    P/\Q is Subspace of P by VECTSP_5:15;
    then (Omega).(P/\Q) = (Omega).P by A10,A15,VECTSP_9:28;
    hence thesis by A5,A9,A6,A16;
  end;
end;

theorem Th12:
  for F being Field for V being finite-dimensional VectSp of F for
  v being Vector of V st v <> 0.V holds dim Lin{v} = 1
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let v be Vector of V;
  assume v <> 0.V;
  then
A1: v <> 0.Lin{v} by VECTSP_4:11;
  v in {v} by TARSKI:def 1;
  then v in Lin{v} by VECTSP_7:8;
  then reconsider v0=v as Vector of Lin{v} by STRUCT_0:def 5;
  Lin{v0}=Lin{v} & (Omega).Lin{v0} = Lin{v0} by VECTSP_9:17;
  hence thesis by A1,VECTSP_9:30;
end;

theorem Th13:
  for F being Field for V being finite-dimensional VectSp of F for
W being Subspace of V for v being Vector of V st not v in W holds dim(W+Lin{v})
  =dim W + 1
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let W be Subspace of V;
  let v be Vector of V such that
A1: not v in W;
  the carrier of (Omega).(W/\Lin{v}) = {0.(W/\Lin{v})}
  proof
    thus the carrier of (Omega).(W/\Lin{v}) c= {0.(W/\Lin{v})}
    proof
      let a be set;
      assume a in the carrier of (Omega).(W/\Lin{v});
      then
A2:   a in (the carrier of W)/\the carrier of Lin{v} by VECTSP_5:def 2;
      then a in the carrier of Lin{v} by XBOOLE_0:def 4;
      then a in Lin{v} by STRUCT_0:def 5;
      then consider e being Element of F such that
A3:   a=e*v by VECTSP10:3;
      a in the carrier of W by A2,XBOOLE_0:def 4;
      then
A4:   a in W by STRUCT_0:def 5;
      now
        assume e<>0.F;
        then v=e"*(e*v) by VECTSP_1:20;
        hence contradiction by A1,A4,A3,VECTSP_4:21;
      end;
      then a=0.V by A3,VECTSP_1:14;
      then a = 0.(W/\Lin{v}) by VECTSP_4:11;
      hence thesis by TARSKI:def 1;
    end;
    let a be set;
    assume a in {0.(W/\Lin{v})};
    then a=0.(W/\Lin{v}) by TARSKI:def 1;
    then a=0.V by VECTSP_4:11;
    then a in W/\Lin{v} by VECTSP_4:17;
    hence thesis by STRUCT_0:def 5;
  end;
  then (Omega).(W/\Lin{v})=(0).(W/\Lin{v}) by VECTSP_4:def 3;
  then
A5: dim(W/\Lin{v})=0 by VECTSP_9:29;
A6: dim(W+Lin{v}) + dim(W/\Lin{v}) = dim W + dim Lin{v} by VECTSP_9:32;
  v <> 0.V by A1,VECTSP_4:17;
  hence thesis by A5,A6,Th12;
end;

theorem Th14:
  for F being Field for V being finite-dimensional VectSp of F for
  W being Subspace of V for v,u being Vector of V st v<>u & {v,u} is
  linearly-independent & W/\Lin{v,u}=(0).V holds dim(W+Lin{v,u})=dim W + 2
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let W be Subspace of V;
  let v,u be Vector of V such that
A1: v<>u and
A2: {v,u} is linearly-independent and
A3: W/\Lin{v,u}=(0).V;
  u in {v,u} by TARSKI:def 2;
  then
A4: u in Lin{v,u} by VECTSP_7:8;
  v in {v,u} by TARSKI:def 2;
  then v in Lin{v,u} by VECTSP_7:8;
  then reconsider v1=v,u1=u as Vector of Lin{v,u} by A4,STRUCT_0:def 5;
  reconsider L={v1,u1} as linearly-independent Subset of Lin{v,u} by A2,
VECTSP_9:12;
  (Omega).Lin{v,u}=Lin L by VECTSP_9:17;
  then
A5: dim Lin{v,u}=2 by A1,VECTSP_9:31;
  (Omega).(W/\Lin{v,u})=(0).(W/\Lin{v,u}) by A3,VECTSP_4:36;
  then dim(W/\Lin{v,u}) = 0 by VECTSP_9:29;
  hence dim(W+Lin{v,u}) = dim(W+Lin{v,u}) + dim(W/\Lin{v,u})
    .= dim W + 2 by A5,VECTSP_9:32;
end;

theorem Th15:
  for F being Field for V being finite-dimensional VectSp of F for
W1,W2 being Subspace of V st W1 is Subspace of W2 for k being Nat st dim W1+1=k
  & dim W2=k+1 for v being Vector of V st v in W2 & not v in W1 holds W1+Lin{v}
  in pencil(W1,W2,k)
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let W1,W2 be Subspace of V such that
A1: W1 is Subspace of W2;
  let k be Nat such that
A2: dim W1+1=k and
A3: dim W2=k+1;
  let v be Vector of V such that
A4: v in W2 and
A5: not v in W1;
  set W=W1+Lin{v};
A6: dim W = k by A2,A5,Th13;
  then
A7: W in k Subspaces_of V by VECTSP_9:def 2;
  v in the carrier of W2 by A4,STRUCT_0:def 5;
  then {v} c= the carrier of W2 by ZFMISC_1:31;
  then Lin{v} is Subspace of W2 by VECTSP_9:16;
  then W1 is Subspace of W & W is Subspace of W2 by A1,VECTSP_5:7,34;
  then
A8: W in segment(W1,W2) by A1,Def1;
  dim (Omega).W2 = k+1 by A3,VECTSP_9:27;
  then
A9: W <> (Omega).W2 by A6;
  dim (Omega).W1 + 1 = k by A2,VECTSP_9:27;
  then W <> (Omega).W1 by A6;
  then not W in {(Omega).W1,(Omega).W2} by A9,TARSKI:def 2;
  then W in pencil(W1,W2) by A8,XBOOLE_0:def 5;
  hence thesis by A7,XBOOLE_0:def 4;
end;

theorem Th16:
  for F being Field for V being finite-dimensional VectSp of F for
W1,W2 being Subspace of V st W1 is Subspace of W2 for k being Nat st dim W1+1=k
  & dim W2=k+1 holds pencil(W1,W2,k) is non trivial
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let W1,W2 be Subspace of V;
  assume W1 is Subspace of W2;
  then reconsider U=W1 as Subspace of W2;
  let k be Nat such that
A1: dim W1+1=k & dim W2=k+1;
  set W = the Linear_Compl of U;
A2: W2 is_the_direct_sum_of W,U by VECTSP_5:def 5;
  then
A3: W /\ U = (0).W2 by VECTSP_5:def 4;
  dim W2 = dim U + dim W by A2,VECTSP_9:34;
  then consider u,v being Vector of W such that
A4: u <> v and
A5: {u,v} is linearly-independent and
  (Omega).W = Lin{u,v} by A1,VECTSP_9:31;
A6: now
    assume v in Lin{u};
    then ex a being Element of F st v = a*u by VECTSP10:3;
    hence contradiction by A4,A5,VECTSP_7:5;
  end;
  reconsider u,v as Vector of W2 by VECTSP_4:10;
  reconsider u1=u,v1=v as Vector of V by VECTSP_4:10;
A7: v in W by STRUCT_0:def 5;
A8: now
    assume v in W1;
    then v in (0).W2 by A3,A7,VECTSP_5:3;
    then v=0.W2 by VECTSP_4:35;
    then v=0.W by VECTSP_4:11;
    hence contradiction by A5,VECTSP_7:4;
  end;
A9: u in W by STRUCT_0:def 5;
A10: now
    assume u in W1;
    then u in (0).W2 by A3,A9,VECTSP_5:3;
    then u=0.W2 by VECTSP_4:35;
    then u=0.W by VECTSP_4:11;
    hence contradiction by A5,VECTSP_7:4;
  end;
  v in {v1} by TARSKI:def 1;
  then v in Lin{v1} by VECTSP_7:8;
  then
A11: v in W1+Lin{v1} by VECTSP_5:2;
A12: not v in Lin{u} by A6,VECTSP10:13;
A13: now
    reconsider Wx=W as Subspace of V by VECTSP_4:26;
    assume W1+Lin{v1} = W1+Lin{u1};
    then consider h,j being Vector of V such that
A14: h in W1 and
A15: j in Lin{u1} and
A16: v1 = h+j by A11,VECTSP_5:1;
    consider a being Element of F such that
A17: j=a*u1 by A15,VECTSP10:3;
    v1-a*u1=h+(a*u1-a*u1) by A16,A17,RLVECT_1:def 3;
    then v1-a*u1=h+0.V by RLVECT_1:15;
    then
A18: v1-a*u1=h by RLVECT_1:4;
    a*u = a*u1 by VECTSP_4:14;
    then
A19: v1-a*u1 = v-a*u by VECTSP_4:16;
    a*u in Wx by A9,VECTSP_4:21;
    then v-a*u in Wx by A7,VECTSP_4:23;
    then v-a*u in W/\U by A14,A18,A19,VECTSP_5:3;
    then v-a*u = 0.W2 by A3,VECTSP_4:35;
    then h = 0.V by A18,A19,VECTSP_4:11;
    then v1 = j by A16,RLVECT_1:4;
    hence contradiction by A12,A15,VECTSP10:13;
  end;
  v in W2 by STRUCT_0:def 5;
  then
A20: W1+Lin{v1} in pencil(W1,W2,k) by A1,A8,Th15;
  u in W2 by STRUCT_0:def 5;
  then W1+Lin{u1} in pencil(W1,W2,k) by A1,A10,Th15;
  then 2 c= card pencil(W1,W2,k) by A13,A20,PENCIL_1:2;
  hence thesis by PENCIL_1:4;
end;

definition
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let k be Nat;
  func PencilSpace(V,k) -> strict TopStruct equals
  TopStruct(#k Subspaces_of V
    , k Pencils_of V#);
  coherence;
end;

theorem Th17:
  for F being Field for V being finite-dimensional VectSp of F for
  k being Nat st 1 <= k & k < dim V holds PencilSpace(V,k) is non void
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let k be Nat such that
A1: 1 <= k & k < dim V;
  set S=PencilSpace(V,k);
  the topology of S is non empty by A1,Th10;
  hence thesis by PENCIL_1:def 4;
end;

theorem Th18:
  for F being Field for V being finite-dimensional VectSp of F for
  k being Nat st 1 <= k & k < dim V & 3 <= dim V holds PencilSpace(V,k) is non
  degenerated
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let k be Nat such that
A1: 1 <= k and
A2: k < dim V and
A3: 3 <= dim V;
  set S=PencilSpace(V,k);
  now
    let B be Block of S;
    the topology of S is non empty by A1,A2,Th10;
    then consider W1,W2 being Subspace of V such that
A4: W1 is Subspace of W2 and
A5: dim W1+1=k and
A6: dim W2=k+1 and
A7: B=pencil(W1,W2,k) by Def4;
A8: the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
    per cases by A2,A3,Th1;
    suppose
      k+1 < dim V;
      then
A9:   (Omega).W2 <> (Omega).V by A6,VECTSP_9:28;
A10:  now
        assume
A11:    the carrier of V = the carrier of W2;
        (Omega).W2 is Subspace of V by Th4;
        hence contradiction by A9,A11,VECTSP_4:29;
      end;
      the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
      then not the carrier of V c= the carrier of W2 by A10,XBOOLE_0:def 10;
      then consider v being set such that
A12:  v in the carrier of V and
A13:  not v in the carrier of W2 by TARSKI:def 3;
      reconsider v as Vector of V by A12;
      set X=W1+Lin{v};
A14:  now
        v in {v} by TARSKI:def 1;
        then v in Lin{v} by VECTSP_7:8;
        then v in X by VECTSP_5:2;
        then
A15:    v in the carrier of X by STRUCT_0:def 5;
        assume X in B;
        then X is Subspace of W2 by A7,Th8;
        then the carrier of X c= the carrier of W2 by VECTSP_4:def 2;
        hence contradiction by A13,A15;
      end;
      not v in W2 by A13,STRUCT_0:def 5;
      then dim X = k by A4,A5,Th13,VECTSP_4:8;
      hence the carrier of S <> B by A14,VECTSP_9:def 2;
    end;
    suppose
A16:  2 <= k & k+1>=dim V;
      set I = the Basis of W1;
      reconsider I1=I as finite Subset of W1 by VECTSP_9:20;
      2-1 <= dim W1+1-1 by A5,A16,XREAL_1:9;
      then 1 <= card I1 by VECTSP_9:def 1;
      then I1 is non empty;
      then consider i being set such that
A17:  i in I by XBOOLE_0:def 1;
      reconsider i as Vector of W1 by A17;
      reconsider J=I1\{i} as finite Subset of V by A8,XBOOLE_1:1;
      I is linearly-independent by VECTSP_7:def 3;
      then I\{i} is linearly-independent by VECTSP_7:1,XBOOLE_1:36;
      then reconsider JJ=I\{i} as linearly-independent Subset of V by
VECTSP_9:11;
      J c= the carrier of Lin J
      proof
        let a be set;
        assume a in J;
        then a in Lin J by VECTSP_7:8;
        hence thesis by STRUCT_0:def 5;
      end;
      then reconsider JJJ=JJ as linearly-independent Subset of Lin J by
VECTSP_9:12;
      Lin JJJ = Lin J by VECTSP_9:17;
      then
A18:  J is Basis of Lin J by VECTSP_7:def 3;
A19:  card I = dim W1 by VECTSP_9:def 1;
      set T = the Linear_Compl of W1;
A20:  V is_the_direct_sum_of W1,T by VECTSP_5:38;
      then
A21:  W1/\T=(0).V by VECTSP_5:def 4;
      k+1 <= dim V by A2,NAT_1:13;
      then dim V = k+1 by A16,XXREAL_0:1;
      then k+1 - (dim W1 + 1) = dim W1 + dim T - (dim W1 + 1) by A20,
VECTSP_9:34;
      then consider u,v being Vector of T such that
A22:  u<>v and
A23:  {u,v} is linearly-independent and
A24:  (Omega).T=Lin{u,v} by A5,VECTSP_9:31;
A25:  v in the carrier of T;
      the carrier of T c= the carrier of V & u in the carrier of T by
VECTSP_4:def 2;
      then reconsider u1=u,v1=v as Vector of V by A25;
      reconsider Y={u,v} as linearly-independent Subset of V by A23,VECTSP_9:11
;
A26:  Y={u,v};
      Lin (I\{i}) is Subspace of Lin I by VECTSP_7:13,XBOOLE_1:36;
      then
A27:  Lin J is Subspace of W1 by VECTSP_9:17;
      the carrier of ((Lin J)/\Lin{u1,v1}) c= the carrier of (0).V
      proof
        let a be set;
        assume a in the carrier of ((Lin J)/\Lin{u1,v1});
        then
A28:    a in (Lin J)/\Lin{u1,v1} by STRUCT_0:def 5;
        then a in Lin {u1,v1} by VECTSP_5:3;
        then a in Lin{u,v} by VECTSP_9:17;
        then a in the carrier of the VectSpStr of T by A24,STRUCT_0:def 5;
        then
A29:    a in T by STRUCT_0:def 5;
        a in Lin J by A28,VECTSP_5:3;
        then a in W1 by A27,VECTSP_4:8;
        then a in W1 /\ T by A29,VECTSP_5:3;
        hence thesis by A21,STRUCT_0:def 5;
      end;
      then
A30:  (0).V is Subspace of (Lin J)/\Lin{u1,v1} & (Lin J)/\Lin{u1,v1} is
      Subspace of (0).V by VECTSP_4:27,39;
      card J = card I1 - card{i} by A17,EULER_1:4
        .= dim W1 - 1 by A19,CARD_1:30;
      then dim Lin J = dim W1 - 1 by A18,VECTSP_9:def 1;
      then
A31:  dim ((Lin J)+Lin{u1,v1}) = dim W1 - 1 + 2 by A22,A26,A30,Th14,VECTSP_4:25
;
A32:  Lin I = (Omega).W1 by VECTSP_7:def 3;
A33:  i in W1 by STRUCT_0:def 5;
      now
A34:    now
          reconsider IV=I as Subset of V by A8,XBOOLE_1:1;
          assume
A35:      i in (Lin J)+Lin{u1,v1};
          IV c= the carrier of (Lin J)+Lin{u1,v1}
          proof
            let a be set;
            {i} c= I by A17,ZFMISC_1:31;
            then
A36:        I\{i}\/{i}=I by XBOOLE_1:45;
            assume
A37:        a in IV;
            per cases by A37,A36,XBOOLE_0:def 3;
            suppose
              a in J;
              then
A38:          a in Lin J by VECTSP_7:8;
              then a in V by VECTSP_4:9;
              then reconsider o=a as Vector of V by STRUCT_0:def 5;
              o in (Lin J)+Lin{u1,v1} by A38,VECTSP_5:2;
              hence thesis by STRUCT_0:def 5;
            end;
            suppose
              a in {i};
              then a=i by TARSKI:def 1;
              hence thesis by A35,STRUCT_0:def 5;
            end;
          end;
          then Lin IV is Subspace of (Lin J)+Lin{u1,v1} by VECTSP_9:16;
          then Lin I is Subspace of (Lin J)+Lin{u1,v1} by VECTSP_9:17;
          then
A39:      W1 is Subspace of (Lin J)+Lin{u1,v1} by A32,Th5;
          the carrier of (W1/\Lin{u1,v1}) c= the carrier of (0).V
          proof
            let a be set;
            assume a in the carrier of (W1/\Lin{u1,v1});
            then
A40:        a in W1/\Lin{u1,v1} by STRUCT_0:def 5;
            then a in Lin {u1,v1} by VECTSP_5:3;
            then a in Lin {u,v} by VECTSP_9:17;
            then a in the carrier of the VectSpStr of T by A24,STRUCT_0:def 5;
            then
A41:        a in T by STRUCT_0:def 5;
            a in W1 by A40,VECTSP_5:3;
            then a in W1 /\ T by A41,VECTSP_5:3;
            hence thesis by A21,STRUCT_0:def 5;
          end;
          then (0).V is Subspace of W1/\Lin{u1,v1} & W1/\Lin{u1,v1} is
          Subspace of (0).V by VECTSP_4:27,39;
          then
A42:      dim (W1+Lin{u1,v1}) = dim W1 + 2 by A22,A26,Th14,VECTSP_4:25;
          Lin{u1,v1} is Subspace of (Lin J)+Lin{u1,v1} by VECTSP_5:7;
          then W1+Lin{u1,v1} is Subspace of (Lin J)+Lin{u1,v1} by A39,
VECTSP_5:34;
          then dim W1 + 1+1 <= dim W1 + 1 by A31,A42,VECTSP_9:25;
          hence contradiction by NAT_1:13;
        end;
        assume (Lin J)+Lin{u1,v1} in B;
        then W1 is Subspace of (Lin J)+Lin{u1,v1} by A7,Th8;
        hence contradiction by A33,A34,VECTSP_4:8;
      end;
      hence the carrier of S <> B by A5,A31,VECTSP_9:def 2;
    end;
  end;
  then not the carrier of S is Block of S;
  hence S is non degenerated by PENCIL_1:def 5;
end;

theorem Th19:
  for F being Field for V being finite-dimensional VectSp of F for
  k being Nat st 1 <= k & k < dim V holds PencilSpace(V,k) is
  with_non_trivial_blocks
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let k be Nat such that
A1: 1 <= k & k < dim V;
  set S=PencilSpace(V,k);
  thus S is with_non_trivial_blocks
  proof
    let X be Block of S;
    S is non void by A1,Th17;
    then
    ex W1,W2 being Subspace of V st W1 is Subspace of W2 & dim W1+1=k & dim
    W2=k+1 & X=pencil(W1,W2,k) by Def4;
    then X is non trivial by Th16;
    hence thesis by PENCIL_1:4;
  end;
end;

theorem Th20:
  for F being Field for V being finite-dimensional VectSp of F for
  k being Nat st 1 <= k & k < dim V holds PencilSpace(V,k) is
  identifying_close_blocks
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let k be Nat such that
A1: 1 <= k and
A2: k < dim V;
  set S=PencilSpace(V,k);
  thus S is identifying_close_blocks
  proof
    let X,Y be Block of S;
    assume 2 c= card(X/\Y);
    then consider P,Q being set such that
A3: P in X/\Y & Q in X/\Y and
A4: P<>Q by PENCIL_1:2;
A5: P in X & Q in X by A3,XBOOLE_0:def 4;
A6: P in Y & Q in Y by A3,XBOOLE_0:def 4;
A7: S is non void by A1,A2,Th17;
    then consider W1,W2 being Subspace of V such that
A8: W1 is Subspace of W2 and
A9: dim W1+1=k & dim W2=k+1 and
A10: X=pencil(W1,W2,k) by Def4;
    the topology of S is non empty by A7;
    then X in the topology of S;
    then reconsider P,Q as Point of S by A5;
A11: S is non empty by A2,VECTSP_9:36;
    then ex P1 being strict Subspace of V st P1=P & dim P1 = k by
VECTSP_9:def 2;
    then reconsider P as strict Subspace of V;
    ex Q1 being strict Subspace of V st Q1=Q & dim Q1 = k by A11,VECTSP_9:def 2
;
    then reconsider Q as strict Subspace of V;
    consider U1,U2 being Subspace of V such that
A12: U1 is Subspace of U2 and
A13: dim U1+1=k & dim U2=k+1 and
A14: Y=pencil(U1,U2,k) by A7,Def4;
A15: (Omega).W2=P+Q by A4,A5,A9,A10,Th11
      .= (Omega).U2 by A4,A6,A13,A14,Th11;
    (Omega).W1=P/\Q by A4,A5,A9,A10,Th11
      .= (Omega).U1 by A4,A6,A13,A14,Th11;
    hence thesis by A8,A10,A12,A14,A15,Th6;
  end;
end;

theorem
  for F being Field for V being finite-dimensional VectSp of F for k
  being Nat st 1 <= k & k < dim V & 3 <= dim V holds PencilSpace(V,k) is PLS
by Th17,Th18,Th19,Th20,VECTSP_9:36;

begin :: Grassmann spaces

definition
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let m,n be Nat;
  func SubspaceSet(V,m,n) -> Subset-Family of m Subspaces_of V means
  :Def6:
for X being set holds X in it iff ex W being Subspace of V st dim W = n & X = m
  Subspaces_of W;
  existence
  proof
    defpred P[set] means ex W being Subspace of V st dim W = n & $1 = m
    Subspaces_of W;
    set A=bool (m Subspaces_of V);
    consider X being set such that
A1: for x being set holds x in X iff x in A & P[x] from XBOOLE_0:sch 1;
    X c= A
    proof
      let a be set;
      assume a in X;
      hence thesis by A1;
    end;
    then reconsider X as Subset-Family of m Subspaces_of V;
    take X;
    let x be set;
    thus x in X implies ex W being Subspace of V st dim W=n & x = m
    Subspaces_of W by A1;
    given W being Subspace of V such that
A2: dim W=n and
A3: x = m Subspaces_of W;
    x c= m Subspaces_of V by A3,VECTSP_9:38;
    hence thesis by A1,A2,A3;
  end;
  uniqueness
  proof
    let S,T be Subset-Family of m Subspaces_of V such that
A4: for X being set holds X in S iff ex W being Subspace of V st dim W
    = n & X = m Subspaces_of W and
A5: for X being set holds X in T iff ex W being Subspace of V st dim W
    = n & X = m Subspaces_of W;
    now
      let X be set;
      thus X in S implies X in T
      proof
        assume X in S;
        then ex W being Subspace of V st dim W = n & X = m Subspaces_of W by A4
;
        hence thesis by A5;
      end;
      assume X in T;
      then ex W being Subspace of V st dim W = n & X = m Subspaces_of W by A5;
      hence X in S by A4;
    end;
    hence thesis by TARSKI:1;
  end;
end;

theorem Th22:
  for F being Field for V being finite-dimensional VectSp of F for
  m,n be Nat st n <= dim V holds SubspaceSet(V,m,n) is non empty
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let m,n be Nat;
  assume n <= dim V;
  then consider W being strict Subspace of V such that
A1: dim W = n by VECTSP_9:35;
  m Subspaces_of W in SubspaceSet(V,m,n) by A1,Def6;
  hence thesis;
end;

theorem Th23:
  for F being Field for W1,W2 being finite-dimensional VectSp of F
  st (Omega).W1 = (Omega).W2 for m being Nat holds m Subspaces_of W1 = m
  Subspaces_of W2
proof
  let F be Field;
  let W1,W2 be finite-dimensional VectSp of F such that
A1: (Omega).W1 = (Omega).W2;
  let m be Nat;
  (Omega).W1 is Subspace of (Omega).W2 by A1,VECTSP_4:24;
  then W1 is Subspace of (Omega).W2 by Th5;
  then W1 is Subspace of W2 by Th3;
  hence m Subspaces_of W1 c= m Subspaces_of W2 by VECTSP_9:38;
  (Omega).W2 is Subspace of (Omega).W1 by A1,VECTSP_4:24;
  then W2 is Subspace of (Omega).W1 by Th5;
  then W2 is Subspace of W1 by Th3;
  hence thesis by VECTSP_9:38;
end;

theorem Th24:
  for F being Field for V being finite-dimensional VectSp of F for
  W being Subspace of V for m being Nat st 1<=m & m <= dim V & m Subspaces_of V
  c= m Subspaces_of W holds (Omega).V = (Omega).W
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let W be Subspace of V;
  let m be Nat such that
A1: 1<=m and
A2: m <= dim V and
A3: m Subspaces_of V c= m Subspaces_of W;
  hereby
A4: dim W <= dim V by VECTSP_9:25;
    assume
A5: (Omega).V <> (Omega).W;
    then dim W <> dim V by VECTSP_9:28;
    then
A6: dim W < dim V by A4,XXREAL_0:1;
    per cases by A2,XXREAL_0:1;
    suppose
      m=dim V;
      then m Subspaces_of W = {} by A6,VECTSP_9:37;
      hence contradiction by A2,A3,VECTSP_9:36;
    end;
    suppose
A7:   m < dim V;
A8:   now
        assume
A9:     the carrier of V = the carrier of W;
        (Omega).W is strict Subspace of V by Th4;
        hence contradiction by A5,A9,VECTSP_4:29;
      end;
      the carrier of W c= the carrier of V by VECTSP_4:def 2;
      then not the carrier of V c= the carrier of W by A8,XBOOLE_0:def 10;
      then consider x being set such that
A10:  x in the carrier of V and
A11:  not x in the carrier of W by TARSKI:def 3;
      reconsider x as Vector of V by A10;
      0.V in W by VECTSP_4:17;
      then x <> 0.V by A11,STRUCT_0:def 5;
      then {x} is linearly-independent by VECTSP_7:3;
      then consider I being Basis of V such that
A12:  {x} c= I by VECTSP_7:19;
      reconsider J=I as finite Subset of V by VECTSP_9:20;
      card J = dim V by VECTSP_9:def 1;
      then consider K being Subset of J such that
A13:  card K = m by A7,Lm1;
A14:  I is linearly-independent by VECTSP_7:def 3;
      per cases;
      suppose
A15:    x in K;
        reconsider L=K as finite Subset of V by XBOOLE_1:1;
        L c= the carrier of Lin L
        proof
          let a be set;
          assume a in L;
          then a in Lin L by VECTSP_7:8;
          hence thesis by STRUCT_0:def 5;
        end;
        then reconsider L9=L as Subset of Lin L;
        L is linearly-independent by A14,VECTSP_7:1;
        then reconsider LL1 = L9 as linearly-independent Subset of Lin L by
VECTSP_9:12;
        Lin LL1 = the VectSpStr of Lin L by VECTSP_9:17;
        then L is Basis of Lin L by VECTSP_7:def 3;
        then dim Lin L = m by A13,VECTSP_9:def 1;
        then Lin L in m Subspaces_of V by VECTSP_9:def 2;
        then ex M being strict Subspace of W st M=Lin L & dim M = m by A3,
VECTSP_9:def 2;
        then x in W by A15,VECTSP_4:9,VECTSP_7:8;
        hence contradiction by A11,STRUCT_0:def 5;
      end;
      suppose
A16:    not x in K;
        consider y being set such that
A17:    y in K by A1,A13,CARD_1:27,XBOOLE_0:def 1;
        (K\{y})\/{x} c= the carrier of V
        proof
          let a be set;
          assume a in (K\{y})\/{x};
          then a in (K\{y}) or a in {x} by XBOOLE_0:def 3;
          hence thesis by TARSKI:def 3;
        end;
        then reconsider L=(K\{y})\/{x} as finite Subset of V;
        L c= the carrier of Lin L
        proof
          let a be set;
          assume a in L;
          then a in Lin L by VECTSP_7:8;
          hence thesis by STRUCT_0:def 5;
        end;
        then reconsider L9=L as Subset of Lin L;
        L c= I
        proof
          let a be set;
          assume a in L;
          then a in K\{y} or a in {x} by XBOOLE_0:def 3;
          hence thesis by A12;
        end;
        then L is linearly-independent by A14,VECTSP_7:1;
        then reconsider LL1 = L9 as linearly-independent Subset of Lin L by
VECTSP_9:12;
        Lin LL1 = the VectSpStr of Lin L by VECTSP_9:17;
        then
A18:    L is Basis of Lin L by VECTSP_7:def 3;
        not x in K\{y} by A16,XBOOLE_0:def 5;
        then card L = card(K\{y})+1 by CARD_2:41
          .= card K - card{y} + 1 by A17,EULER_1:4
          .= card K - 1 + 1 by CARD_1:30
          .= m by A13;
        then dim Lin L = m by A18,VECTSP_9:def 1;
        then Lin L in m Subspaces_of V by VECTSP_9:def 2;
        then
A19:    ex M being strict Subspace of W st M=Lin L & dim M = m by A3,
VECTSP_9:def 2;
        x in {x} by TARSKI:def 1;
        then x in L by XBOOLE_0:def 3;
        then x in W by A19,VECTSP_4:9,VECTSP_7:8;
        hence contradiction by A11,STRUCT_0:def 5;
      end;
    end;
  end;
end;

definition
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let m,n be Nat;
  func GrassmannSpace(V,m,n) -> strict TopStruct equals
  TopStruct(#m
    Subspaces_of V, SubspaceSet(V,m,n)#);
  coherence;
end;

theorem Th25:
  for F being Field for V being finite-dimensional VectSp of F for
  m,n being Nat st n <= dim V holds GrassmannSpace(V,m,n) is non void
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let m,n be Nat;
  assume n <= dim V;
  then the topology of GrassmannSpace(V,m,n) is non empty by Th22;
  hence thesis by PENCIL_1:def 4;
end;

theorem Th26:
  for F being Field for V being finite-dimensional VectSp of F for
m,n being Nat st 1 <= m & m < n & n < dim V holds GrassmannSpace(V,m,n) is non
  degenerated
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let m,n be Nat such that
A1: 1 <= m and
A2: m < n and
A3: n < dim V;
  set S=GrassmannSpace(V,m,n);
A4: m < dim V by A2,A3,XXREAL_0:2;
  hereby
    assume
A5: the carrier of S is Block of S;
    the topology of S is non empty by A3,Th22;
    then consider W being Subspace of V such that
A6: dim W = n and
A7: m Subspaces_of V = m Subspaces_of W by A5,Def6;
    (Omega).V = (Omega).W by A1,A4,A7,Th24;
    then dim W = dim (Omega).V by VECTSP_9:27;
    hence contradiction by A3,A6,VECTSP_9:27;
  end;
end;

theorem Th27:
  for F being Field for V being finite-dimensional VectSp of F for
  m,n being Nat st 1 <= m & m < n & n <= dim V holds GrassmannSpace(V,m,n) is
  with_non_trivial_blocks
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let m,n be Nat such that
A1: 1 <= m and
A2: m < n and
A3: n <= dim V;
  set S=GrassmannSpace(V,m,n);
  let B be Block of S;
  the topology of S is non empty by A3,Th22;
  then consider W being Subspace of V such that
A4: dim W = n and
A5: B = m Subspaces_of W by Def6;
  m+1 <= n by A2,NAT_1:13;
  then consider U being strict Subspace of W such that
A6: dim U = m+1 by A4,VECTSP_9:35;
  set I = the Basis of U;
A7: card I = m+1 by A6,VECTSP_9:def 1;
  reconsider I9=I as finite Subset of U by VECTSP_9:20;
  reconsider m as Element of NAT by ORDINAL1:def 12;
  1+1 <= m+1 by A1,XREAL_1:7;
  then 2 c= card I by A7,NAT_1:39;
  then consider i,j being set such that
A8: i in I and
A9: j in I and
A10: i<>j by PENCIL_1:2;
  reconsider I1=I9\{i} as finite Subset of U;
  I1 c= the carrier of Lin I1
  proof
    let a be set;
    assume a in I1;
    then a in Lin I1 by VECTSP_7:8;
    hence thesis by STRUCT_0:def 5;
  end;
  then reconsider I19=I1 as Subset of Lin I1;
A11: I is linearly-independent by VECTSP_7:def 3;
  then I1 is linearly-independent by VECTSP_7:1,XBOOLE_1:36;
  then reconsider II1=I19 as linearly-independent Subset of Lin I1 by
VECTSP_9:12;
  Lin II1 = the VectSpStr of Lin I1 by VECTSP_9:17;
  then
A12: I1 is Basis of Lin I1 by VECTSP_7:def 3;
  reconsider I2=I9\{j} as finite Subset of U;
  I2 c= the carrier of Lin I2
  proof
    let a be set;
    assume a in I2;
    then a in Lin I2 by VECTSP_7:8;
    hence thesis by STRUCT_0:def 5;
  end;
  then reconsider I29=I2 as Subset of Lin I2;
  I2 is linearly-independent by A11,VECTSP_7:1,XBOOLE_1:36;
  then reconsider II2=I29 as linearly-independent Subset of Lin I2 by
VECTSP_9:12;
  Lin II2 = the VectSpStr of Lin I2 by VECTSP_9:17;
  then
A13: I2 is Basis of Lin I2 by VECTSP_7:def 3;
  card I2 = card I9 - card{j} by A9,EULER_1:4
    .= m+1 - 1 by A7,CARD_1:30;
  then
A14: dim Lin I2 = m by A13,VECTSP_9:def 1;
  Lin I2 is strict Subspace of W by VECTSP_4:26;
  then
A15: Lin I2 in B by A5,A14,VECTSP_9:def 2;
  card I1 = card I9 - card{i} by A8,EULER_1:4
    .= m+1 - 1 by A7,CARD_1:30;
  then
A16: dim Lin I1 = m by A12,VECTSP_9:def 1;
  Lin I1 is strict Subspace of W by VECTSP_4:26;
  then
A17: Lin I1 in B by A5,A16,VECTSP_9:def 2;
  not j in {i} by A10,TARSKI:def 1;
  then j in I1 by A9,XBOOLE_0:def 5;
  then
A18: j in Lin I1 by VECTSP_7:8;
  not j in Lin I2 by A11,A9,VECTSP_9:14;
  hence thesis by A17,A15,A18,PENCIL_1:2;
end;

theorem Th28:
  for F being Field for V being finite-dimensional VectSp of F for
  m being Nat st m+1 <= dim V holds GrassmannSpace(V,m,m+1) is
  identifying_close_blocks
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let m be Nat such that
A1: m+1 <= dim V;
  set S = GrassmannSpace(V,m,m+1);
  let K,L be Block of S;
A2: the topology of S is non empty by A1,Th22;
  then consider W1 being Subspace of V such that
A3: dim W1 = m+1 and
A4: K = m Subspaces_of W1 by Def6;
  assume 2 c= card(K/\L);
  then consider x,y being set such that
A5: x in K/\L and
A6: y in K/\L and
A7: x <> y by PENCIL_1:2;
  y in K by A6,XBOOLE_0:def 4;
  then consider Y being strict Subspace of W1 such that
A8: y=Y and
A9: dim Y = m by A4,VECTSP_9:def 2;
  consider W2 being Subspace of V such that
A10: dim W2 = m+1 and
A11: L = m Subspaces_of W2 by A2,Def6;
  y in L by A6,XBOOLE_0:def 4;
  then consider Y9 being strict Subspace of W2 such that
A12: y=Y9 and
  dim Y9 = m by A11,VECTSP_9:def 2;
  x in L by A5,XBOOLE_0:def 4;
  then consider X9 being strict Subspace of W2 such that
A13: x=X9 and
  dim X9 = m by A11,VECTSP_9:def 2;
  x in K by A5,XBOOLE_0:def 4;
  then consider X being strict Subspace of W1 such that
A14: x=X and
A15: dim X = m by A4,VECTSP_9:def 2;
  reconsider x,y as strict Subspace of V by A14,A8,VECTSP_4:26;
A16: now
    reconsider y9=y as strict Subspace of x+y by VECTSP_5:7;
    reconsider x9=x as strict Subspace of x+y by VECTSP_5:7;
    assume
A17: dim(x+y)=m;
    then (Omega).x9 = (Omega).(x+y) by A14,A15,VECTSP_9:28;
    then x = y+x by VECTSP_5:5;
    then
A18: y is Subspace of x by VECTSP_5:8;
    (Omega).y9 = (Omega).(x+y) by A8,A9,A17,VECTSP_9:28;
    then x is Subspace of y by VECTSP_5:8;
    hence contradiction by A7,A18,VECTSP_4:25;
  end;
  x+y is Subspace of W1 by A14,A8,VECTSP_5:34;
  then x is Subspace of x+y & dim (x+y) <= m+1 by A3,VECTSP_5:7,VECTSP_9:25;
  then
A19: dim (x+y) = m+1 by A14,A15,A16,NAT_1:9,VECTSP_9:25;
  X9+Y9=x+y by A13,A12,VECTSP10:12;
  then
A20: (Omega).(X9+Y9) = (Omega).W2 by A10,A19,VECTSP_9:28;
A21: X+Y=x+y by A14,A8,VECTSP10:12;
  then (Omega).(X+Y) = (Omega).W1 by A3,A19,VECTSP_9:28;
  hence thesis by A4,A11,A13,A12,A21,A20,Th23,VECTSP10:12;
end;

theorem
  for F being Field for V being finite-dimensional VectSp of F for m
  being Nat st 1 <= m & m+1 < dim V holds GrassmannSpace(V,m,m+1) is PLS
proof
  let F be Field;
  let V be finite-dimensional VectSp of F;
  let m be Nat;
  assume that
A1: 1 <= m and
A2: m+1 < dim V;
A3: m < m+1 by NAT_1:13;
  m <= dim V by A2,NAT_1:13;
  hence thesis by A1,A2,A3,Th25,Th26,Th27,Th28,VECTSP_9:36;
end;

begin :: Veronese spaces

definition
  let X be set;
  func PairSet(X) means
  :Def8:
  for z being set holds z in it iff ex x,y being
  set st x in X & y in X & z={x,y};
  existence
  proof
    defpred P[set] means ex x,y being set st x in X & y in X & $1={x,y};
    consider S being set such that
A1: for z being set holds z in S iff z in bool X & P[z] from XBOOLE_0:
    sch 1;
    take S;
    let z be set;
    thus z in S implies P[z] by A1;
    assume
A2: P[z];
    then z c= X by ZFMISC_1:32;
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    let p1,p2 be set such that
A3: for z being set holds z in p1 iff ex x,y being set st x in X & y
    in X & z={x,y} and
A4: for z being set holds z in p2 iff ex x,y being set st x in X & y
    in X & z={x,y};
    now
      let z be set;
      z in p1 iff ex x,y being set st x in X & y in X & z={x,y} by A3;
      hence z in p1 iff z in p2 by A4;
    end;
    hence thesis by TARSKI:1;
  end;
end;

registration
  let X be non empty set;
  cluster PairSet(X) -> non empty;
  coherence
  proof
    consider x being set such that
A1: x in X by XBOOLE_0:def 1;
    {x,x} in PairSet(X) by A1,Def8;
    hence thesis;
  end;
end;

definition
  let t,X be set;
  func PairSet(t,X) means
  :Def9:
  for z being set holds z in it iff ex y being set st y in X & z={t,y};
  existence
  proof
    t in {t} by TARSKI:def 1;
    then
A1: t in X\/{t} by XBOOLE_0:def 3;
    defpred P[set] means ex y being set st y in X & $1={t,y};
    consider S being set such that
A2: for z being set holds z in S iff z in bool (X\/{t}) & P[z] from
    XBOOLE_0:sch 1;
    take S;
    let z be set;
    thus z in S implies P[z] by A2;
    assume
A3: P[z];
    then consider y being set such that
A4: y in X and
A5: z={t,y};
    y in X\/{t} by A4,XBOOLE_0:def 3;
    then z c= X\/{t} by A5,A1,ZFMISC_1:32;
    hence thesis by A2,A3;
  end;
  uniqueness
  proof
    let p1,p2 be set such that
A6: for z being set holds z in p1 iff ex y being set st y in X & z={t, y} and
A7: for z being set holds z in p2 iff ex y being set st y in X & z={t ,y};
    now
      let z be set;
      z in p1 iff ex y being set st y in X & z={t,y} by A6;
      hence z in p1 iff z in p2 by A7;
    end;
    hence thesis by TARSKI:1;
  end;
end;

registration
  let t be set;
  let X be non empty set;
  cluster PairSet(t,X) -> non empty;
  coherence
  proof
    consider x being set such that
A1: x in X by XBOOLE_0:def 1;
    {t,x} in PairSet(t,X) by A1,Def9;
    hence thesis;
  end;
end;

registration
  let t be set;
  let X be non trivial set;
  cluster PairSet(t,X) -> non trivial;
  coherence
  proof
    2 c= card X by PENCIL_1:4;
    then consider x,y being set such that
A1: x in X & y in X and
A2: x<>y by PENCIL_1:2;
A3: now
      assume
A4:   {t,x}={t,y};
      then y=t by A2,ZFMISC_1:6;
      hence contradiction by A2,A4,ZFMISC_1:6;
    end;
    {t,x} in PairSet(t,X) & {t,y} in PairSet(t,X) by A1,Def9;
    then 2 c= card PairSet(t,X) by A3,PENCIL_1:2;
    hence thesis by PENCIL_1:4;
  end;
end;

definition
  let X be set;
  let L be Subset-Family of X;
  func PairSetFamily(L) -> Subset-Family of PairSet(X) means
  :Def10:
  for S
  being set holds S in it iff ex t being set, l being Subset of X st t in X & l
  in L & S=PairSet(t,l);
  existence
  proof
    set A=PairSet(X);
    defpred P[Subset of A] means ex t being set, l being Subset of X st t in X
    & l in L & $1=PairSet(t,l);
    consider F being Subset-Family of A such that
A1: for B being Subset of A holds B in F iff P[B] from SUBSET_1:sch 3;
    take F;
    let S be set;
    thus S in F implies ex t being set, l being Subset of X st t in X & l in L
    & S=PairSet(t,l) by A1;
    given t being set, l being Subset of X such that
A2: t in X and
A3: l in L and
A4: S=PairSet(t,l);
    S c= PairSet(X)
    proof
      let a be set;
      assume a in S;
      then ex y being set st y in l & a={t,y} by A4,Def9;
      hence thesis by A2,Def8;
    end;
    hence thesis by A1,A2,A3,A4;
  end;
  uniqueness
  proof
    let p1,p2 be Subset-Family of PairSet(X) such that
A5: for z being set holds z in p1 iff ex t being set, l being Subset
    of X st t in X & l in L & z=PairSet(t,l) and
A6: for z being set holds z in p2 iff ex t being set, l being Subset
    of X st t in X & l in L & z=PairSet(t,l);
    now
      let z be set;
      z in p1 iff ex t being set, l being Subset of X st t in X & l in L
      & z=PairSet(t,l) by A5;
      hence z in p1 iff z in p2 by A6;
    end;
    hence thesis by TARSKI:1;
  end;
end;

registration
  let X be non empty set;
  let L be non empty Subset-Family of X;
  cluster PairSetFamily(L) -> non empty;
  coherence
  proof
    consider l being set such that
A1: l in L by XBOOLE_0:def 1;
    consider t being set such that
A2: t in X by XBOOLE_0:def 1;
    PairSet(t,l) in PairSetFamily(L) by A2,A1,Def10;
    hence thesis;
  end;
end;

definition
  let S be TopStruct;
  func VeroneseSpace(S) -> strict TopStruct equals
  TopStruct(#PairSet(the
    carrier of S), PairSetFamily(the topology of S)#);
  coherence;
end;

registration
  let S be non empty TopStruct;
  cluster VeroneseSpace(S) -> non empty;
  coherence;
end;

registration
  let S be non empty non void TopStruct;
  cluster VeroneseSpace(S) -> non void;
  coherence
  proof
    thus the topology of VeroneseSpace(S) is non empty;
  end;
end;

registration
  let S be non empty non void non degenerated TopStruct;
  cluster VeroneseSpace(S) -> non degenerated;
  coherence
  proof
    assume the carrier of VeroneseSpace(S) is Block of VeroneseSpace(S);
    then consider t being set, l being Subset of S such that
A1: t in the carrier of S and
A2: l in the topology of S and
A3: PairSet(the carrier of S)=PairSet(t,l) by Def10;
    not the carrier of S in the topology of S by PENCIL_1:def 5;
    then not the carrier of S c= l by A2,XBOOLE_0:def 10;
    then consider s being set such that
A4: s in the carrier of S and
A5: not s in l by TARSKI:def 3;
    now
      assume {t,s} in PairSet(t,l);
      then
A6:   ex z being set st z in l & {t,s}={t,z} by Def9;
      then s = t by A5,ZFMISC_1:6;
      hence contradiction by A5,A6,ZFMISC_1:6;
    end;
    hence contradiction by A1,A3,A4,Def8;
  end;
end;

registration
  let S be non empty non void with_non_trivial_blocks TopStruct;
  cluster VeroneseSpace(S) -> with_non_trivial_blocks;
  coherence
  proof
    let L be Block of VeroneseSpace(S);
    consider t being set, l being Subset of S such that
    t in the carrier of S and
A1: l in the topology of S and
A2: L=PairSet(t,l) by Def10;
    2 c= card l by A1,PENCIL_1:def 6;
    then reconsider l as non trivial set by PENCIL_1:4;
    PairSet(t,l) is non trivial;
    hence thesis by A2,PENCIL_1:4;
  end;
end;

registration
  let S be identifying_close_blocks TopStruct;
  cluster VeroneseSpace(S) -> identifying_close_blocks;
  coherence
  proof
    let K,L be Block of VeroneseSpace(S);
    assume 2 c= card (K/\L);
    then consider a,b being set such that
A1: a in K/\L and
A2: b in K/\L and
A3: a <> b by PENCIL_1:2;
A4: a in K by A1,XBOOLE_0:def 4;
    then
A5: the topology of VeroneseSpace(S) is non empty by SUBSET_1:def 1;
    then consider t being set, k being Subset of S such that
    t in the carrier of S and
A6: k in the topology of S and
A7: K=PairSet(t,k) by Def10;
    b in K by A2,XBOOLE_0:def 4;
    then consider y being set such that
A8: y in k and
A9: b={t,y} by A7,Def9;
    consider x being set such that
A10: x in k and
A11: a={t,x} by A4,A7,Def9;
    consider s being set, l being Subset of S such that
    s in the carrier of S and
A12: l in the topology of S and
A13: L=PairSet(s,l) by A5,Def10;
    a in L by A1,XBOOLE_0:def 4;
    then consider z being set such that
A14: z in l and
A15: a={s,z} by A13,Def9;
    b in L by A2,XBOOLE_0:def 4;
    then consider w being set such that
A16: w in l and
A17: b={s,w} by A13,Def9;
A18: t=s or t=z by A11,A15,ZFMISC_1:6;
    now
      assume
A19:  y<>w;
      then y=t by A3,A9,A15,A17,A18,ZFMISC_1:6;
      hence contradiction by A9,A17,A19,ZFMISC_1:6;
    end;
    then
A20: y in k/\l by A8,A16,XBOOLE_0:def 4;
A21: t=s or t=w by A9,A17,ZFMISC_1:6;
    now
      assume
A22:  x<>z;
      then x=t by A3,A11,A15,A17,A21,ZFMISC_1:6;
      hence contradiction by A11,A15,A22,ZFMISC_1:6;
    end;
    then x in k/\l by A10,A14,XBOOLE_0:def 4;
    then 2 c= card (k/\l) by A3,A11,A9,A20,PENCIL_1:2;
    hence thesis by A3,A6,A7,A12,A13,A15,A17,A18,A21,PENCIL_1:def 7;
  end;
end;