vectsp10.miz



    begin

    definition

      let K be doubleLoopStr;

      :: VECTSP10:def1

      func StructVectSp (K) -> strict ModuleStr over K equals ModuleStr (# the carrier of K, the addF of K, ( 0. K), the multF of K #);

      coherence ;

    end

    registration

      let K be non empty doubleLoopStr;

      cluster ( StructVectSp K) -> non empty;

      coherence ;

    end

    registration

      let K be Abelian non empty doubleLoopStr;

      cluster ( StructVectSp K) -> Abelian;

      coherence

      proof

        set V = ( StructVectSp K);

        now

          let x,y be Vector of V;

          reconsider x9 = x, y9 = y as Element of K;

          

          thus (x + y) = (y9 + x9) by RLVECT_1: 2

          .= (y + x);

        end;

        hence thesis;

      end;

    end

    registration

      let K be add-associative non empty doubleLoopStr;

      cluster ( StructVectSp K) -> add-associative;

      coherence

      proof

        set V = ( StructVectSp K);

        now

          let x,y,z be Vector of V;

          reconsider x9 = x, y9 = y, z9 = z as Element of K;

          

          thus ((x + y) + z) = ((x9 + y9) + z9)

          .= (x9 + (y9 + z9)) by RLVECT_1:def 3

          .= (x + (y + z));

        end;

        hence thesis;

      end;

    end

    registration

      let K be right_zeroed non empty doubleLoopStr;

      cluster ( StructVectSp K) -> right_zeroed;

      coherence

      proof

        set V = ( StructVectSp K);

        now

          let x be Vector of V;

          reconsider x9 = x as Element of K;

          

          thus (x + ( 0. V)) = (x9 + ( 0. K))

          .= x by RLVECT_1:def 4;

        end;

        hence thesis;

      end;

    end

    registration

      let K be right_complementable non empty doubleLoopStr;

      cluster ( StructVectSp K) -> right_complementable;

      coherence

      proof

        set V = ( StructVectSp K);

        let x be Vector of V;

        reconsider x9 = x as Element of K;

        consider t be Element of K such that

         A1: (x9 + t) = ( 0. K) by ALGSTR_0:def 11;

        reconsider t9 = t as Vector of V;

        take t9;

        thus thesis by A1;

      end;

    end

    registration

      let K be associative left_unital distributive non empty doubleLoopStr;

      cluster ( StructVectSp K) -> vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        set V = ( StructVectSp K);

        now

          let x,y be Element of K;

          let v,w be Vector of V;

          reconsider v9 = v, w9 = w as Element of K;

          

          thus (x * (v + w)) = (x * (v9 + w9))

          .= ((x * v9) + (x * w9)) by VECTSP_1:def 7

          .= ((x * v) + (x * w));

          

          thus ((x + y) * v) = ((x + y) * v9)

          .= ((x * v9) + (y * v9)) by VECTSP_1:def 7

          .= ((x * v) + (y * v));

          

          thus ((x * y) * v) = ((x * y) * v9)

          .= (x * (y * v9)) by GROUP_1:def 3

          .= (the lmult of V . (x,(y * v)))

          .= (x * (y * v));

          

          thus (( 1. K) * v) = (( 1. K) * v9)

          .= v;

        end;

        hence thesis;

      end;

    end

    registration

      let K be non degenerated non empty doubleLoopStr;

      cluster ( StructVectSp K) -> non trivial;

      coherence ;

    end

    registration

      let K be non degenerated non empty doubleLoopStr;

      cluster non trivial for ModuleStr over K;

      existence

      proof

        take ( StructVectSp K);

        thus thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      cluster add-associative right_zeroed right_complementable strict for non empty ModuleStr over K;

      correctness

      proof

        take ( StructVectSp K);

        thus thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable associative left_unital distributive non empty doubleLoopStr;

      cluster add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital strict for non empty ModuleStr over K;

      correctness

      proof

        take ( StructVectSp K);

        thus thesis;

      end;

    end

    registration

      let K be Abelian add-associative right_zeroed right_complementable associative left_unital distributive non degenerated non empty doubleLoopStr;

      cluster Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital strict for non trivial ModuleStr over K;

      existence

      proof

        take ( StructVectSp K);

        thus thesis;

      end;

    end

    theorem :: VECTSP10:1

    

     Th1: for K be add-associative right_zeroed right_complementable associative left_unital distributive non empty doubleLoopStr, a be Element of K holds for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K, v be Vector of V holds (( 0. K) * v) = ( 0. V) & (a * ( 0. V)) = ( 0. V)

    proof

      let F be add-associative right_zeroed right_complementable associative left_unital distributive non empty doubleLoopStr;

      let x be Element of F;

      let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F, v be Vector of V;

      (v + (( 0. F) * v)) = ((( 1. F) * v) + (( 0. F) * v)) by VECTSP_1:def 17

      .= ((( 1. F) + ( 0. F)) * v) by VECTSP_1:def 15

      .= (( 1. F) * v) by RLVECT_1: 4

      .= v by VECTSP_1:def 17

      .= (v + ( 0. V)) by RLVECT_1: 4;

      hence

       A1: (( 0. F) * v) = ( 0. V) by RLVECT_1: 8;

      

      hence (x * ( 0. V)) = ((x * ( 0. F)) * v) by VECTSP_1:def 16

      .= ( 0. V) by A1;

    end;

    theorem :: VECTSP10:2

    for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V be VectSp of K holds for S,T be Subspace of V, v be Vector of V st (S /\ T) = ( (0). V) & v in S & v in T holds v = ( 0. V)

    proof

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K, S,T be Subspace of V, v be Vector of V;

      assume that

       A1: (S /\ T) = ( (0). V) and

       A2: v in S & v in T;

      v in the carrier of S & v in the carrier of T by A2;

      then v in (the carrier of S /\ the carrier of T) by XBOOLE_0:def 4;

      then v in the carrier of (S /\ T) by VECTSP_5:def 2;

      then v in {( 0. V)} by A1, VECTSP_4:def 3;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: VECTSP10:3

    

     Th3: for K be Field, V be VectSp of K holds for x be object, v be Vector of V holds x in ( Lin {v}) iff ex a be Element of K st x = (a * v)

    proof

      let K be Field, V be VectSp of K, x be object, v be Vector of V;

      thus x in ( Lin {v}) implies ex a be Element of K st x = (a * v)

      proof

        assume x in ( Lin {v});

        then

        consider l be Linear_Combination of {v} such that

         A1: x = ( Sum l) by VECTSP_7: 7;

        ( Sum l) = ((l . v) * v) by VECTSP_6: 17;

        hence thesis by A1;

      end;

      given a be Element of K such that

       A2: x = (a * v);

      deffunc F( set) = ( 0. K);

      consider f be Function of the carrier of V, the carrier of K such that

       A3: (f . v) = a and

       A4: for z be Vector of V st z <> v holds (f . z) = F(z) from FUNCT_2:sch 6;

      reconsider f as Element of ( Funcs (the carrier of V,the carrier of K)) by FUNCT_2: 8;

      now

        let z be Vector of V;

        assume not z in {v};

        then z <> v by TARSKI:def 1;

        hence (f . z) = ( 0. K) by A4;

      end;

      then

      reconsider f as Linear_Combination of V by VECTSP_6:def 1;

      ( Carrier f) c= {v}

      proof

        let x be object;

        assume

         A5: x in ( Carrier f);

        then (f . x) <> ( 0. K) by VECTSP_6: 2;

        then x = v by A4, A5;

        hence thesis by TARSKI:def 1;

      end;

      then

      reconsider f as Linear_Combination of {v} by VECTSP_6:def 4;

      ( Sum f) = x by A2, A3, VECTSP_6: 17;

      hence thesis by VECTSP_7: 7;

    end;

    theorem :: VECTSP10:4

    

     Th4: for K be Field, V be VectSp of K, v be Vector of V, a,b be Scalar of V st v <> ( 0. V) & (a * v) = (b * v) holds a = b

    proof

      let K be Field, V be VectSp of K, v be Vector of V, a,b be Scalar of V such that

       A1: v <> ( 0. V) and

       A2: (a * v) = (b * v);

      ((a * v) - (b * v)) = ( 0. V) by A2, VECTSP_1: 19;

      then ((a - b) * v) = ( 0. V) by VECTSP_4: 82;

      then (a - b) = ( 0. K) by A1, VECTSP_1: 15;

      hence thesis by VECTSP_1: 19;

    end;

    theorem :: VECTSP10:5

    

     Th5: for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr holds for V be VectSp of K holds for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v,v1,v2 be Vector of V st v1 in W1 & v2 in W2 & v = (v1 + v2) holds (v |-- (W1,W2)) = [v1, v2]

    proof

      let K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;

      let W1,W2 be Subspace of V;

      assume

       A1: V is_the_direct_sum_of (W1,W2);

      let v,v1,v2 be Vector of V;

      ( [v1, v2] `1 ) = v1 & ( [v1, v2] `2 ) = v2;

      hence thesis by A1, VECTSP_5:def 6;

    end;

    theorem :: VECTSP10:6

    

     Th6: for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr holds for V be VectSp of K holds for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v,v1,v2 be Vector of V st (v |-- (W1,W2)) = [v1, v2] holds v = (v1 + v2)

    proof

      let K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;

      let W1,W2 be Subspace of V such that

       A1: V is_the_direct_sum_of (W1,W2);

      let v,v1,v2 be Vector of V;

      assume (v |-- (W1,W2)) = [v1, v2];

      then ((v |-- (W1,W2)) `1 ) = v1 & ((v |-- (W1,W2)) `2 ) = v2;

      hence thesis by A1, VECTSP_5:def 6;

    end;

    theorem :: VECTSP10:7

    

     Th7: for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr holds for V be VectSp of K holds for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v,v1,v2 be Vector of V st (v |-- (W1,W2)) = [v1, v2] holds v1 in W1 & v2 in W2

    proof

      let K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;

      let W1,W2 be Subspace of V such that

       A1: V is_the_direct_sum_of (W1,W2);

      let v,v1,v2 be Vector of V;

      assume (v |-- (W1,W2)) = [v1, v2];

      then ((v |-- (W1,W2)) `1 ) = v1 & ((v |-- (W1,W2)) `2 ) = v2;

      hence thesis by A1, VECTSP_5:def 6;

    end;

    theorem :: VECTSP10:8

    

     Th8: for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr holds for V be VectSp of K holds for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v,v1,v2 be Vector of V st (v |-- (W1,W2)) = [v1, v2] holds (v |-- (W2,W1)) = [v2, v1]

    proof

      let K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;

      let W1,W2 be Subspace of V;

      assume

       A1: V is_the_direct_sum_of (W1,W2);

      let v,v1,v2 be Vector of V;

      assume

       A2: (v |-- (W1,W2)) = [v1, v2];

      then

       A3: ((v |-- (W1,W2)) `1 ) = v1;

      then

       A4: v1 in W1 by A1, VECTSP_5:def 6;

      

       A5: ((v |-- (W1,W2)) `2 ) = v2 by A2;

      then

       A6: v2 in W2 by A1, VECTSP_5:def 6;

      v = (v2 + v1) by A1, A3, A5, VECTSP_5:def 6;

      hence thesis by A1, A4, A6, Th5, VECTSP_5: 41;

    end;

    theorem :: VECTSP10:9

    

     Th9: for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr holds for V be VectSp of K holds for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v be Vector of V st v in W1 holds (v |-- (W1,W2)) = [v, ( 0. V)]

    proof

      let K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;

      let W1,W2 be Subspace of V such that

       A1: V is_the_direct_sum_of (W1,W2);

      let v be Vector of V such that

       A2: v in W1;

      ( 0. V) in W2 & (v + ( 0. V)) = v by RLVECT_1: 4, VECTSP_4: 17;

      hence thesis by A1, A2, Th5;

    end;

    theorem :: VECTSP10:10

    

     Th10: for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr holds for V be VectSp of K holds for W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds for v be Vector of V st v in W2 holds (v |-- (W1,W2)) = [( 0. V), v]

    proof

      let K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;

      let W1,W2 be Subspace of V;

      assume

       A1: V is_the_direct_sum_of (W1,W2);

      let v be Vector of V;

      assume v in W2;

      then (v |-- (W2,W1)) = [v, ( 0. V)] by A1, Th9, VECTSP_5: 41;

      hence thesis by A1, Th8, VECTSP_5: 41;

    end;

    theorem :: VECTSP10:11

    

     Th11: for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr holds for V be VectSp of K holds for V1 be Subspace of V, W1 be Subspace of V1, v be Vector of V st v in W1 holds v is Vector of V1

    proof

      let K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;

      let V1 be Subspace of V, W1 be Subspace of V1, v be Vector of V;

      assume v in W1;

      then the carrier of W1 c= the carrier of V1 & v in the carrier of W1 by VECTSP_4:def 2;

      hence thesis;

    end;

    theorem :: VECTSP10:12

    

     Th12: for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr holds for V be VectSp of K holds for V1,V2,W be Subspace of V, W1,W2 be Subspace of W st W1 = V1 & W2 = V2 holds (W1 + W2) = (V1 + V2)

    proof

      let K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;

      let V1,V2,W be Subspace of V, W1,W2 be Subspace of W such that

       A1: W1 = V1 & W2 = V2;

      reconsider W3 = (W1 + W2) as Subspace of V by VECTSP_4: 26;

      now

        let v be Vector of V;

        

         A2: the carrier of W1 c= the carrier of W & the carrier of W2 c= the carrier of W by VECTSP_4:def 2;

        hereby

          assume

           A3: v in W3;

          then

          reconsider w = v as Vector of W by Th11;

          consider w1,w2 be Vector of W such that

           A4: w1 in W1 & w2 in W2 and

           A5: w = (w1 + w2) by A3, VECTSP_5: 1;

          reconsider v1 = w1, v2 = w2 as Vector of V by VECTSP_4: 10;

          v = (v1 + v2) by A5, VECTSP_4: 13;

          hence v in (V1 + V2) by A1, A4, VECTSP_5: 1;

        end;

        assume v in (V1 + V2);

        then

        consider v1,v2 be Vector of V such that

         A6: v1 in V1 & v2 in V2 and

         A7: v = (v1 + v2) by VECTSP_5: 1;

        v1 in the carrier of W1 & v2 in the carrier of W2 by A1, A6;

        then

        reconsider w1 = v1, w2 = v2 as Vector of W by A2;

        v = (w1 + w2) by A7, VECTSP_4: 13;

        hence v in W3 by A1, A6, VECTSP_5: 1;

      end;

      hence thesis by VECTSP_4: 30;

    end;

    theorem :: VECTSP10:13

    

     Th13: for K be Field, V be VectSp of K, W be Subspace of V holds for v be Vector of V, w be Vector of W st v = w holds ( Lin {w}) = ( Lin {v})

    proof

      let K be Field, V be VectSp of K, W be Subspace of V, v be Vector of V, w be Vector of W such that

       A1: v = w;

      reconsider W1 = ( Lin {w}) as Subspace of V by VECTSP_4: 26;

      now

        let u be Vector of V;

        hereby

          assume u in W1;

          then

          consider a be Element of K such that

           A2: u = (a * w) by Th3;

          u = (a * v) by A1, A2, VECTSP_4: 14;

          hence u in ( Lin {v}) by Th3;

        end;

        assume u in ( Lin {v});

        then

        consider a be Element of K such that

         A3: u = (a * v) by Th3;

        u = (a * w) by A1, A3, VECTSP_4: 14;

        hence u in W1 by Th3;

      end;

      hence thesis by VECTSP_4: 30;

    end;

    theorem :: VECTSP10:14

    

     Th14: for K be Field, V be VectSp of K holds for v be Vector of V, X be Subspace of V st not v in X holds for y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & W = X holds (X + ( Lin {v})) is_the_direct_sum_of (W,( Lin {y}))

    proof

      let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V such that

       A1: not v in X;

      let y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v}));

      assume that

       A2: v = y and

       A3: W = X;

      ( Lin {v}) = ( Lin {y}) by A2, Th13;

      hence the ModuleStr of (X + ( Lin {v})) = (W + ( Lin {y})) by A3, Th12;

      assume (W /\ ( Lin {y})) <> ( (0). (X + ( Lin {v})));

      then

      consider z be Vector of (X + ( Lin {v})) such that

       A4: not (z in (W /\ ( Lin {y})) iff z in ( (0). (X + ( Lin {v})))) by VECTSP_4: 30;

      per cases by A4;

        suppose that

         A5: z in (W /\ ( Lin {y})) and

         A6: not z in ( (0). (X + ( Lin {v})));

        z in ( Lin {y}) by A5, VECTSP_5: 3;

        then

        consider a be Element of K such that

         A7: z = (a * y) by Th3;

        

         A8: z in W by A5, VECTSP_5: 3;

        now

          per cases ;

            suppose a = ( 0. K);

            then z = ( 0. (X + ( Lin {v}))) by A7, VECTSP_1: 15;

            hence contradiction by A6, VECTSP_4: 17;

          end;

            suppose

             A9: a <> ( 0. K);

            y = (( 1_ K) * y) by VECTSP_1:def 17

            .= (((a " ) * a) * y) by A9, VECTSP_1:def 10

            .= ((a " ) * (a * y)) by VECTSP_1:def 16;

            hence contradiction by A1, A2, A3, A8, A7, VECTSP_4: 21;

          end;

        end;

        hence contradiction;

      end;

        suppose that

         A10: not z in (W /\ ( Lin {y})) and

         A11: z in ( (0). (X + ( Lin {v})));

        z = ( 0. (X + ( Lin {v}))) by A11, VECTSP_4: 35;

        hence contradiction by A10, VECTSP_4: 17;

      end;

    end;

    theorem :: VECTSP10:15

    

     Th15: for K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & X = W & not v in X holds (y |-- (W,( Lin {y}))) = [( 0. W), y]

    proof

      let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v}));

      assume v = y & X = W & not v in X;

      then y in {y} & (X + ( Lin {v})) is_the_direct_sum_of (W,( Lin {y})) by Th14, TARSKI:def 1;

      then (y |-- (W,( Lin {y}))) = [( 0. (X + ( Lin {v}))), y] by Th10, VECTSP_7: 8;

      hence thesis by VECTSP_4: 11;

    end;

    theorem :: VECTSP10:16

    

     Th16: for K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V holds for y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & X = W & not v in X holds for w be Vector of (X + ( Lin {v})) st w in X holds (w |-- (W,( Lin {y}))) = [w, ( 0. V)]

    proof

      let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) such that

       A1: v = y and

       A2: X = W and

       A3: not v in X;

      

       A4: (X + ( Lin {v})) is_the_direct_sum_of (W,( Lin {y})) by A1, A2, A3, Th14;

      let w be Vector of (X + ( Lin {v}));

      assume w in X;

      then (w |-- (W,( Lin {y}))) = [w, ( 0. (X + ( Lin {v})))] by A2, A4, Th9;

      hence thesis by VECTSP_4: 11;

    end;

    theorem :: VECTSP10:17

    

     Th17: for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K holds for v be Vector of V, W1,W2 be Subspace of V holds ex v1,v2 be Vector of V st (v |-- (W1,W2)) = [v1, v2]

    proof

      let K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;

      let v be Vector of V, W1,W2 be Subspace of V;

      take ((v |-- (W1,W2)) `1 ), ((v |-- (W1,W2)) `2 );

      thus thesis by MCART_1: 21;

    end;

    theorem :: VECTSP10:18

    

     Th18: for K be Field, V be VectSp of K holds for v be Vector of V, X be Subspace of V, y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & X = W & not v in X holds for w be Vector of (X + ( Lin {v})) holds ex x be Vector of X, r be Element of K st (w |-- (W,( Lin {y}))) = [x, (r * v)]

    proof

      let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) such that

       A1: v = y and

       A2: X = W and

       A3: not v in X;

      let w be Vector of (X + ( Lin {v}));

      consider v1,v2 be Vector of (X + ( Lin {v})) such that

       A4: (w |-- (W,( Lin {y}))) = [v1, v2] by Th17;

      

       A5: (X + ( Lin {v})) is_the_direct_sum_of (W,( Lin {y})) by A1, A2, A3, Th14;

      then v1 in W by A4, Th7;

      then

      reconsider x = v1 as Vector of X by A2;

      v2 in ( Lin {y}) by A5, A4, Th7;

      then

      consider r be Element of K such that

       A6: v2 = (r * y) by Th3;

      take x, r;

      thus thesis by A1, A4, A6, VECTSP_4: 14;

    end;

    theorem :: VECTSP10:19

    

     Th19: for K be Field, V be VectSp of K holds for v be Vector of V, X be Subspace of V, y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & X = W & not v in X holds for w1,w2 be Vector of (X + ( Lin {v})), x1,x2 be Vector of X, r1,r2 be Element of K st (w1 |-- (W,( Lin {y}))) = [x1, (r1 * v)] & (w2 |-- (W,( Lin {y}))) = [x2, (r2 * v)] holds ((w1 + w2) |-- (W,( Lin {y}))) = [(x1 + x2), ((r1 + r2) * v)]

    proof

      let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v}));

      assume that

       A1: v = y and

       A2: X = W and

       A3: not v in X;

      

       A4: (X + ( Lin {v})) is_the_direct_sum_of (W,( Lin {y})) by A1, A2, A3, Th14;

      let w1,w2 be Vector of (X + ( Lin {v})), x1,x2 be Vector of X, r1,r2 be Element of K such that

       A5: (w1 |-- (W,( Lin {y}))) = [x1, (r1 * v)] and

       A6: (w2 |-- (W,( Lin {y}))) = [x2, (r2 * v)];

      reconsider y1 = x1, y2 = x2 as Vector of (X + ( Lin {v})) by A2, VECTSP_4: 10;

      

       A7: (r2 * v) = (r2 * y) by A1, VECTSP_4: 14;

      then

       A8: y2 in W by A4, A6, Th7;

      ((r1 + r2) * v) = ((r1 + r2) * y) by A1, VECTSP_4: 14;

      then

       A9: ((r1 + r2) * v) in ( Lin {y}) by Th3;

      reconsider z1 = x1, z2 = x2 as Vector of V by VECTSP_4: 10;

      

       A10: (y1 + y2) = (z1 + z2) by VECTSP_4: 13

      .= (x1 + x2) by VECTSP_4: 13;

      

       A11: (r1 * v) = (r1 * y) by A1, VECTSP_4: 14;

      then y1 in W by A4, A5, Th7;

      then

       A12: (y1 + y2) in W by A8, VECTSP_4: 20;

      

       A13: w2 = (y2 + (r2 * y)) by A4, A6, A7, Th6;

      w1 = (y1 + (r1 * y)) by A4, A5, A11, Th6;

      

      then

       A14: (w1 + w2) = (((y1 + (r1 * y)) + y2) + (r2 * y)) by A13, RLVECT_1:def 3

      .= (((y1 + y2) + (r1 * y)) + (r2 * y)) by RLVECT_1:def 3

      .= ((y1 + y2) + ((r1 * y) + (r2 * y))) by RLVECT_1:def 3

      .= ((y1 + y2) + ((r1 + r2) * y)) by VECTSP_1:def 15;

      ((r1 + r2) * y) = ((r1 + r2) * v) by A1, VECTSP_4: 14;

      hence thesis by A4, A12, A9, A14, A10, Th5;

    end;

    theorem :: VECTSP10:20

    

     Th20: for K be Field, V be VectSp of K holds for v be Vector of V, X be Subspace of V, y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v})) st v = y & X = W & not v in X holds for w be Vector of (X + ( Lin {v})), x be Vector of X, t,r be Element of K st (w |-- (W,( Lin {y}))) = [x, (r * v)] holds ((t * w) |-- (W,( Lin {y}))) = [(t * x), ((t * r) * v)]

    proof

      let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be Vector of (X + ( Lin {v})), W be Subspace of (X + ( Lin {v}));

      assume that

       A1: v = y and

       A2: X = W and

       A3: not v in X;

      

       A4: (X + ( Lin {v})) is_the_direct_sum_of (W,( Lin {y})) by A1, A2, A3, Th14;

      let w be Vector of (X + ( Lin {v})), x be Vector of X, t,r be Element of K such that

       A5: (w |-- (W,( Lin {y}))) = [x, (r * v)];

      reconsider z = x as Vector of (X + ( Lin {v})) by A2, VECTSP_4: 10;

      (r * y) = (r * v) by A1, VECTSP_4: 14;

      

      then

       A6: (t * w) = (t * (z + (r * y))) by A4, A5, Th6

      .= ((t * z) + (t * (r * y))) by VECTSP_1:def 14

      .= ((t * z) + ((t * r) * y)) by VECTSP_1:def 16;

      reconsider u = x as Vector of V by VECTSP_4: 10;

      

       A7: ((t * r) * y) in ( Lin {y}) by Th3;

      

       A8: ((t * r) * y) = ((t * r) * v) by A1, VECTSP_4: 14;

      

       A9: (t * z) = (t * u) by VECTSP_4: 14

      .= (t * x) by VECTSP_4: 14;

      then (t * z) in W by A2;

      hence thesis by A4, A9, A8, A7, A6, Th5;

    end;

    begin

    definition

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K;

      let W be Subspace of V;

      :: VECTSP10:def2

      func CosetSet (V,W) -> non empty Subset-Family of V equals the set of all A where A be Coset of W;

      correctness

      proof

        set C = the set of all A where A be Coset of W;

        

         A1: C c= ( bool the carrier of V)

        proof

          let x be object;

          assume x in C;

          then ex A be Coset of W st A = x;

          hence thesis;

        end;

        the carrier of W is Coset of W by VECTSP_4: 73;

        then the carrier of W in C;

        hence thesis by A1;

      end;

    end

    definition

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K;

      let W be Subspace of V;

      :: VECTSP10:def3

      func addCoset (V,W) -> BinOp of ( CosetSet (V,W)) means

      : Def3: for A,B be Element of ( CosetSet (V,W)) holds for a,b be Vector of V st A = (a + W) & B = (b + W) holds (it . (A,B)) = ((a + b) + W);

      existence

      proof

        defpred P[ set, set, set] means for a,b be Vector of V st $1 = (a + W) & $2 = (b + W) holds $3 = ((a + b) + W);

        set C = ( CosetSet (V,W));

         A1:

        now

          let A,B be Element of C;

          A in C;

          then

          consider A1 be Coset of W such that

           A2: A1 = A;

          consider a be Vector of V such that

           A3: A1 = (a + W) by VECTSP_4:def 6;

          B in C;

          then

          consider B1 be Coset of W such that

           A4: B1 = B;

          consider b be Vector of V such that

           A5: B1 = (b + W) by VECTSP_4:def 6;

          reconsider z = ((a + b) + W) as Coset of W by VECTSP_4:def 6;

          z in C;

          then

          reconsider z as Element of C;

          take z;

          thus P[A, B, z]

          proof

            let a1,b1 be Vector of V;

            assume that

             A6: A = (a1 + W) and

             A7: B = (b1 + W);

            a1 in (a + W) by A2, A3, A6, VECTSP_4: 44;

            then

            consider w1 be Vector of V such that

             A8: w1 in W and

             A9: a1 = (a + w1) by VECTSP_4: 42;

            b1 in (b + W) by A4, A5, A7, VECTSP_4: 44;

            then

            consider w2 be Vector of V such that

             A10: w2 in W and

             A11: b1 = (b + w2) by VECTSP_4: 42;

            

             A12: (w1 + w2) in W by A8, A10, VECTSP_4: 20;

            (a1 + b1) = (((w1 + a) + b) + w2) by A9, A11, RLVECT_1:def 3

            .= ((w1 + (a + b)) + w2) by RLVECT_1:def 3

            .= ((a + b) + (w1 + w2)) by RLVECT_1:def 3;

            then

             A13: (a1 + b1) in ((a + b) + W) by A12;

            (a1 + b1) in ((a1 + b1) + W) by VECTSP_4: 44;

            hence thesis by A13, VECTSP_4: 56;

          end;

        end;

        consider f be Function of [:C, C:], C such that

         A14: for A,B be Element of C holds P[A, B, (f . (A,B))] from BINOP_1:sch 3( A1);

        reconsider f as BinOp of C;

        take f;

        let A,B be Element of C;

        let a,b be Vector of V;

        assume A = (a + W) & B = (b + W);

        hence thesis by A14;

      end;

      uniqueness

      proof

        set C = ( CosetSet (V,W));

        let f1,f2 be BinOp of ( CosetSet (V,W)) such that

         A15: for A,B be Element of ( CosetSet (V,W)) holds for a,b be Vector of V st A = (a + W) & B = (b + W) holds (f1 . (A,B)) = ((a + b) + W) and

         A16: for A,B be Element of ( CosetSet (V,W)) holds for a,b be Vector of V st A = (a + W) & B = (b + W) holds (f2 . (A,B)) = ((a + b) + W);

        now

          let A,B be Element of ( CosetSet (V,W));

          A in C;

          then

          consider A1 be Coset of W such that

           A17: A1 = A;

          consider a be Vector of V such that

           A18: A1 = (a + W) by VECTSP_4:def 6;

          B in C;

          then

          consider B1 be Coset of W such that

           A19: B1 = B;

          consider b be Vector of V such that

           A20: B1 = (b + W) by VECTSP_4:def 6;

          

          thus (f1 . (A,B)) = ((a + b) + W) by A15, A17, A19, A18, A20

          .= (f2 . (A,B)) by A16, A17, A19, A18, A20;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K;

      let W be Subspace of V;

      :: VECTSP10:def4

      func zeroCoset (V,W) -> Element of ( CosetSet (V,W)) equals the carrier of W;

      coherence

      proof

        the carrier of W = (( 0. V) + W) by VECTSP_4: 45;

        then the carrier of W is Coset of W by VECTSP_4:def 6;

        then the carrier of W in ( CosetSet (V,W));

        hence thesis;

      end;

    end

    definition

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K;

      let W be Subspace of V;

      :: VECTSP10:def5

      func lmultCoset (V,W) -> Function of [:the carrier of K, ( CosetSet (V,W)):], ( CosetSet (V,W)) means

      : Def5: for z be Element of K, A be Element of ( CosetSet (V,W)) holds for a be Vector of V st A = (a + W) holds (it . (z,A)) = ((z * a) + W);

      existence

      proof

        defpred P[ Element of K, set, set] means for a be Vector of V st $2 = (a + W) holds $3 = (($1 * a) + W);

        set cF = the carrier of K;

        set C = ( CosetSet (V,W));

         A1:

        now

          let z be Element of K;

          let A be Element of C;

          A in C;

          then

          consider A1 be Coset of W such that

           A2: A1 = A;

          consider a be Vector of V such that

           A3: A1 = (a + W) by VECTSP_4:def 6;

          reconsider c = ((z * a) + W) as Coset of W by VECTSP_4:def 6;

          c in C;

          then

          reconsider c as Element of C;

          take c;

          thus P[z, A, c]

          proof

            let a1 be Vector of V;

            assume A = (a1 + W);

            then a1 in (a + W) by A2, A3, VECTSP_4: 44;

            then

            consider w1 be Vector of V such that

             A4: w1 in W & a1 = (a + w1) by VECTSP_4: 42;

            (z * a1) = ((z * a) + (z * w1)) & (z * w1) in W by A4, VECTSP_1:def 14, VECTSP_4: 21;

            then

             A5: (z * a1) in ((z * a) + W);

            (z * a1) in ((z * a1) + W) by VECTSP_4: 44;

            hence thesis by A5, VECTSP_4: 56;

          end;

        end;

        consider f be Function of [:cF, C:], C such that

         A6: for z be Element of K holds for A be Element of C holds P[z, A, (f . (z,A))] from BINOP_1:sch 3( A1);

        take f;

        let z be Element of K, A be Element of C, a be Vector of V;

        assume A = (a + W);

        hence thesis by A6;

      end;

      uniqueness

      proof

        set cF = the carrier of K;

        set C = ( CosetSet (V,W));

        let f1,f2 be Function of [:cF, C:], C such that

         A7: for z be Element of K, A be Element of ( CosetSet (V,W)) holds for a be Vector of V st A = (a + W) holds (f1 . (z,A)) = ((z * a) + W) and

         A8: for z be Element of K, A be Element of ( CosetSet (V,W)) holds for a be Vector of V st A = (a + W) holds (f2 . (z,A)) = ((z * a) + W);

        set C = ( CosetSet (V,W));

        now

          let z be Element of K;

          let A be Element of ( CosetSet (V,W));

          A in C;

          then

          consider A1 be Coset of W such that

           A9: A1 = A;

          consider a be Vector of V such that

           A10: A1 = (a + W) by VECTSP_4:def 6;

          

          thus (f1 . (z,A)) = ((z * a) + W) by A7, A9, A10

          .= (f2 . (z,A)) by A8, A9, A10;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K;

      let W be Subspace of V;

      :: VECTSP10:def6

      func VectQuot (V,W) -> strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K means

      : Def6: the carrier of it = ( CosetSet (V,W)) & the addF of it = ( addCoset (V,W)) & ( 0. it ) = ( zeroCoset (V,W)) & the lmult of it = ( lmultCoset (V,W));

      existence

      proof

        set C = ( CosetSet (V,W)), aC = ( addCoset (V,W)), zC = ( zeroCoset (V,W)), lC = ( lmultCoset (V,W)), A = ModuleStr (# C, aC, zC, lC #);

        

         A1: A is right_zeroed

        proof

          let A1 be Element of A;

          A1 in C;

          then

          consider aa be Coset of W such that

           A2: A1 = aa;

          consider a be Vector of V such that

           A3: aa = (a + W) by VECTSP_4:def 6;

          ( 0. A) = (( 0. V) + W) by VECTSP_4: 45;

          

          hence (A1 + ( 0. A)) = ((a + ( 0. V)) + W) by A2, A3, Def3

          .= A1 by A2, A3, RLVECT_1: 4;

        end;

        

         A4: A is right_complementable

        proof

          let A1 be Element of A;

          

           A5: ( 0. A) = (( 0. V) + W) by VECTSP_4: 45;

          A1 in C;

          then

          consider aa be Coset of W such that

           A6: A1 = aa;

          consider a be Vector of V such that

           A7: aa = (a + W) by VECTSP_4:def 6;

          set A2 = (( - a) + W);

          A2 is Coset of W by VECTSP_4:def 6;

          then A2 in C;

          then

          reconsider A2 as Element of A;

          take A2;

          

          thus (A1 + A2) = ((a + ( - a)) + W) by A6, A7, Def3

          .= ( 0. A) by A5, RLVECT_1: 5;

        end;

         A8:

        now

          let x,y be Element of K;

          let A1,A2 be Element of A;

          A1 in C;

          then

          consider aa be Coset of W such that

           A9: A1 = aa;

          A2 in C;

          then

          consider bb be Coset of W such that

           A10: A2 = bb;

          consider b be Vector of V such that

           A11: bb = (b + W) by VECTSP_4:def 6;

          

           A12: (lC . (x,A2)) = (x * A2) & (lC . (x,A2)) = ((x * b) + W) by A10, A11, Def5;

          consider a be Vector of V such that

           A13: aa = (a + W) by VECTSP_4:def 6;

          

           A14: (aC . (A1,A2)) = ((a + b) + W) by A9, A10, A13, A11, Def3;

          

           A15: (lC . (x,A1)) = ((x * a) + W) by A9, A13, Def5;

          

          thus (x * (A1 + A2)) = (lC . (x,(the addF of A . (A1,A2))))

          .= ((x * (a + b)) + W) by A14, Def5

          .= (((x * a) + (x * b)) + W) by VECTSP_1:def 14

          .= ((x * A1) + (x * A2)) by A15, A12, Def3;

          

           A16: (lC . (y,A1)) = ((y * a) + W) by A9, A13, Def5;

          

          thus ((x + y) * A1) = (the lmult of A . ((x + y),A1))

          .= (((x + y) * a) + W) by A9, A13, Def5

          .= (((x * a) + (y * a)) + W) by VECTSP_1:def 15

          .= ((x * A1) + (y * A1)) by A15, A16, Def3;

          

          thus ((x * y) * A1) = (the lmult of A . ((x * y),A1))

          .= (((x * y) * a) + W) by A9, A13, Def5

          .= ((x * (y * a)) + W) by VECTSP_1:def 16

          .= (lC . (x,(y * A1))) by A16, Def5

          .= (x * (y * A1));

          

          thus (( 1_ K) * A1) = (the lmult of A . (( 1_ K),A1))

          .= ((( 1_ K) * a) + W) by A9, A13, Def5

          .= A1 by A9, A13, VECTSP_1:def 17;

        end;

        

         A17: A is Abelian

        proof

          let A1,A2 be Element of A;

          A1 in C;

          then

          consider aa be Coset of W such that

           A18: A1 = aa;

          consider a be Vector of V such that

           A19: aa = (a + W) by VECTSP_4:def 6;

          A2 in C;

          then

          consider bb be Coset of W such that

           A20: A2 = bb;

          consider b be Vector of V such that

           A21: bb = (b + W) by VECTSP_4:def 6;

          

          thus (A1 + A2) = ((a + b) + W) by A18, A20, A19, A21, Def3

          .= (A2 + A1) by A18, A20, A19, A21, Def3;

        end;

        A is add-associative

        proof

          let A1,A2,A3 be Element of A;

          A1 in C;

          then

          consider aa be Coset of W such that

           A22: A1 = aa;

          consider a be Vector of V such that

           A23: aa = (a + W) by VECTSP_4:def 6;

          A2 in C;

          then

          consider bb be Coset of W such that

           A24: A2 = bb;

          consider b be Vector of V such that

           A25: bb = (b + W) by VECTSP_4:def 6;

          A3 in C;

          then

          consider cc be Coset of W such that

           A26: A3 = cc;

          consider c be Vector of V such that

           A27: cc = (c + W) by VECTSP_4:def 6;

          

           A28: (aC . (A2,A3)) = ((b + c) + W) by A24, A26, A25, A27, Def3;

          (aC . (A1,A2)) = ((a + b) + W) by A22, A24, A23, A25, Def3;

          

          hence ((A1 + A2) + A3) = (((a + b) + c) + W) by A26, A27, Def3

          .= ((a + (b + c)) + W) by RLVECT_1:def 3

          .= (A1 + (A2 + A3)) by A22, A23, A28, Def3;

        end;

        then

        reconsider A as strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K by A17, A1, A4, A8, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

        take A;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: VECTSP10:21

    

     Th21: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V holds ( zeroCoset (V,W)) = (( 0. V) + W) & ( 0. ( VectQuot (V,W))) = ( zeroCoset (V,W))

    proof

      let F be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of F;

      let W be Subspace of V;

      ( 0. V) = ( 0. W) & ( 0. W) in W by VECTSP_4: 11;

      hence ( zeroCoset (V,W)) = (( 0. V) + W) by VECTSP_4: 49;

      thus thesis by Def6;

    end;

    theorem :: VECTSP10:22

    

     Th22: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V be VectSp of K, W be Subspace of V, w be Vector of ( VectQuot (V,W)) holds w is Coset of W & ex v be Vector of V st w = (v + W)

    proof

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V, w be Vector of ( VectQuot (V,W));

      set qv = ( VectQuot (V,W)), cs = ( CosetSet (V,W));

      cs = the carrier of qv by Def6;

      then w in the set of all A where A be Coset of W;

      then ex A be Coset of W st A = w;

      hence thesis by VECTSP_4:def 6;

    end;

    theorem :: VECTSP10:23

    

     Th23: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V be VectSp of K, W be Subspace of V, v be Vector of V holds (v + W) is Coset of W & (v + W) is Vector of ( VectQuot (V,W))

    proof

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V, v be Vector of V;

      set cs = ( CosetSet (V,W));

      thus (v + W) is Coset of W by VECTSP_4:def 6;

      then (v + W) in cs;

      hence thesis by Def6;

    end;

    theorem :: VECTSP10:24

    for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V be VectSp of K, W be Subspace of V, A be Coset of W holds A is Vector of ( VectQuot (V,W))

    proof

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V, A be Coset of W;

      set cs = ( CosetSet (V,W));

      A in cs;

      hence thesis by Def6;

    end;

    theorem :: VECTSP10:25

    for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V holds for A be Vector of ( VectQuot (V,W)), v be Vector of V, a be Scalar of V st A = (v + W) holds (a * A) = ((a * v) + W)

    proof

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V;

      set vw = ( VectQuot (V,W)), lm = the lmult of vw;

      let A be Vector of vw, v be Vector of V, a be Scalar of V;

      assume

       A1: A = (v + W);

      A is Coset of W by Th22;

      then A in the set of all B where B be Coset of W;

      then

      reconsider w = A as Element of ( CosetSet (V,W));

      

      thus (a * A) = (lm . (a,A))

      .= (( lmultCoset (V,W)) . (a,w)) by Def6

      .= ((a * v) + W) by A1, Def5;

    end;

    theorem :: VECTSP10:26

    for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V holds for A1,A2 be Vector of ( VectQuot (V,W)), v1,v2 be Vector of V st A1 = (v1 + W) & A2 = (v2 + W) holds (A1 + A2) = ((v1 + v2) + W)

    proof

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V;

      set vw = ( VectQuot (V,W));

      let A1,A2 be Vector of vw, v1,v2 be Vector of V;

      assume

       A1: A1 = (v1 + W) & A2 = (v2 + W);

      A2 is Coset of W by Th22;

      then

       A2: A2 in the set of all B where B be Coset of W;

      A1 is Coset of W by Th22;

      then A1 in the set of all B where B be Coset of W;

      then

      reconsider w1 = A1, w2 = A2 as Element of ( CosetSet (V,W)) by A2;

      

      thus (A1 + A2) = (( addCoset (V,W)) . (w1,w2)) by Def6

      .= ((v1 + v2) + W) by A1, Def3;

    end;

    begin

    theorem :: VECTSP10:27

    

     Th27: for K be Field, V be VectSp of K holds for X be Subspace of V, fi be linear-Functional of X, v be Vector of V, y be Vector of (X + ( Lin {v})) st v = y & not v in X holds for r be Element of K holds ex psi be linear-Functional of (X + ( Lin {v})) st (psi | the carrier of X) = fi & (psi . y) = r

    proof

      let K be Field, V be VectSp of K, X be Subspace of V, fi be linear-Functional of X, v be Vector of V, y be Vector of (X + ( Lin {v}));

      assume that

       A1: v = y and

       A2: not v in X;

      reconsider W1 = X as Subspace of (X + ( Lin {v})) by VECTSP_5: 7;

      let r be Element of K;

      defpred P[ Element of (X + ( Lin {v})), Element of K] means for x be Vector of X, s be Element of K st (($1 |-- (W1,( Lin {y}))) `1 ) = x & (($1 |-- (W1,( Lin {y}))) `2 ) = (s * v) holds $2 = ((fi . x) + (s * r));

      

       A3: for e be Element of (X + ( Lin {v})) holds ex a be Element of K st P[e, a]

      proof

        let e be Element of (X + ( Lin {v}));

        consider x be Vector of X, s be Element of K such that

         A4: (e |-- (W1,( Lin {y}))) = [x, (s * v)] by A1, A2, Th18;

        take ((fi . x) + (s * r));

        let x9 be Vector of X, t be Element of K such that

         A5: ((e |-- (W1,( Lin {y}))) `1 ) = x9 and

         A6: ((e |-- (W1,( Lin {y}))) `2 ) = (t * v);

        v <> ( 0. V) by A2, VECTSP_4: 17;

        then t = s by A4, A6, Th4;

        hence thesis by A4, A5;

      end;

      consider f be Function of the carrier of (X + ( Lin {v})), the carrier of K such that

       A7: for e be Element of (X + ( Lin {v})) holds P[e, (f . e)] from FUNCT_2:sch 3( A3);

       A8:

      now

        let a be object;

        assume a in ( dom fi);

        then

        reconsider x = a as Vector of X;

        X is Subspace of (X + ( Lin {v})) by VECTSP_5: 7;

        then the carrier of X c= the carrier of (X + ( Lin {v})) by VECTSP_4:def 2;

        then

        reconsider v1 = x as Vector of (X + ( Lin {v}));

        v1 in X;

        

        then (v1 |-- (W1,( Lin {y}))) = [v1, ( 0. V)] by A1, A2, Th16

        .= [v1, (( 0. K) * v)] by Th1;

        then

         A9: ((v1 |-- (W1,( Lin {y}))) `1 ) = x & ((v1 |-- (W1,( Lin {y}))) `2 ) = (( 0. K) * v);

        

        thus (fi . a) = ((fi . x) + ( 0. K)) by RLVECT_1: 4

        .= ((fi . x) + (( 0. K) * r))

        .= (f . a) by A7, A9;

      end;

      reconsider f as Functional of (X + ( Lin {v}));

      

       A10: (y |-- (W1,( Lin {y}))) = [( 0. W1), y] by A1, A2, Th15;

      then

       A11: ((y |-- (W1,( Lin {y}))) `1 ) = ( 0. X);

      

       A12: f is additive

      proof

        let v1,v2 be Vector of (X + ( Lin {v}));

        consider x1 be Vector of X, s1 be Element of K such that

         A13: (v1 |-- (W1,( Lin {y}))) = [x1, (s1 * v)] by A1, A2, Th18;

        

         A14: ((v1 |-- (W1,( Lin {y}))) `1 ) = x1 & ((v1 |-- (W1,( Lin {y}))) `2 ) = (s1 * v) by A13;

        consider x2 be Vector of X, s2 be Element of K such that

         A15: (v2 |-- (W1,( Lin {y}))) = [x2, (s2 * v)] by A1, A2, Th18;

        

         A16: ((v2 |-- (W1,( Lin {y}))) `1 ) = x2 & ((v2 |-- (W1,( Lin {y}))) `2 ) = (s2 * v) by A15;

        ((v1 + v2) |-- (W1,( Lin {y}))) = [(x1 + x2), ((s1 + s2) * v)] by A1, A2, A13, A15, Th19;

        then (((v1 + v2) |-- (W1,( Lin {y}))) `1 ) = (x1 + x2) & (((v1 + v2) |-- (W1,( Lin {y}))) `2 ) = ((s1 + s2) * v);

        

        hence (f . (v1 + v2)) = ((fi . (x1 + x2)) + ((s1 + s2) * r)) by A7

        .= ((fi . (x1 + x2)) + ((s1 * r) + (s2 * r))) by VECTSP_1:def 3

        .= (((fi . x1) + (fi . x2)) + ((s1 * r) + (s2 * r))) by VECTSP_1:def 20

        .= ((((fi . x1) + (fi . x2)) + (s1 * r)) + (s2 * r)) by RLVECT_1:def 3

        .= ((((fi . x1) + (s1 * r)) + (fi . x2)) + (s2 * r)) by RLVECT_1:def 3

        .= (((fi . x1) + (s1 * r)) + ((fi . x2) + (s2 * r))) by RLVECT_1:def 3

        .= ((f . v1) + ((fi . x2) + (s2 * r))) by A7, A14

        .= ((f . v1) + (f . v2)) by A7, A16;

      end;

      f is homogeneous

      proof

        let v0 be Vector of (X + ( Lin {v})), t be Element of K;

        consider x0 be Vector of X, s0 be Element of K such that

         A17: (v0 |-- (W1,( Lin {y}))) = [x0, (s0 * v)] by A1, A2, Th18;

        

         A18: ((v0 |-- (W1,( Lin {y}))) `1 ) = x0 & ((v0 |-- (W1,( Lin {y}))) `2 ) = (s0 * v) by A17;

        ((t * v0) |-- (W1,( Lin {y}))) = [(t * x0), ((t * s0) * v)] by A1, A2, A17, Th20;

        then (((t * v0) |-- (W1,( Lin {y}))) `1 ) = (t * x0) & (((t * v0) |-- (W1,( Lin {y}))) `2 ) = ((t * s0) * v);

        

        hence (f . (t * v0)) = ((fi . (t * x0)) + ((t * s0) * r)) by A7

        .= ((t * (fi . x0)) + ((t * s0) * r)) by HAHNBAN1:def 8

        .= ((t * (fi . x0)) + (t * (s0 * r))) by GROUP_1:def 3

        .= (t * ((fi . x0) + (s0 * r))) by VECTSP_1:def 2

        .= (t * (f . v0)) by A7, A18;

      end;

      then

      reconsider f as linear-Functional of (X + ( Lin {v})) by A12;

      take f;

      

       A19: ( dom fi) = the carrier of X by FUNCT_2:def 1;

      ( dom f) = the carrier of (X + ( Lin {v})) & X is Subspace of (X + ( Lin {v})) by FUNCT_2:def 1, VECTSP_5: 7;

      then ( dom fi) c= ( dom f) by A19, VECTSP_4:def 2;

      then ( dom fi) = (( dom f) /\ the carrier of X) by A19, XBOOLE_1: 28;

      hence (f | the carrier of X) = fi by A8, FUNCT_1: 46;

      ((y |-- (W1,( Lin {y}))) `2 ) = y by A10

      .= (( 1_ K) * v) by A1, VECTSP_1:def 17;

      

      hence (f . y) = ((fi . ( 0. X)) + (( 1_ K) * r)) by A7, A11

      .= (( 0. K) + (( 1_ K) * r)) by HAHNBAN1:def 9

      .= (( 0. K) + r)

      .= r by RLVECT_1: 4;

    end;

    registration

      let K be right_zeroed non empty addLoopStr;

      let V be non empty ModuleStr over K;

      cluster additive 0-preserving for Functional of V;

      existence

      proof

        take ( 0Functional V);

        thus thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let V be right_zeroed non empty ModuleStr over K;

      cluster additive -> 0-preserving for Functional of V;

      coherence

      proof

        let f be Functional of V;

        assume

         A1: f is additive;

        (f . ( 0. V)) = (f . (( 0. V) + ( 0. V))) by RLVECT_1:def 4

        .= ((f . ( 0. V)) + (f . ( 0. V))) by A1;

        hence (f . ( 0. V)) = ( 0. K) by RLVECT_1: 9;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K;

      cluster homogeneous -> 0-preserving for Functional of V;

      coherence

      proof

        let f be Functional of V;

        assume

         A1: f is homogeneous;

        

        thus (f . ( 0. V)) = (f . (( 0. K) * ( 0. V))) by Th1

        .= (( 0. K) * (f . ( 0. V))) by A1

        .= ( 0. K);

      end;

    end

    registration

      let K be non empty ZeroStr;

      let V be non empty ModuleStr over K;

      cluster ( 0Functional V) -> constant;

      coherence

      proof

        let x,y be object;

        set f = ( 0Functional V);

        assume x in ( dom f) & y in ( dom f);

        then

        reconsider v = x, w = y as Vector of V;

        

        thus (f . x) = (f . v)

        .= ( 0. K) by HAHNBAN1: 14

        .= (f . w) by HAHNBAN1: 14

        .= (f . y);

      end;

    end

    registration

      let K be non empty ZeroStr;

      let V be non empty ModuleStr over K;

      cluster constant for Functional of V;

      existence

      proof

        take ( 0Functional V);

        thus thesis;

      end;

    end

    definition

      let K be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let V be right_zeroed non empty ModuleStr over K;

      let f be 0-preserving Functional of V;

      :: original: constant

      redefine

      :: VECTSP10:def7

      attr f is constant means f = ( 0Functional V);

      compatibility

      proof

        

         A1: (f . ( 0. V)) = ( 0. K) & the carrier of V = ( dom f) by FUNCT_2:def 1, HAHNBAN1:def 9;

        hereby

          assume

           A2: f is constant;

          now

            let v be Vector of V;

            

            thus (f . v) = ( 0. K) by A1, A2

            .= (( 0Functional V) . v) by HAHNBAN1: 14;

          end;

          hence f = ( 0Functional V) by FUNCT_2: 63;

        end;

        assume

         A3: f = ( 0Functional V);

        now

          let x,y be object;

          assume x in ( dom f) & y in ( dom f);

          then

          reconsider v = x, w = y as Vector of V;

          

          thus (f . x) = (( 0Functional V) . v) by A3

          .= ( 0. K) by HAHNBAN1: 14

          .= (( 0Functional V) . w) by HAHNBAN1: 14

          .= (f . y) by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let V be right_zeroed non empty ModuleStr over K;

      cluster constant additive 0-preserving for Functional of V;

      existence

      proof

        take ( 0Functional V);

        thus thesis;

      end;

    end

    registration

      let K be Field;

      let V be non trivial VectSp of K;

      cluster additive homogeneous non constant non trivial for Functional of V;

      existence

      proof

        consider v be Vector of V such that

         A1: v <> ( 0. V) by STRUCT_0:def 18;

        set W = the Linear_Compl of ( Lin {v} qua Subset of V);

        

         A2: V is_the_direct_sum_of (W,( Lin {v})) by VECTSP_5:def 5;

        then

         A3: the ModuleStr of V = (W + ( Lin {v}));

        then

        reconsider y = v as Vector of (W + ( Lin {v}));

        

         A4: (W /\ ( Lin {v})) = ( (0). V) by A2;

        now

          v in {v} by TARSKI:def 1;

          then v in ( Lin {v}) by VECTSP_7: 8;

          then

           A5: v in the carrier of ( Lin {v});

          assume v in W;

          then v in the carrier of W;

          then v in (the carrier of W /\ the carrier of ( Lin {v})) by A5, XBOOLE_0:def 4;

          then v in the carrier of (W /\ ( Lin {v})) by VECTSP_5:def 2;

          then v in {( 0. V)} by A4, VECTSP_4:def 3;

          hence contradiction by A1, TARSKI:def 1;

        end;

        then

        consider psi be linear-Functional of (W + ( Lin {v})) such that (psi | the carrier of W) = ( 0Functional W) and

         A6: (psi . y) = ( 1_ K) by Th27;

        reconsider f = psi as Functional of V by A3;

        take f;

        thus f is additive

        proof

          let v1,v2 be Vector of V;

          reconsider w1 = v1, w2 = v2 as Vector of (W + ( Lin {v})) by A3;

          (v1 + v2) = (w1 + w2) by A3;

          hence thesis by VECTSP_1:def 20;

        end;

        thus f is homogeneous

        proof

          let v1 be Vector of V, a be Element of K;

          reconsider w1 = v1 as Vector of (W + ( Lin {v})) by A3;

          (a * v1) = (the lmult of (W + ( Lin {v})) . (a,w1)) by A3

          .= (a * w1);

          hence thesis by HAHNBAN1:def 8;

        end;

        then

        reconsider f1 = f as homogeneous Functional of V;

        thus f is non constant

        proof

          

           A7: the carrier of V = ( dom f) & (f1 . ( 0. V)) = ( 0. K) by FUNCT_2:def 1, HAHNBAN1:def 9;

          assume f is constant;

          hence contradiction by A6, A7;

        end;

        thus f is non trivial

        proof

          set x = [v, ( 1_ K)], y = [( 0. V), ( 0. K)];

          

           A8: the carrier of V = ( dom f) by FUNCT_2:def 1;

          then

           A9: x in f by A6, FUNCT_1: 1;

          (f1 . ( 0. V)) = ( 0. K) by HAHNBAN1:def 9;

          then

           A10: y in f by A8, FUNCT_1: 1;

          assume

           A11: f is trivial;

          per cases by A11, ZFMISC_1: 131;

            suppose f = {} ;

            hence contradiction;

          end;

            suppose ex z be object st f = {z};

            then

            consider z be object such that

             A12: f = {z};

            z = x & z = y by A9, A10, A12, TARSKI:def 1;

            hence contradiction by XTUPLE_0: 1;

          end;

        end;

      end;

    end

    registration

      let K be Field;

      let V be non trivial VectSp of K;

      cluster trivial -> constant for Functional of V;

      coherence ;

    end

    definition

      let K be Field;

      let V be non trivial VectSp of K;

      let v be Vector of V;

      let W be Linear_Compl of ( Lin {v});

      assume

       A1: v <> ( 0. V);

      :: VECTSP10:def8

      func coeffFunctional (v,W) -> non constant non trivial linear-Functional of V means

      : Def8: (it . v) = ( 1_ K) & (it | the carrier of W) = ( 0Functional W);

      existence

      proof

        

         A2: V is_the_direct_sum_of (W,( Lin {v})) by VECTSP_5:def 5;

        then

         A3: the ModuleStr of V = (W + ( Lin {v}));

        then

        reconsider y = v as Vector of (W + ( Lin {v}));

        

         A4: (W /\ ( Lin {v})) = ( (0). V) by A2;

        now

          v in {v} by TARSKI:def 1;

          then v in ( Lin {v}) by VECTSP_7: 8;

          then

           A5: v in the carrier of ( Lin {v});

          assume v in W;

          then v in the carrier of W;

          then v in (the carrier of W /\ the carrier of ( Lin {v})) by A5, XBOOLE_0:def 4;

          then v in the carrier of (W /\ ( Lin {v})) by VECTSP_5:def 2;

          then v in {( 0. V)} by A4, VECTSP_4:def 3;

          hence contradiction by A1, TARSKI:def 1;

        end;

        then

        consider psi be linear-Functional of (W + ( Lin {v})) such that

         A6: (psi | the carrier of W) = ( 0Functional W) and

         A7: (psi . y) = ( 1_ K) by Th27;

        reconsider f = psi as Functional of V by A3;

        

         A8: f is additive

        proof

          let v1,v2 be Vector of V;

          reconsider w1 = v1, w2 = v2 as Vector of (W + ( Lin {v})) by A3;

          (v1 + v2) = (w1 + w2) by A3;

          hence thesis by VECTSP_1:def 20;

        end;

        f is homogeneous

        proof

          let v1 be Vector of V, a be Element of K;

          reconsider w1 = v1 as Vector of (W + ( Lin {v})) by A3;

          (a * v1) = (the lmult of (W + ( Lin {v})) . (a,w1)) by A3

          .= (a * w1);

          hence thesis by HAHNBAN1:def 8;

        end;

        then

        reconsider f as linear-Functional of V by A8;

        f is non constant

        proof

          

           A9: the carrier of V = ( dom f) & (f . ( 0. V)) = ( 0. K) by FUNCT_2:def 1, HAHNBAN1:def 9;

          assume f is constant;

          hence contradiction by A7, A9;

        end;

        then

        reconsider f as non constant non trivial linear-Functional of V;

        take f;

        thus thesis by A6, A7;

      end;

      uniqueness

      proof

        let f1,f2 be non constant non trivial linear-Functional of V such that

         A10: (f1 . v) = ( 1_ K) and

         A11: (f1 | the carrier of W) = ( 0Functional W) and

         A12: (f2 . v) = ( 1_ K) and

         A13: (f2 | the carrier of W) = ( 0Functional W);

        V is_the_direct_sum_of (W,( Lin {v})) by VECTSP_5:def 5;

        then

         A14: the ModuleStr of V = (W + ( Lin {v}));

        now

          let w be Vector of V;

          w in (W + ( Lin {v})) by A14;

          then

          consider v1,v2 be Vector of V such that

           A15: v1 in W and

           A16: v2 in ( Lin {v}) and

           A17: w = (v1 + v2) by VECTSP_5: 1;

          consider a be Element of K such that

           A18: v2 = (a * v) by A16, Th3;

          

           A19: v1 in the carrier of W by A15;

          

          then

           A20: (f1 . v1) = ((f2 | the carrier of W) . v1) by A11, A13, FUNCT_1: 49

          .= (f2 . v1) by A19, FUNCT_1: 49;

          

          thus (f1 . w) = ((f1 . v1) + (f1 . (a * v))) by A17, A18, VECTSP_1:def 20

          .= ((f1 . v1) + (a * (f1 . v))) by HAHNBAN1:def 8

          .= ((f1 . v1) + (f2 . (a * v))) by A10, A12, HAHNBAN1:def 8

          .= (f2 . w) by A17, A18, A20, VECTSP_1:def 20;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: VECTSP10:28

    

     Th28: for K be Field, V be non trivial VectSp of K holds for f be non constant 0-preserving Functional of V holds ex v be Vector of V st v <> ( 0. V) & (f . v) <> ( 0. K)

    proof

      let K be Field, V be non trivial VectSp of K, f be non constant 0-preserving Functional of V;

      

       A1: (f . ( 0. V)) = ( 0. K) by HAHNBAN1:def 9;

      assume

       A2: for v be Vector of V st v <> ( 0. V) holds (f . v) = ( 0. K);

      now

        let x,y be object;

        assume x in ( dom f) & y in ( dom f);

        then

        reconsider v = x, w = y as Vector of V;

        

        thus (f . x) = (f . v)

        .= ( 0. K) by A2, A1

        .= (f . w) by A2, A1

        .= (f . y);

      end;

      hence contradiction by FUNCT_1:def 10;

    end;

    theorem :: VECTSP10:29

    

     Th29: for K be Field, V be non trivial VectSp of K holds for v be Vector of V, a be Scalar of V holds for W be Linear_Compl of ( Lin {v}) st v <> ( 0. V) holds (( coeffFunctional (v,W)) . (a * v)) = a

    proof

      let K be Field, V be non trivial VectSp of K, v be Vector of V, a be Scalar of V, W be Linear_Compl of ( Lin {v});

      assume

       A1: v <> ( 0. V);

      set cf = ( coeffFunctional (v,W));

      

      thus (cf . (a * v)) = (a * (cf . v)) by HAHNBAN1:def 8

      .= (a * ( 1_ K)) by A1, Def8

      .= a;

    end;

    theorem :: VECTSP10:30

    

     Th30: for K be Field, V be non trivial VectSp of K holds for v,w be Vector of V holds for W be Linear_Compl of ( Lin {v}) st v <> ( 0. V) & w in W holds (( coeffFunctional (v,W)) . w) = ( 0. K)

    proof

      let K be Field, V be non trivial VectSp of K, v,w be Vector of V, W be Linear_Compl of ( Lin {v});

      assume that

       A1: v <> ( 0. V) and

       A2: w in W;

      set cf = ( coeffFunctional (v,W)), cw = the carrier of W;

      reconsider s = w as Vector of W by A2;

      w in cw by A2;

      

      hence (cf . w) = ((cf | cw) . w) by FUNCT_1: 49

      .= (( 0Functional W) . s) by A1, Def8

      .= ( 0. K) by HAHNBAN1: 14;

    end;

    theorem :: VECTSP10:31

    for K be Field, V be non trivial VectSp of K holds for v,w be Vector of V, a be Scalar of V holds for W be Linear_Compl of ( Lin {v}) st v <> ( 0. V) & w in W holds (( coeffFunctional (v,W)) . ((a * v) + w)) = a

    proof

      let K be Field, V be non trivial VectSp of K, v,w be Vector of V, a be Scalar of V, W be Linear_Compl of ( Lin {v});

      assume that

       A1: v <> ( 0. V) and

       A2: w in W;

      set cf = ( coeffFunctional (v,W));

      

      thus (cf . ((a * v) + w)) = ((cf . (a * v)) + (cf . w)) by VECTSP_1:def 20

      .= ((cf . (a * v)) + ( 0. K)) by A1, A2, Th30

      .= (cf . (a * v)) by RLVECT_1:def 4

      .= a by A1, Th29;

    end;

    theorem :: VECTSP10:32

    for K be non empty addLoopStr holds for V be non empty ModuleStr over K holds for f,g be Functional of V, v be Vector of V holds ((f - g) . v) = ((f . v) - (g . v))

    proof

      let K be non empty addLoopStr;

      let V be non empty ModuleStr over K;

      let f,g be Functional of V, v be Vector of V;

      

      thus ((f - g) . v) = ((f . v) + (( - g) . v)) by HAHNBAN1:def 3

      .= ((f . v) - (g . v)) by HAHNBAN1:def 4;

    end;

    registration

      let K be Field;

      let V be non trivial VectSp of K;

      cluster (V *' ) -> non trivial;

      coherence

      proof

        set g = the non constant linear-Functional of V;

        

         A1: g <> ( 0Functional V);

        reconsider g as Element of (V *' ) by HAHNBAN1:def 10;

        assume (V *' ) is trivial;

        then g = ( 0. (V *' ));

        hence contradiction by A1, HAHNBAN1:def 10;

      end;

    end

    begin

    definition

      let S be non empty 1-sorted;

      let Z be ZeroStr;

      let f be Function of S, Z;

      :: VECTSP10:def9

      func ker f -> Subset of S equals { v where v be Element of S : (f . v) = ( 0. Z) };

      coherence

      proof

        set A = { v where v be Element of S : (f . v) = ( 0. Z) };

        A c= the carrier of S

        proof

          let x be object;

          assume x in A;

          then ex v be Element of S st v = x & (f . v) = ( 0. Z);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let K be right_zeroed non empty addLoopStr;

      let V be non empty ModuleStr over K;

      let f be 0-preserving Functional of V;

      cluster ( ker f) -> non empty;

      coherence

      proof

        (f . ( 0. V)) = ( 0. K) by HAHNBAN1:def 9;

        then ( 0. V) in ( ker f);

        hence thesis;

      end;

    end

    theorem :: VECTSP10:33

    

     Th33: for K be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr holds for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K holds for f be linear-Functional of V holds ( ker f) is linearly-closed

    proof

      let F be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F;

      let f be linear-Functional of V;

      set V1 = ( ker f);

      thus for v,u be Vector of V st v in V1 & u in V1 holds (v + u) in V1

      proof

        let v,u be Vector of V;

        assume v in V1 & u in V1;

        then (ex a be Vector of V st a = v & (f . a) = ( 0. F)) & ex b be Vector of V st b = u & (f . b) = ( 0. F);

        

        then (f . (v + u)) = (( 0. F) + ( 0. F)) by VECTSP_1:def 20

        .= ( 0. F) by RLVECT_1: 4;

        hence thesis;

      end;

      let a be Element of F;

      let v be Vector of V;

      assume v in V1;

      then ex w be Vector of V st w = v & (f . w) = ( 0. F);

      

      then (f . (a * v)) = (a * ( 0. F)) by HAHNBAN1:def 8

      .= ( 0. F);

      hence thesis;

    end;

    definition

      let K be non empty ZeroStr;

      let V be non empty ModuleStr over K;

      let f be Functional of V;

      :: VECTSP10:def10

      attr f is degenerated means ( ker f) <> {( 0. V)};

    end

    registration

      let K be non degenerated non empty doubleLoopStr;

      let V be non trivial ModuleStr over K;

      cluster non degenerated 0-preserving -> non constant for Functional of V;

      coherence

      proof

        let f be Functional of V;

        assume that

         A1: f is non degenerated and

         A2: f is 0-preserving and

         A3: f is constant;

        

         A4: (f . ( 0. V)) = ( 0. K) by A2;

         A5:

        now

          assume

           A6: for v be Vector of V st v <> ( 0. V) holds (f . v) = ( 0. K);

          the carrier of V c= ( ker f)

          proof

            let x be object;

            assume x in the carrier of V;

            then

            reconsider v = x as Vector of V;

            per cases ;

              suppose v = ( 0. V);

              hence thesis by A4;

            end;

              suppose v <> ( 0. V);

              then (f . v) = ( 0. K) by A6;

              hence thesis;

            end;

          end;

          

          then the carrier of V = ( ker f)

          .= {( 0. V)} by A1;

          hence contradiction;

        end;

        ( dom f) = the carrier of V by FUNCT_2:def 1;

        hence contradiction by A3, A4, A5;

      end;

    end

    definition

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K;

      let f be linear-Functional of V;

      :: VECTSP10:def11

      func Ker f -> strict non empty Subspace of V means

      : Def11: the carrier of it = ( ker f);

      existence by Th33, VECTSP_4: 34;

      uniqueness by VECTSP_4: 29;

    end

    definition

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K;

      let W be Subspace of V;

      let f be additive Functional of V;

      assume

       A1: the carrier of W c= ( ker f);

      :: VECTSP10:def12

      func QFunctional (f,W) -> additive Functional of ( VectQuot (V,W)) means

      : Def12: for A be Vector of ( VectQuot (V,W)), a be Vector of V st A = (a + W) holds (it . A) = (f . a);

      existence

      proof

        defpred P[ set, set] means for a be Vector of V st $1 = (a + W) holds $2 = (f . a);

        set aC = ( addCoset (V,W));

        set C = ( CosetSet (V,W));

        set vq = ( VectQuot (V,W));

         A2:

        now

          let A be Vector of vq;

          consider a be Vector of V such that

           A3: A = (a + W) by Th22;

          take y = (f . a);

          thus P[A, y]

          proof

            let a1 be Vector of V;

            assume A = (a1 + W);

            then a in (a1 + W) by A3, VECTSP_4: 44;

            then

            consider w be Vector of V such that

             A4: w in W and

             A5: a = (a1 + w) by VECTSP_4: 42;

            w in the carrier of W by A4;

            then w in ( ker f) by A1;

            then

             A6: ex aa be Vector of V st aa = w & (f . aa) = ( 0. K);

            

            thus y = ((f . a1) + (f . w)) by A5, VECTSP_1:def 20

            .= (f . a1) by A6, RLVECT_1:def 4;

          end;

        end;

        consider ff be Function of the carrier of vq, the carrier of K such that

         A7: for A be Vector of vq holds P[A, (ff . A)] from FUNCT_2:sch 3( A2);

        reconsider ff as Functional of vq;

        

         A8: C = the carrier of vq by Def6;

        now

          

           A9: the addF of vq = ( addCoset (V,W)) by Def6;

          let A,B be Vector of vq;

          consider a be Vector of V such that

           A10: A = (a + W) by Th22;

          consider b be Vector of V such that

           A11: B = (b + W) by Th22;

          (aC . (A,B)) = ((a + b) + W) by A8, A10, A11, Def3;

          

          hence (ff . (A + B)) = (f . (a + b)) by A7, A9

          .= ((f . a) + (f . b)) by VECTSP_1:def 20

          .= ((ff . A) + (f . b)) by A7, A10

          .= ((ff . A) + (ff . B)) by A7, A11;

        end;

        then

        reconsider ff as additive Functional of vq by VECTSP_1:def 20;

        take ff;

        thus thesis by A7;

      end;

      uniqueness

      proof

        set vq = ( VectQuot (V,W));

        let f1,f2 be additive Functional of vq such that

         A12: for A be Vector of ( VectQuot (V,W)) holds for a be Vector of V st A = (a + W) holds (f1 . A) = (f . a) and

         A13: for A be Vector of ( VectQuot (V,W)) holds for a be Vector of V st A = (a + W) holds (f2 . A) = (f . a);

        now

          let A be Vector of vq;

          consider a be Vector of V such that

           A14: A = (a + W) by Th22;

          

          thus (f1 . A) = (f . a) by A12, A14

          .= (f2 . A) by A13, A14;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: VECTSP10:34

    

     Th34: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V be VectSp of K, W be Subspace of V holds for f be linear-Functional of V st the carrier of W c= ( ker f) holds ( QFunctional (f,W)) is homogeneous

    proof

      let F be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of F;

      let W be Subspace of V;

      let f be linear-Functional of V;

      set qf = ( QFunctional (f,W));

      set vq = ( VectQuot (V,W));

      assume

       A1: the carrier of W c= ( ker f);

      now

        set C = ( CosetSet (V,W));

        let A be Vector of vq;

        let r be Scalar of vq;

        

         A2: C = the carrier of vq by Def6;

        then A in C;

        then

        consider aa be Coset of W such that

         A3: A = aa;

        consider a be Vector of V such that

         A4: aa = (a + W) by VECTSP_4:def 6;

        (r * A) = (the lmult of vq . (r,A))

        .= (( lmultCoset (V,W)) . (r,A)) by Def6

        .= ((r * a) + W) by A2, A3, A4, Def5;

        

        hence (qf . (r * A)) = (f . (r * a)) by A1, Def12

        .= (r * (f . a)) by HAHNBAN1:def 8

        .= (r * (qf . A)) by A1, A3, A4, Def12;

      end;

      hence thesis;

    end;

    definition

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K;

      let f be linear-Functional of V;

      :: VECTSP10:def13

      func CQFunctional (f) -> linear-Functional of ( VectQuot (V,( Ker f))) equals ( QFunctional (f,( Ker f)));

      correctness

      proof

        the carrier of ( Ker f) = ( ker f) by Def11;

        hence thesis by Th34;

      end;

    end

    theorem :: VECTSP10:35

    

     Th35: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V be VectSp of K, f be linear-Functional of V holds for A be Vector of ( VectQuot (V,( Ker f))), v be Vector of V st A = (v + ( Ker f)) holds (( CQFunctional f) . A) = (f . v)

    proof

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, f be linear-Functional of V;

      let A be Vector of ( VectQuot (V,( Ker f))), v be Vector of V;

      assume

       A1: A = (v + ( Ker f));

      the carrier of ( Ker f) = ( ker f) by Def11;

      hence thesis by A1, Def12;

    end;

    registration

      let K be Field;

      let V be non trivial VectSp of K;

      let f be non constant linear-Functional of V;

      cluster ( CQFunctional f) -> non constant;

      coherence

      proof

        set W = ( Ker f), qf = ( CQFunctional f), qv = ( VectQuot (V,W));

        consider v be Vector of V such that v <> ( 0. V) and

         A1: (f . v) <> ( 0. K) by Th28;

        reconsider cv = (v + W) as Vector of qv by Th23;

        assume qf is constant;

        then qf = ( 0Functional qv);

        

        then ( 0. K) = (qf . cv) by HAHNBAN1: 14

        .= (f . v) by Th35;

        hence contradiction by A1;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be VectSp of K;

      let f be linear-Functional of V;

      cluster ( CQFunctional f) -> non degenerated;

      coherence

      proof

        set qf = ( CQFunctional f), W = ( Ker f), qV = ( VectQuot (V,W));

        

         A1: the carrier of W = ( ker f) by Def11;

        

         A2: the carrier of qV = ( CosetSet (V,W)) by Def6;

        thus ( ker qf) c= {( 0. qV)}

        proof

          let x be object;

          assume x in ( ker qf);

          then

          consider w be Vector of qV such that

           A3: x = w and

           A4: (qf . w) = ( 0. K);

          w in ( CosetSet (V,W)) by A2;

          then

          consider A be Coset of W such that

           A5: w = A;

          consider v be Vector of V such that

           A6: A = (v + W) by VECTSP_4:def 6;

          (f . v) = ( 0. K) by A1, A4, A5, A6, Def12;

          then v in ( ker f);

          then v in W by A1;

          

          then w = ( zeroCoset (V,W)) by A5, A6, VECTSP_4: 49

          .= ( 0. qV) by Th21;

          hence thesis by A3, TARSKI:def 1;

        end;

        thus {( 0. qV)} c= ( ker qf)

        proof

          let x be object;

          assume x in {( 0. qV)};

          then

           A7: x = ( 0. qV) by TARSKI:def 1;

          (qf . ( 0. qV)) = ( 0. K) by HAHNBAN1:def 9;

          hence thesis by A7;

        end;

      end;

    end