pencil_4.miz



    begin

    theorem :: PENCIL_4:1

    

     Th1: for k,n be 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 be finite set holds for n be Nat st n <= ( card X) holds ex Y be Subset of X st ( card Y) = n by FINSEQ_4: 72;

    theorem :: PENCIL_4:2

    

     Th2: for F be Field holds for V be VectSp of F holds for W be 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 :: PENCIL_4:3

    

     Th3: for F be Field holds for V be VectSp of F holds for W be 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 :: PENCIL_4:4

    

     Th4: for F be Field holds for V be VectSp of F holds for W be 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 :: PENCIL_4:5

    

     Th5: for F be Field holds for V,W be 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;

      :: PENCIL_4:def1

      func segment (W1,W2) -> Subset of ( Subspaces V) means

      : Def1: for W be 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 be 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 be Subset of A such that

           A1: for x be 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 be strict Subspace of V holds W in S iff W1 is Subspace of W & W is Subspace of W2 and

           A4: for W be strict Subspace of V holds W in T iff W1 is Subspace of W & W is Subspace of W2;

          now

            let x be object;

            thus x in S implies x in T

            proof

              assume

               A5: x in S;

              then

              consider x1 be 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 be 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: 2;

        end;

        hence thesis;

      end;

    end

    theorem :: PENCIL_4:6

    

     Th6: for F be Field holds for V be VectSp of F holds for W1,W2,W3,W4 be 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 object;

        assume

         A5: a in ( segment (W1,W2));

        then ex A1 be 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 object;

      assume

       A7: a in ( segment (W3,W4));

      then ex A1 be 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;

      :: PENCIL_4:def2

      func pencil (W1,W2) -> Subset of ( Subspaces V) equals (( segment (W1,W2)) \ {( (Omega). W1), ( (Omega). W2)});

      coherence ;

    end

    theorem :: PENCIL_4:7

    for F be Field holds for V be VectSp of F holds for W1,W2,W3,W4 be 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;

      :: PENCIL_4:def3

      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 :: PENCIL_4:8

    

     Th8: for F be Field holds for V be finite-dimensional VectSp of F holds for k be Nat holds for W1,W2,W be 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 be 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 :: PENCIL_4:9

    for F be Field holds for V be finite-dimensional VectSp of F holds for k be Nat holds for W1,W2,W3,W4 be 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;

      :: PENCIL_4:def4

      func k Pencils_of V -> Subset-Family of (k Subspaces_of V) means

      : Def4: for X be set holds X in it iff ex W1,W2 be 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[ object] means ex W1,W2 be 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 be set such that

         A1: for x be object holds x in X iff x in A & P[x] from XBOOLE_0:sch 1;

        X c= A by A1;

        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 be 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 be 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 be set holds X in S iff ex W1,W2 be 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 be set holds X in T iff ex W1,W2 be 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 object;

          thus x in S implies x in T

          proof

            assume x in S;

            then ex W1,W2 be 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 be 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: 2;

      end;

    end

    theorem :: PENCIL_4:10

    

     Th10: for F be Field holds for V be finite-dimensional VectSp of F holds for k be 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 be 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 be 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 :: PENCIL_4:11

    

     Th11: for F be Field holds for V be finite-dimensional VectSp of F holds for W1,W2,P,Q be Subspace of V holds for k be 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 be 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 be 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 :: PENCIL_4:12

    

     Th12: for F be Field holds for V be finite-dimensional VectSp of F holds for v be 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});

      ( Lin {v0}) = ( Lin {v}) & ( (Omega). ( Lin {v0})) = ( Lin {v0}) by VECTSP_9: 17;

      hence thesis by A1, VECTSP_9: 30;

    end;

    theorem :: PENCIL_4:13

    

     Th13: for F be Field holds for V be finite-dimensional VectSp of F holds for W be Subspace of V holds for v be 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 object;

          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});

          then

          consider e be 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;

          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 object;

        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;

      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 :: PENCIL_4:14

    

     Th14: for F be Field holds for V be finite-dimensional VectSp of F holds for W be Subspace of V holds for v,u be 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;

      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 :: PENCIL_4:15

    

     Th15: for F be Field holds for V be finite-dimensional VectSp of F holds for W1,W2 be Subspace of V st W1 is Subspace of W2 holds for k be Nat st (( dim W1) + 1) = k & ( dim W2) = (k + 1) holds for v be 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;

      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, VECTSP_5: 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 :: PENCIL_4:16

    

     Th16: for F be Field holds for V be finite-dimensional VectSp of F holds for W1,W2 be Subspace of V st W1 is Subspace of W2 holds for k be 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 be 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 be 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;

       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;

       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 be 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 be 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;

      then

       A20: (W1 + ( Lin {v1})) in ( pencil (W1,W2,k)) by A1, A8, Th15;

      u in W2;

      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;

      :: PENCIL_4:def5

      func PencilSpace (V,k) -> strict TopStruct equals TopStruct (# (k Subspaces_of V), (k Pencils_of V) #);

      coherence ;

    end

    theorem :: PENCIL_4:17

    

     Th17: for F be Field holds for V be finite-dimensional VectSp of F holds for k be Nat st 1 <= k & k < ( dim V) holds ( PencilSpace (V,k)) is non void by Th10;

    theorem :: PENCIL_4:18

    

     Th18: for F be Field holds for V be finite-dimensional VectSp of F holds for k be 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 be 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;

          then

          consider v be object such that

           A12: v in the carrier of V and

           A13: not v in the carrier of W2;

          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;

            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;

          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 be object such that

           A17: i in I;

          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 object;

            assume a in J;

            then a in ( Lin J) by VECTSP_7: 8;

            hence thesis;

          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 be 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;

          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;

          reconsider Y = {u, v} as linearly-independent Subset of V by A23, VECTSP_9: 11;

          

           A25: Y = {u, v};

          ( Lin (I \ {i})) is Subspace of ( Lin I) by VECTSP_7: 13, XBOOLE_1: 36;

          then

           A26: ( 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 object;

            assume a in the carrier of (( Lin J) /\ ( Lin {u1, v1}));

            then

             A27: a in (( Lin J) /\ ( Lin {u1, v1}));

            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 ModuleStr of T by A24;

            then

             A28: a in T;

            a in ( Lin J) by A27, VECTSP_5: 3;

            then a in W1 by A26, VECTSP_4: 8;

            then a in (W1 /\ T) by A28, VECTSP_5: 3;

            hence thesis by A21;

          end;

          then

           A29: ( (0). V) is Subspace of (( Lin J) /\ ( Lin {u1, v1})) & (( Lin J) /\ ( Lin {u1, v1})) is Subspace of ( (0). V) by VECTSP_4: 27, VECTSP_4: 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

           A30: ( dim (( Lin J) + ( Lin {u1, v1}))) = ((( dim W1) - 1) + 2) by A22, A25, A29, Th14, VECTSP_4: 25;

          

           A31: ( Lin I) = ( (Omega). W1) by VECTSP_7:def 3;

          

           A32: i in W1;

          now

             A33:

            now

              reconsider IV = I as Subset of V by A8, XBOOLE_1: 1;

              assume

               A34: i in (( Lin J) + ( Lin {u1, v1}));

              IV c= the carrier of (( Lin J) + ( Lin {u1, v1}))

              proof

                let a be object;

                 {i} c= I by A17, ZFMISC_1: 31;

                then

                 A35: ((I \ {i}) \/ {i}) = I by XBOOLE_1: 45;

                assume

                 A36: a in IV;

                per cases by A36, A35, XBOOLE_0:def 3;

                  suppose a in J;

                  then

                   A37: a in ( Lin J) by VECTSP_7: 8;

                  then a in V by VECTSP_4: 9;

                  then

                  reconsider o = a as Vector of V;

                  o in (( Lin J) + ( Lin {u1, v1})) by A37, VECTSP_5: 2;

                  hence thesis;

                end;

                  suppose a in {i};

                  then a = i by TARSKI:def 1;

                  hence thesis by A34;

                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

               A38: W1 is Subspace of (( Lin J) + ( Lin {u1, v1})) by A31, Th5;

              the carrier of (W1 /\ ( Lin {u1, v1})) c= the carrier of ( (0). V)

              proof

                let a be object;

                assume a in the carrier of (W1 /\ ( Lin {u1, v1}));

                then

                 A39: a in (W1 /\ ( Lin {u1, v1}));

                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 ModuleStr of T by A24;

                then

                 A40: a in T;

                a in W1 by A39, VECTSP_5: 3;

                then a in (W1 /\ T) by A40, VECTSP_5: 3;

                hence thesis by A21;

              end;

              then ( (0). V) is Subspace of (W1 /\ ( Lin {u1, v1})) & (W1 /\ ( Lin {u1, v1})) is Subspace of ( (0). V) by VECTSP_4: 27, VECTSP_4: 39;

              then

               A41: ( dim (W1 + ( Lin {u1, v1}))) = (( dim W1) + 2) by A22, A25, 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 A38, VECTSP_5: 34;

              then ((( dim W1) + 1) + 1) <= (( dim W1) + 1) by A30, A41, 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 A32, A33, VECTSP_4: 8;

          end;

          hence the carrier of S <> B by A5, A30, VECTSP_9:def 2;

        end;

      end;

      then not the carrier of S is Block of S;

      hence S is non degenerated;

    end;

    theorem :: PENCIL_4:19

    

     Th19: for F be Field holds for V be finite-dimensional VectSp of F holds for k be 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 be 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 :: PENCIL_4:20

    

     Th20: for F be Field holds for V be finite-dimensional VectSp of F holds for k be 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 be object 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 be 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 be 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 be 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 be 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 :: PENCIL_4:21

    for F be Field holds for V be finite-dimensional VectSp of F holds for k be 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

    definition

      let F be Field;

      let V be finite-dimensional VectSp of F;

      let m,n be Nat;

      :: PENCIL_4:def6

      func SubspaceSet (V,m,n) -> Subset-Family of (m Subspaces_of V) means

      : Def6: for X be set holds X in it iff ex W be Subspace of V st ( dim W) = n & X = (m Subspaces_of W);

      existence

      proof

        defpred P[ object] means ex W be Subspace of V st ( dim W) = n & $1 = (m Subspaces_of W);

        set A = ( bool (m Subspaces_of V));

        consider X be set such that

         A1: for x be object holds x in X iff x in A & P[x] from XBOOLE_0:sch 1;

        X c= A by A1;

        then

        reconsider X as Subset-Family of (m Subspaces_of V);

        take X;

        let x be set;

        thus x in X implies ex W be Subspace of V st ( dim W) = n & x = (m Subspaces_of W) by A1;

        given W be 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 be set holds X in S iff ex W be Subspace of V st ( dim W) = n & X = (m Subspaces_of W) and

         A5: for X be set holds X in T iff ex W be Subspace of V st ( dim W) = n & X = (m Subspaces_of W);

        now

          let X be object;

          thus X in S implies X in T

          proof

            assume X in S;

            then ex W be 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 be 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: 2;

      end;

    end

    theorem :: PENCIL_4:22

    

     Th22: for F be Field holds for V be finite-dimensional VectSp of F holds 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 be 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 :: PENCIL_4:23

    

     Th23: for F be Field holds for W1,W2 be finite-dimensional VectSp of F st ( (Omega). W1) = ( (Omega). W2) holds for m be 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 :: PENCIL_4:24

    

     Th24: for F be Field holds for V be finite-dimensional VectSp of F holds for W be Subspace of V holds for m be 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;

          then

          consider x be object such that

           A10: x in the carrier of V and

           A11: not x in the carrier of W;

          reconsider x as Vector of V by A10;

          ( 0. V) in W by VECTSP_4: 17;

          then x <> ( 0. V) by A11;

          then {x} is linearly-independent by VECTSP_7: 3;

          then

          consider I be 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 be 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 object;

              assume a in L;

              then a in ( Lin L) by VECTSP_7: 8;

              hence thesis;

            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 ModuleStr 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 be 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;

          end;

            suppose

             A16: not x in K;

            consider y be object 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 object;

              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 object;

              assume a in L;

              then a in ( Lin L) by VECTSP_7: 8;

              hence thesis;

            end;

            then

            reconsider L9 = L as Subset of ( Lin L);

            L c= I

            proof

              let a be object;

              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 ModuleStr 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 be 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;

          end;

        end;

      end;

    end;

    definition

      let F be Field;

      let V be finite-dimensional VectSp of F;

      let m,n be Nat;

      :: PENCIL_4:def7

      func GrassmannSpace (V,m,n) -> strict TopStruct equals TopStruct (# (m Subspaces_of V), ( SubspaceSet (V,m,n)) #);

      coherence ;

    end

    theorem :: PENCIL_4:25

    

     Th25: for F be Field holds for V be finite-dimensional VectSp of F holds for m,n be Nat st n <= ( dim V) holds ( GrassmannSpace (V,m,n)) is non void by Th22;

    theorem :: PENCIL_4:26

    

     Th26: for F be Field holds for V be finite-dimensional VectSp of F holds for m,n be 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 be 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 :: PENCIL_4:27

    

     Th27: for F be Field holds for V be finite-dimensional VectSp of F holds for m,n be 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 be 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 be 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 ( Segm 2) c= ( Segm (m + 1)) by NAT_1: 39;

      then

      consider i,j be object such that

       A8: i in I and

       A9: j in I and

       A10: i <> j by PENCIL_1: 2, A7;

      reconsider I1 = (I9 \ {i}) as finite Subset of U;

      I1 c= the carrier of ( Lin I1)

      proof

        let a be object;

        assume a in I1;

        then a in ( Lin I1) by VECTSP_7: 8;

        hence thesis;

      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 ModuleStr 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 object;

        assume a in I2;

        then a in ( Lin I2) by VECTSP_7: 8;

        hence thesis;

      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 ModuleStr 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 :: PENCIL_4:28

    

     Th28: for F be Field holds for V be finite-dimensional VectSp of F holds for m be 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 be 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 be object 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 be strict Subspace of W1 such that

       A8: y = Y and

       A9: ( dim Y) = m by A4, VECTSP_9:def 2;

      consider W2 be 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 be 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 be 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 be 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 :: PENCIL_4:29

    for F be Field holds for V be finite-dimensional VectSp of F holds for m be 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

    definition

      let X be set;

      :: PENCIL_4:def8

      func PairSet (X) -> set means

      : Def8: for z be set holds z in it iff ex x,y be set st x in X & y in X & z = {x, y};

      existence

      proof

        defpred P[ object] means ex x,y be set st x in X & y in X & $1 = {x, y};

        consider S be set such that

         A1: for z be object 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 be set holds z in p1 iff ex x,y be set st x in X & y in X & z = {x, y} and

         A4: for z be set holds z in p2 iff ex x,y be set st x in X & y in X & z = {x, y};

        now

          let z be object;

          z in p1 iff ex x,y be 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: 2;

      end;

    end

    registration

      let X be non empty set;

      cluster ( PairSet X) -> non empty;

      coherence

      proof

        consider x be object 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 be object, X be set;

      :: PENCIL_4:def9

      func PairSet (t,X) -> set means

      : Def9: for z be set holds z in it iff ex y be 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[ object] means ex y be set st y in X & $1 = {t, y};

        consider S be set such that

         A2: for z be object 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 be 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 be set holds z in p1 iff ex y be set st y in X & z = {t, y} and

         A7: for z be set holds z in p2 iff ex y be set st y in X & z = {t, y};

        now

          let z be object;

          z in p1 iff ex y be 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: 2;

      end;

    end

    registration

      let t be set;

      let X be non empty set;

      cluster ( PairSet (t,X)) -> non empty;

      coherence

      proof

        consider x be object 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 be object 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;

      :: PENCIL_4:def10

      func PairSetFamily (L) -> Subset-Family of ( PairSet X) means

      : Def10: for S be set holds S in it iff ex t be set, l be 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 be set, l be Subset of X st t in X & l in L & $1 = ( PairSet (t,l));

        consider F be Subset-Family of A such that

         A1: for B be 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 be set, l be Subset of X st t in X & l in L & S = ( PairSet (t,l)) by A1;

        given t be set, l be 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 object;

          assume a in S;

          then ex y be 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 be set holds z in p1 iff ex t be set, l be Subset of X st t in X & l in L & z = ( PairSet (t,l)) and

         A6: for z be set holds z in p2 iff ex t be set, l be Subset of X st t in X & l in L & z = ( PairSet (t,l));

        now

          let z be object;

          z in p1 iff ex t be set, l be 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: 2;

      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 be object such that

         A1: l in L by XBOOLE_0:def 1;

        reconsider l as set by TARSKI: 1;

        consider t be object 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;

      :: PENCIL_4:def11

      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 ;

    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 be set, l be 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 be object such that

         A4: s in the carrier of S and

         A5: not s in l;

        now

          assume {t, s} in ( PairSet (t,l));

          then

           A6: ex z be 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 be set, l be 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 be object 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 be set, k be 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 be set such that

         A8: y in k and

         A9: b = {t, y} by A7, Def9;

        consider x be set such that

         A10: x in k and

         A11: a = {t, x} by A4, A7, Def9;

        consider s be set, l be 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 be 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 be 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