vectsp_4.miz



    begin

    reserve x,y,y1,y2 for object;

    

     Lm1: for GF be add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, a,b be Element of GF, v be Element of V holds ((a - b) * v) = ((a * v) - (b * v))

    proof

      let GF be add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, a,b be Element of GF, v be Element of V;

      

      thus ((a - b) * v) = ((a * v) + (( - b) * v)) by VECTSP_1:def 15

      .= ((a * v) - (b * v)) by VECTSP_1: 21;

    end;

    definition

      let GF be non empty multMagma;

      let V be non empty ModuleStr over GF;

      let V1 be Subset of V;

      :: VECTSP_4:def1

      attr V1 is linearly-closed means (for v,u be Element of V st v in V1 & u in V1 holds (v + u) in V1) & for a be Element of GF, v be Element of V st v in V1 holds (a * v) in V1;

    end

    theorem :: VECTSP_4:1

    

     Th1: for GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1 be Subset of V st V1 <> {} & V1 is linearly-closed holds ( 0. V) in V1

    proof

      let GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1 be Subset of V;

      assume that

       A1: V1 <> {} and

       A2: V1 is linearly-closed;

      set x = the Element of V1;

      reconsider x as Element of V by A1, TARSKI:def 3;

      (( 0. GF) * x) in V1 by A1, A2;

      hence thesis by VECTSP_1: 14;

    end;

    theorem :: VECTSP_4:2

    

     Th2: for GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1 be Subset of V st V1 is linearly-closed holds for v be Element of V st v in V1 holds ( - v) in V1

    proof

      let GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1 be Subset of V;

      assume

       A1: V1 is linearly-closed;

      let v be Element of V;

      assume v in V1;

      then (( - ( 1_ GF)) * v) in V1 by A1;

      hence thesis by VECTSP_1: 14;

    end;

    theorem :: VECTSP_4:3

    for GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1 be Subset of V st V1 is linearly-closed holds for v,u be Element of V st v in V1 & u in V1 holds (v - u) in V1

    proof

      let GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1 be Subset of V;

      assume

       A1: V1 is linearly-closed;

      let v,u be Element of V;

      assume that

       A2: v in V1 and

       A3: u in V1;

      ( - u) in V1 by A1, A3, Th2;

      hence thesis by A1, A2;

    end;

    theorem :: VECTSP_4:4

    

     Th4: for GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF holds {( 0. V)} is linearly-closed

    proof

      let GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF;

      thus for v,u be Element of V st v in {( 0. V)} & u in {( 0. V)} holds (v + u) in {( 0. V)}

      proof

        let v,u be Element of V;

        assume v in {( 0. V)} & u in {( 0. V)};

        then v = ( 0. V) & u = ( 0. V) by TARSKI:def 1;

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

        hence thesis by TARSKI:def 1;

      end;

      let a be Element of GF;

      let v be Element of V;

      assume

       A1: v in {( 0. V)};

      then v = ( 0. V) by TARSKI:def 1;

      hence thesis by A1, VECTSP_1: 14;

    end;

    theorem :: VECTSP_4:5

    for GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1 be Subset of V st the carrier of V = V1 holds V1 is linearly-closed;

    theorem :: VECTSP_4:6

    for GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1,V2,V3 be Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v be Element of V, u be Element of V : v in V1 & u in V2 } holds V3 is linearly-closed

    proof

      let GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1,V2,V3 be Subset of V;

      assume that

       A1: V1 is linearly-closed & V2 is linearly-closed and

       A2: V3 = { (v + u) where v be Element of V, u be Element of V : v in V1 & u in V2 };

      thus for v,u be Element of V st v in V3 & u in V3 holds (v + u) in V3

      proof

        let v,u be Element of V;

        assume that

         A3: v in V3 and

         A4: u in V3;

        consider v1,v2 be Element of V such that

         A5: v = (v1 + v2) and

         A6: v1 in V1 & v2 in V2 by A2, A3;

        consider u1,u2 be Element of V such that

         A7: u = (u1 + u2) and

         A8: u1 in V1 & u2 in V2 by A2, A4;

        

         A9: (v + u) = (((v1 + v2) + u1) + u2) by A5, A7, RLVECT_1:def 3

        .= (((v1 + u1) + v2) + u2) by RLVECT_1:def 3

        .= ((v1 + u1) + (v2 + u2)) by RLVECT_1:def 3;

        (v1 + u1) in V1 & (v2 + u2) in V2 by A1, A6, A8;

        hence thesis by A2, A9;

      end;

      let a be Element of GF;

      let v be Element of V;

      assume v in V3;

      then

      consider v1,v2 be Element of V such that

       A10: v = (v1 + v2) and

       A11: v1 in V1 & v2 in V2 by A2;

      

       A12: (a * v) = ((a * v1) + (a * v2)) by A10, VECTSP_1:def 14;

      (a * v1) in V1 & (a * v2) in V2 by A1, A11;

      hence thesis by A2, A12;

    end;

    theorem :: VECTSP_4:7

    for GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1,V2 be Subset of V st V1 is linearly-closed & V2 is linearly-closed holds (V1 /\ V2) is linearly-closed

    proof

      let GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, V1,V2 be Subset of V;

      assume that

       A1: V1 is linearly-closed and

       A2: V2 is linearly-closed;

      thus for v,u be Element of V st v in (V1 /\ V2) & u in (V1 /\ V2) holds (v + u) in (V1 /\ V2)

      proof

        let v,u be Element of V;

        assume

         A3: v in (V1 /\ V2) & u in (V1 /\ V2);

        then v in V2 & u in V2 by XBOOLE_0:def 4;

        then

         A4: (v + u) in V2 by A2;

        v in V1 & u in V1 by A3, XBOOLE_0:def 4;

        then (v + u) in V1 by A1;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      let a be Element of GF;

      let v be Element of V;

      assume

       A5: v in (V1 /\ V2);

      then v in V2 by XBOOLE_0:def 4;

      then

       A6: (a * v) in V2 by A2;

      v in V1 by A5, XBOOLE_0:def 4;

      then (a * v) in V1 by A1;

      hence thesis by A6, XBOOLE_0:def 4;

    end;

    definition

      let GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF;

      :: VECTSP_4:def2

      mode Subspace of V -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF means

      : Def2: the carrier of it c= the carrier of V & ( 0. it ) = ( 0. V) & the addF of it = (the addF of V || the carrier of it ) & the lmult of it = (the lmult of V | [:the carrier of GF, the carrier of it :] qua set);

      existence

      proof

        take V;

        thus the carrier of V c= the carrier of V & ( 0. V) = ( 0. V);

        thus thesis by RELSET_1: 19;

      end;

    end

    reserve GF for add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr,

V,X,Y for Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF;

    reserve a for Element of GF;

    reserve u,u1,u2,v,v1,v2 for Element of V;

    reserve W,W1,W2 for Subspace of V;

    reserve V1 for Subset of V;

    reserve w,w1,w2 for Element of W;

    theorem :: VECTSP_4:8

    x in W1 & W1 is Subspace of W2 implies x in W2

    proof

      assume x in W1 & W1 is Subspace of W2;

      then x in the carrier of W1 & the carrier of W1 c= the carrier of W2 by Def2;

      hence thesis;

    end;

    theorem :: VECTSP_4:9

    

     Th9: x in W implies x in V

    proof

      assume x in W;

      then

       A1: x in the carrier of W;

      the carrier of W c= the carrier of V by Def2;

      hence thesis by A1;

    end;

    theorem :: VECTSP_4:10

    

     Th10: w is Element of V

    proof

      w in V by Th9, RLVECT_1: 1;

      hence thesis;

    end;

    theorem :: VECTSP_4:11

    ( 0. W) = ( 0. V) by Def2;

    theorem :: VECTSP_4:12

    ( 0. W1) = ( 0. W2)

    proof

      

      thus ( 0. W1) = ( 0. V) by Def2

      .= ( 0. W2) by Def2;

    end;

    theorem :: VECTSP_4:13

    

     Th13: w1 = v & w2 = u implies (w1 + w2) = (v + u)

    proof

      assume

       A1: v = w1 & u = w2;

      (w1 + w2) = ((the addF of V || the carrier of W) . [w1, w2]) by Def2;

      hence thesis by A1, FUNCT_1: 49;

    end;

    theorem :: VECTSP_4:14

    

     Th14: w = v implies (a * w) = (a * v)

    proof

      assume

       A1: w = v;

      (a * w) = ((the lmult of V | [:the carrier of GF, the carrier of W:] qua set) . [a, w]) by Def2;

      hence thesis by A1, FUNCT_1: 49;

    end;

    theorem :: VECTSP_4:15

    

     Th15: w = v implies ( - v) = ( - w)

    proof

      

       A1: ( - v) = (( - ( 1_ GF)) * v) & ( - w) = (( - ( 1_ GF)) * w) by VECTSP_1: 14;

      assume w = v;

      hence thesis by A1, Th14;

    end;

    theorem :: VECTSP_4:16

    

     Th16: w1 = v & w2 = u implies (w1 - w2) = (v - u)

    proof

      assume that

       A1: w1 = v and

       A2: w2 = u;

      ( - w2) = ( - u) by A2, Th15;

      hence thesis by A1, Th13;

    end;

    

     Lm2: the carrier of W = V1 implies V1 is linearly-closed

    proof

      set VW = the carrier of W;

      reconsider WW = W as Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF;

      assume

       A1: the carrier of W = V1;

      thus for v, u st v in V1 & u in V1 holds (v + u) in V1

      proof

        let v, u;

        assume v in V1 & u in V1;

        then

        reconsider vv = v, uu = u as Element of WW by A1;

        reconsider vw = (vv + uu) as Element of VW;

        vw in V1 by A1;

        hence thesis by Th13;

      end;

      let a, v;

      assume v in V1;

      then

      reconsider vv = v as Element of WW by A1;

      reconsider vw = (a * vv) as Element of VW;

      vw in V1 by A1;

      hence thesis by Th14;

    end;

    theorem :: VECTSP_4:17

    

     Th17: ( 0. V) in W

    proof

      ( 0. W) in W;

      hence thesis by Def2;

    end;

    theorem :: VECTSP_4:18

    ( 0. W1) in W2

    proof

      ( 0. W1) = ( 0. V) by Def2;

      hence thesis by Th17;

    end;

    theorem :: VECTSP_4:19

    ( 0. W) in V by Th9, RLVECT_1: 1;

    theorem :: VECTSP_4:20

    

     Th20: u in W & v in W implies (u + v) in W

    proof

      reconsider VW = the carrier of W as Subset of V by Def2;

      assume u in W & v in W;

      then

       A1: u in the carrier of W & v in the carrier of W;

      VW is linearly-closed by Lm2;

      then (u + v) in the carrier of W by A1;

      hence thesis;

    end;

    theorem :: VECTSP_4:21

    

     Th21: v in W implies (a * v) in W

    proof

      reconsider VW = the carrier of W as Subset of V by Def2;

      assume v in W;

      then

       A1: v in the carrier of W;

      VW is linearly-closed by Lm2;

      then (a * v) in the carrier of W by A1;

      hence thesis;

    end;

    theorem :: VECTSP_4:22

    

     Th22: v in W implies ( - v) in W

    proof

      assume v in W;

      then (( - ( 1_ GF)) * v) in W by Th21;

      hence thesis by VECTSP_1: 14;

    end;

    theorem :: VECTSP_4:23

    

     Th23: u in W & v in W implies (u - v) in W

    proof

      assume that

       A1: u in W and

       A2: v in W;

      ( - v) in W by A2, Th22;

      hence thesis by A1, Th20;

    end;

    theorem :: VECTSP_4:24

    

     Th24: V is Subspace of V

    proof

      

       A1: the lmult of V = (the lmult of V | [:the carrier of GF, the carrier of V:] qua set) by RELSET_1: 19;

      ( 0. V) = ( 0. V) & the addF of V = (the addF of V || the carrier of V) by RELSET_1: 19;

      hence thesis by A1, Def2;

    end;

    theorem :: VECTSP_4:25

    

     Th25: for X,V be strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF holds V is Subspace of X & X is Subspace of V implies V = X

    proof

      let X,V be strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF;

      assume that

       A1: V is Subspace of X and

       A2: X is Subspace of V;

      set VX = the carrier of X;

      set VV = the carrier of V;

      VV c= VX & VX c= VV by A1, A2, Def2;

      then

       A3: VV = VX;

      set AX = the addF of X;

      set AV = the addF of V;

      AV = (AX || VV) & AX = (AV || VX) by A1, A2, Def2;

      then

       A4: AV = AX by A3;

      set MX = the lmult of X;

      set MV = the lmult of V;

      

       A5: MX = (MV | [:the carrier of GF, VX:] qua set) by A2, Def2;

      ( 0. V) = ( 0. X) & MV = (MX | [:the carrier of GF, VV:] qua set) by A1, Def2;

      hence thesis by A3, A4, A5;

    end;

    theorem :: VECTSP_4:26

    

     Th26: V is Subspace of X & X is Subspace of Y implies V is Subspace of Y

    proof

      assume that

       A1: V is Subspace of X and

       A2: X is Subspace of Y;

      the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y by A1, A2, Def2;

      then

       A3: the carrier of V c= the carrier of Y;

      

       A4: the addF of V = (the addF of Y || the carrier of V)

      proof

        set AY = the addF of Y;

        set VX = the carrier of X;

        set AX = the addF of X;

        set VV = the carrier of V;

        set AV = the addF of V;

        VV c= VX by A1, Def2;

        then

         A5: [:VV, VV:] c= [:VX, VX:] by ZFMISC_1: 96;

        AV = (AX || VV) by A1, Def2;

        then AV = ((AY || VX) || VV) by A2, Def2;

        hence thesis by A5, FUNCT_1: 51;

      end;

      set MY = the lmult of Y;

      set MX = the lmult of X;

      set MV = the lmult of V;

      set VX = the carrier of X;

      set VV = the carrier of V;

      VV c= VX by A1, Def2;

      then

       A6: [:the carrier of GF, VV:] c= [:the carrier of GF, the carrier of X:] by ZFMISC_1: 95;

      MV = (MX | [:the carrier of GF, VV:] qua set) by A1, Def2;

      then MV = ((MY | [:the carrier of GF, VX:] qua set) | [:the carrier of GF, VV:] qua set) by A2, Def2;

      then

       A7: MV = (MY | [:the carrier of GF, VV:] qua set) by A6, FUNCT_1: 51;

      ( 0. V) = ( 0. X) by A1, Def2;

      then ( 0. V) = ( 0. Y) by A2, Def2;

      hence thesis by A3, A4, A7, Def2;

    end;

    theorem :: VECTSP_4:27

    

     Th27: the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2

    proof

      set VW1 = the carrier of W1;

      set VW2 = the carrier of W2;

      set MW1 = the lmult of W1;

      set MW2 = the lmult of W2;

      set AV = the addF of V;

      set MV = the lmult of V;

      

       A1: the addF of W1 = (AV || VW1) & the addF of W2 = (AV || VW2) by Def2;

      assume

       A2: the carrier of W1 c= the carrier of W2;

      then [:VW1, VW1:] c= [:VW2, VW2:] by ZFMISC_1: 96;

      then

       A3: the addF of W1 = (the addF of W2 || the carrier of W1) by A1, FUNCT_1: 51;

      

       A4: MW1 = (MV | [:the carrier of GF, VW1:] qua set) & MW2 = (MV | [:the carrier of GF, VW2:] qua set) by Def2;

       [:the carrier of GF, VW1:] c= [:the carrier of GF, VW2:] by A2, ZFMISC_1: 95;

      then

       A5: MW1 = (MW2 | [:the carrier of GF, VW1:] qua set) by A4, FUNCT_1: 51;

      ( 0. W1) = ( 0. V) & ( 0. W2) = ( 0. V) by Def2;

      hence thesis by A2, A3, A5, Def2;

    end;

    theorem :: VECTSP_4:28

    

     Th28: (for v st v in W1 holds v in W2) implies W1 is Subspace of W2

    proof

      assume

       A1: for v st v in W1 holds v in W2;

      the carrier of W1 c= the carrier of W2

      proof

        let x be object;

        assume

         A2: x in the carrier of W1;

        the carrier of W1 c= the carrier of V by Def2;

        then

        reconsider v = x as Element of V by A2;

        v in W1 by A2;

        then v in W2 by A1;

        hence thesis;

      end;

      hence thesis by Th27;

    end;

    registration

      let GF be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF;

      cluster strict for Subspace of V;

      existence

      proof

        set M = the lmult of V;

        set W = ModuleStr (# the carrier of V, the addF of V, ( 0. V), M #);

        

         A1: W is vector-distributive

        proof

          let a be Element of GF;

          let v,w be Element of W;

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

          

          thus (a * (v + w)) = (a * (x + y))

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

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

        end;

        

         A2: W is scalar-distributive

        proof

          let a,b be Element of GF;

          let v be Element of W;

          reconsider x = v as Element of V;

          

          thus ((a + b) * v) = ((a + b) * x)

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

          .= ((a * v) + (b * v));

        end;

        

         A3: W is scalar-associative

        proof

          let a,b be Element of GF;

          let v be Element of W;

          reconsider x = v as Element of V;

          

          thus ((a * b) * v) = ((a * b) * x)

          .= (a * (b * x)) by VECTSP_1:def 16

          .= (a * (b * v));

        end;

        

         A4: W is scalar-unital

        proof

          let v be Element of W;

          reconsider x = v as Element of V;

          

          thus (( 1. GF) * v) = (( 1_ GF) * x)

          .= v by VECTSP_1:def 17;

        end;

        

         A5: for a,b be Element of W holds for x,y be Element of V st x = a & b = y holds (a + b) = (x + y);

        W is Abelian add-associative right_zeroed right_complementable

        proof

          thus W is Abelian

          proof

            let a,b be Element of W;

            reconsider x = a, y = b as Element of V;

            

            thus (a + b) = (y + x) by A5

            .= (b + a);

          end;

          hereby

            let a,b,c be Element of W;

            reconsider x = a, y = b, z = c as Element of V;

            

            thus ((a + b) + c) = ((x + y) + z)

            .= (x + (y + z)) by RLVECT_1:def 3

            .= (a + (b + c));

          end;

          hereby

            let a be Element of W;

            reconsider x = a as Element of V;

            

            thus (a + ( 0. W)) = (x + ( 0. V))

            .= a by RLVECT_1: 4;

          end;

          let a be Element of W;

          reconsider x = a as Element of V;

          reconsider b = (( comp V) . x) as Element of W;

          take b;

          

          thus (a + b) = (x + ( - x)) by VECTSP_1:def 13

          .= ( 0. W) by RLVECT_1: 5;

        end;

        then

        reconsider W as Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF by A1, A2, A3, A4;

        

         A6: ( 0. W) = ( 0. V) & the addF of W = (the addF of V || the carrier of W) by RELSET_1: 19;

        the lmult of W = (the lmult of V | [:the carrier of GF, the carrier of W:] qua set) by RELSET_1: 19;

        then

        reconsider W as Subspace of V by A6, Def2;

        take W;

        thus thesis;

      end;

    end

    theorem :: VECTSP_4:29

    

     Th29: for W1,W2 be strict Subspace of V st the carrier of W1 = the carrier of W2 holds W1 = W2

    proof

      let W1,W2 be strict Subspace of V;

      assume the carrier of W1 = the carrier of W2;

      then W1 is Subspace of W2 & W2 is Subspace of W1 by Th27;

      hence thesis by Th25;

    end;

    theorem :: VECTSP_4:30

    

     Th30: for W1,W2 be strict Subspace of V st (for v holds v in W1 iff v in W2) holds W1 = W2

    proof

      let W1,W2 be strict Subspace of V;

      assume

       A1: for v holds v in W1 iff v in W2;

      for x be object holds x in the carrier of W1 iff x in the carrier of W2

      proof

        let x be object;

        thus x in the carrier of W1 implies x in the carrier of W2

        proof

          assume

           A2: x in the carrier of W1;

          the carrier of W1 c= the carrier of V by Def2;

          then

          reconsider v = x as Element of V by A2;

          v in W1 by A2;

          then v in W2 by A1;

          hence thesis;

        end;

        assume

         A3: x in the carrier of W2;

        the carrier of W2 c= the carrier of V by Def2;

        then

        reconsider v = x as Element of V by A3;

        v in W2 by A3;

        then v in W1 by A1;

        hence thesis;

      end;

      then the carrier of W1 = the carrier of W2 by TARSKI: 2;

      hence thesis by Th29;

    end;

    theorem :: VECTSP_4:31

    for V be strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, W be strict Subspace of V holds the carrier of W = the carrier of V implies W = V

    proof

      let V be strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, W be strict Subspace of V;

      assume

       A1: the carrier of W = the carrier of V;

      V is Subspace of V by Th24;

      hence thesis by A1, Th29;

    end;

    theorem :: VECTSP_4:32

    for V be strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, W be strict Subspace of V holds (for v be Element of V holds v in W) implies W = V

    proof

      let V be strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, W be strict Subspace of V;

      assume for v be Element of V holds v in W;

      then

       A1: for v be Element of V holds (v in W iff v in V);

      V is Subspace of V by Th24;

      hence thesis by A1, Th30;

    end;

    theorem :: VECTSP_4:33

    the carrier of W = V1 implies V1 is linearly-closed by Lm2;

    theorem :: VECTSP_4:34

    

     Th34: V1 <> {} & V1 is linearly-closed implies ex W be strict Subspace of V st V1 = the carrier of W

    proof

      assume that

       A1: V1 <> {} and

       A2: V1 is linearly-closed;

      reconsider D = V1 as non empty set by A1;

      reconsider d = ( 0. V) as Element of D by A2, Th1;

      set VV = the carrier of V;

      set C = (( comp V) | D);

      ( dom ( comp V)) = VV by FUNCT_2:def 1;

      then

       A3: ( dom C) = D by RELAT_1: 62;

      

       A4: ( rng C) c= D

      proof

        let x be object;

        assume x in ( rng C);

        then

        consider y be object such that

         A5: y in ( dom C) and

         A6: (C . y) = x by FUNCT_1:def 3;

        reconsider y as Element of V by A3, A5;

        x = (( comp V) . y) by A5, A6, FUNCT_1: 47

        .= ( - y) by VECTSP_1:def 13;

        hence thesis by A2, A3, A5, Th2;

      end;

      set M = (the lmult of V | [:the carrier of GF, D:] qua set);

      ( dom the lmult of V) = [:the carrier of GF, VV:] by FUNCT_2:def 1;

      then

       A7: ( dom M) = [:the carrier of GF, D:] by RELAT_1: 62, ZFMISC_1: 96;

      

       A8: ( rng M) c= D

      proof

        let x be object;

        assume x in ( rng M);

        then

        consider y be object such that

         A9: y in ( dom M) and

         A10: (M . y) = x by FUNCT_1:def 3;

        consider y1,y2 be object such that

         A11: [y1, y2] = y by A7, A9, RELAT_1:def 1;

        reconsider y1 as Element of GF by A7, A9, A11, ZFMISC_1: 87;

        

         A12: y2 in V1 by A7, A9, A11, ZFMISC_1: 87;

        then

        reconsider y2 as Element of V;

        x = (y1 * y2) by A9, A10, A11, FUNCT_1: 47;

        hence thesis by A2, A12;

      end;

      set A = (the addF of V || D);

      ( dom the addF of V) = [:VV, VV:] by FUNCT_2:def 1;

      then

       A13: ( dom A) = [:D, D:] by RELAT_1: 62, ZFMISC_1: 96;

      

       A14: ( rng A) c= D

      proof

        let x be object;

        assume x in ( rng A);

        then

        consider y be object such that

         A15: y in ( dom A) and

         A16: (A . y) = x by FUNCT_1:def 3;

        consider y1,y2 be object such that

         A17: [y1, y2] = y by A13, A15, RELAT_1:def 1;

        

         A18: y1 in D & y2 in D by A13, A15, A17, ZFMISC_1: 87;

        then

        reconsider y1, y2 as Element of V;

        x = (y1 + y2) by A15, A16, A17, FUNCT_1: 47;

        hence thesis by A2, A18;

      end;

      reconsider M as Function of [:the carrier of GF, D:], D by A7, A8, FUNCT_2:def 1, RELSET_1: 4;

      reconsider C as UnOp of D by A3, A4, FUNCT_2:def 1, RELSET_1: 4;

      reconsider A as BinOp of D by A13, A14, FUNCT_2:def 1, RELSET_1: 4;

      set W = ModuleStr (# D, A, d, M #);

      

       A19: for a,b be Element of W holds for x,y be Element of V st x = a & b = y holds (a + b) = (x + y)

      proof

        let a,b be Element of W;

        let x,y be Element of V such that

         A20: x = a & b = y;

        

        thus (a + b) = (A . [a, b])

        .= (x + y) by A13, A20, FUNCT_1: 47;

      end;

      

       A21: W is Abelian add-associative right_zeroed right_complementable

      proof

        thus W is Abelian

        proof

          let a,b be Element of W;

          reconsider x = a, y = b as Element of V by TARSKI:def 3;

          

          thus (a + b) = (y + x) by A19

          .= (b + a) by A19;

        end;

        hereby

          let a,b,c be Element of W;

          reconsider x = a, y = b, z = c as Element of V by TARSKI:def 3;

          

           A22: (b + c) = (y + z) by A19;

          (a + b) = (x + y) by A19;

          

          hence ((a + b) + c) = ((x + y) + z) by A19

          .= (x + (y + z)) by RLVECT_1:def 3

          .= (a + (b + c)) by A19, A22;

        end;

        hereby

          let a be Element of W;

          reconsider x = a as Element of V by TARSKI:def 3;

          

          thus (a + ( 0. W)) = (x + ( 0. V)) by A19

          .= a by RLVECT_1: 4;

        end;

        let a be Element of W;

        reconsider x = a as Element of V by TARSKI:def 3;

        reconsider a9 = a as Element of D;

        reconsider b = (C . a9) as Element of D;

        reconsider b as Element of W;

        take b;

        

        thus (a + b) = (x + (( comp V) . x)) by A3, A19, FUNCT_1: 47

        .= (x + ( - x)) by VECTSP_1:def 13

        .= ( 0. W) by RLVECT_1: 5;

      end;

      

       A23: W is vector-distributive

      proof

        let a be Element of GF;

        let v,w be Element of W;

        reconsider x = v, y = w as Element of V by TARSKI:def 3;

         A24:

        now

          let a be Element of GF;

          let x be Element of W;

          let y be Element of V;

          assume

           A25: y = x;

           [a, x] in ( dom M) by A7;

          hence (a * x) = (a * y) by A25, FUNCT_1: 47;

        end;

        then

         A26: (a * v) = (a * x);

        

         A27: (a * w) = (a * y) by A24;

        (v + w) = (x + y) by A19;

        

        hence (a * (v + w)) = (a * (x + y)) by A24

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

        .= ((a * v) + (a * w)) by A19, A26, A27;

      end;

      

       A28: W is scalar-distributive

      proof

        let a,b be Element of GF;

        let v be Element of W;

        reconsider x = v as Element of V by TARSKI:def 3;

         A29:

        now

          let a be Element of GF;

          let x be Element of W;

          let y be Element of V;

          assume

           A30: y = x;

           [a, x] in ( dom M) by A7;

          hence (a * x) = (a * y) by A30, FUNCT_1: 47;

        end;

        then

         A31: (a * v) = (a * x);

        

         A32: (b * v) = (b * x) by A29;

        

        thus ((a + b) * v) = ((a + b) * x) by A29

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

        .= ((a * v) + (b * v)) by A19, A32, A31;

      end;

      

       A33: W is scalar-associative

      proof

        let a,b be Element of GF;

        let v be Element of W;

        reconsider x = v as Element of V by TARSKI:def 3;

         A34:

        now

          let a be Element of GF;

          let x be Element of W;

          let y be Element of V;

          assume

           A35: y = x;

           [a, x] in ( dom M) by A7;

          hence (a * x) = (a * y) by A35, FUNCT_1: 47;

        end;

        then

         A36: (b * v) = (b * x);

        

        thus ((a * b) * v) = ((a * b) * x) by A34

        .= (a * (b * x)) by VECTSP_1:def 16

        .= (a * (b * v)) by A34, A36;

      end;

      W is scalar-unital

      proof

        let v be Element of W;

        reconsider x = v as Element of V by TARSKI:def 3;

        now

          let a be Element of GF;

          let x be Element of W;

          let y be Element of V;

          assume

           A37: y = x;

           [a, x] in ( dom M) by A7;

          hence (a * x) = (a * y) by A37, FUNCT_1: 47;

        end;

        

        hence (( 1. GF) * v) = (( 1_ GF) * x)

        .= v by VECTSP_1:def 17;

      end;

      then

      reconsider W as Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF by A21, A23, A28, A33;

      ( 0. W) = ( 0. V);

      then

      reconsider W as strict Subspace of V by Def2;

      take W;

      thus thesis;

    end;

    definition

      let GF;

      let V;

      :: VECTSP_4:def3

      func (0). V -> strict Subspace of V means

      : Def3: the carrier of it = {( 0. V)};

      correctness by Th4, Th29, Th34;

    end

    definition

      let GF;

      let V;

      :: VECTSP_4:def4

      func (Omega). V -> strict Subspace of V equals the ModuleStr of V;

      coherence

      proof

        set W = the ModuleStr of V;

        

         A1: W is vector-distributive

        proof

          let x be Element of GF, v,w be Element of W;

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

          

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

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

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

        end;

        

         A2: W is scalar-distributive

        proof

          let x,y be Element of GF, v be Element of W;

          reconsider v9 = v as Element of V;

          

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

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

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

        end;

        

         A3: W is scalar-associative

        proof

          let x,y be Element of GF, v be Element of W;

          reconsider v9 = v as Element of V;

          

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

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

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

        end;

        

         A4: W is scalar-unital

        proof

          let v be Element of W;

          reconsider v9 = v as Element of V;

          

          thus (( 1. GF) * v) = (( 1_ GF) * v9)

          .= v by VECTSP_1:def 17;

        end;

        

         A5: for a holds for v,w be Element of W, v9,w9 be Element of V st v = v9 & w = w9 holds (v + w) = (v9 + w9) & (a * v) = (a * v9);

        W is Abelian add-associative right_zeroed right_complementable

        proof

          thus W is Abelian

          proof

            let x,y be Element of W;

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

            

            thus (x + y) = (y9 + x9) by A5

            .= (y + x);

          end;

          hereby

            let x,y,z be Element of W;

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

            

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

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

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

          end;

          hereby

            let x be Element of W;

            reconsider x9 = x as Element of V;

            

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

            .= x by RLVECT_1: 4;

          end;

          let x be Element of W;

          reconsider x9 = x as Element of V;

          consider b be Element of V such that

           A6: (x9 + b) = ( 0. V) by ALGSTR_0:def 11;

          reconsider b9 = b as Element of W;

          take b9;

          thus thesis by A6;

        end;

        then

        reconsider W as Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF by A4, A1, A2, A3;

        

         A7: the lmult of W = (the lmult of V | [:the carrier of GF, the carrier of W:] qua set) by RELSET_1: 19;

        ( 0. W) = ( 0. V) & the addF of W = (the addF of V || the carrier of W) by RELSET_1: 19;

        hence thesis by A7, Def2;

      end;

    end

    theorem :: VECTSP_4:35

    x in ( (0). V) iff x = ( 0. V)

    proof

      thus x in ( (0). V) implies x = ( 0. V)

      proof

        assume x in ( (0). V);

        then x in the carrier of ( (0). V);

        then x in {( 0. V)} by Def3;

        hence thesis by TARSKI:def 1;

      end;

      thus thesis by Th17;

    end;

    theorem :: VECTSP_4:36

    

     Th36: ( (0). W) = ( (0). V)

    proof

      the carrier of ( (0). W) = {( 0. W)} & the carrier of ( (0). V) = {( 0. V)} by Def3;

      then

       A1: the carrier of ( (0). W) = the carrier of ( (0). V) by Def2;

      ( (0). W) is Subspace of V by Th26;

      hence thesis by A1, Th29;

    end;

    theorem :: VECTSP_4:37

    

     Th37: ( (0). W1) = ( (0). W2)

    proof

      ( (0). W1) = ( (0). V) by Th36;

      hence thesis by Th36;

    end;

    theorem :: VECTSP_4:38

    ( (0). W) is Subspace of V by Th26;

    theorem :: VECTSP_4:39

    ( (0). V) is Subspace of W

    proof

      ( (0). W) = ( (0). V) by Th36;

      hence thesis;

    end;

    theorem :: VECTSP_4:40

    ( (0). W1) is Subspace of W2

    proof

      ( (0). W1) = ( (0). W2) by Th37;

      hence thesis;

    end;

    theorem :: VECTSP_4:41

    for V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF holds V is Subspace of ( (Omega). V)

    proof

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

      reconsider VS = V as Subspace of V by Th24;

      for v be Vector of V st v in VS holds v in ( (Omega). V);

      hence thesis by Th28;

    end;

    definition

      let GF;

      let V;

      let v, W;

      :: VECTSP_4:def5

      func v + W -> Subset of V equals { (v + u) : u in W };

      coherence

      proof

        set Y = { (v + u) : u in W };

        defpred Sep[ object] means ex u st $1 = (v + u) & u in W;

        consider X be set such that

         A1: for x be object holds x in X iff x in the carrier of V & Sep[x] from XBOOLE_0:sch 1;

        X c= the carrier of V by A1;

        then

        reconsider X as Subset of V;

        

         A2: Y c= X

        proof

          let x be object;

          assume x in Y;

          then ex u st x = (v + u) & u in W;

          hence thesis by A1;

        end;

        X c= Y

        proof

          let x be object;

          assume x in X;

          then ex u st x = (v + u) & u in W by A1;

          hence thesis;

        end;

        hence thesis by A2, XBOOLE_0:def 10;

      end;

    end

    

     Lm3: (( 0. V) + W) = the carrier of W

    proof

      set A = { (( 0. V) + u) : u in W };

      

       A1: the carrier of W c= A

      proof

        let x be object;

        assume x in the carrier of W;

        then

         A2: x in W;

        then x in V by Th9;

        then

        reconsider y = x as Element of V;

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

        hence thesis by A2;

      end;

      A c= the carrier of W

      proof

        let x be object;

        assume x in A;

        then

        consider u such that

         A3: x = (( 0. V) + u) and

         A4: u in W;

        x = u by A3, RLVECT_1: 4;

        hence thesis by A4;

      end;

      hence thesis by A1;

    end;

    definition

      let GF;

      let V;

      let W;

      :: VECTSP_4:def6

      mode Coset of W -> Subset of V means

      : Def6: ex v st it = (v + W);

      existence

      proof

        reconsider VW = the carrier of W as Subset of V by Def2;

        take VW;

        take ( 0. V);

        thus thesis by Lm3;

      end;

    end

    reserve B,C for Coset of W;

    theorem :: VECTSP_4:42

    

     Th42: x in (v + W) iff ex u st u in W & x = (v + u)

    proof

      thus x in (v + W) implies ex u st u in W & x = (v + u)

      proof

        assume x in (v + W);

        then

        consider u such that

         A1: x = (v + u) & u in W;

        take u;

        thus thesis by A1;

      end;

      given u such that

       A2: u in W & x = (v + u);

      thus thesis by A2;

    end;

    theorem :: VECTSP_4:43

    

     Th43: ( 0. V) in (v + W) iff v in W

    proof

      thus ( 0. V) in (v + W) implies v in W

      proof

        assume ( 0. V) in (v + W);

        then

        consider u such that

         A1: ( 0. V) = (v + u) and

         A2: u in W;

        v = ( - u) by A1, VECTSP_1: 16;

        hence thesis by A2, Th22;

      end;

      assume v in W;

      then

       A3: ( - v) in W by Th22;

      ( 0. V) = (v + ( - v)) by VECTSP_1: 19;

      hence thesis by A3;

    end;

    theorem :: VECTSP_4:44

    

     Th44: v in (v + W)

    proof

      (v + ( 0. V)) = v & ( 0. V) in W by Th17, RLVECT_1: 4;

      hence thesis;

    end;

    theorem :: VECTSP_4:45

    (( 0. V) + W) = the carrier of W by Lm3;

    theorem :: VECTSP_4:46

    

     Th46: (v + ( (0). V)) = {v}

    proof

      thus (v + ( (0). V)) c= {v}

      proof

        let x be object;

        assume x in (v + ( (0). V));

        then

        consider u such that

         A1: x = (v + u) and

         A2: u in ( (0). V);

        

         A3: the carrier of ( (0). V) = {( 0. V)} by Def3;

        u in the carrier of ( (0). V) by A2;

        then u = ( 0. V) by A3, TARSKI:def 1;

        then x = v by A1, RLVECT_1: 4;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {v};

      then

       A4: x = v by TARSKI:def 1;

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

      hence thesis by A4;

    end;

    

     Lm4: v in W iff (v + W) = the carrier of W

    proof

      ( 0. V) in W & (v + ( 0. V)) = v by Th17, RLVECT_1: 4;

      then

       A1: v in { (v + u) : u in W };

      thus v in W implies (v + W) = the carrier of W

      proof

        assume

         A2: v in W;

        thus (v + W) c= the carrier of W

        proof

          let x be object;

          assume x in (v + W);

          then

          consider u such that

           A3: x = (v + u) and

           A4: u in W;

          (v + u) in W by A2, A4, Th20;

          hence thesis by A3;

        end;

        let x be object;

        assume x in the carrier of W;

        then

        reconsider y = x, z = v as Element of W by A2;

        reconsider y1 = y, z1 = z as Element of V by Th10;

        

         A5: (z + (y - z)) = (y + (z + ( - z))) by RLVECT_1:def 3

        .= (y + ( 0. W)) by VECTSP_1: 19

        .= x by RLVECT_1: 4;

        (y - z) in W;

        then

         A6: (y1 - z1) in W by Th16;

        (y - z) = (y1 - z1) by Th16;

        then (z1 + (y1 - z1)) = x by A5, Th13;

        hence thesis by A6;

      end;

      assume

       A7: (v + W) = the carrier of W;

      assume not v in W;

      hence thesis by A7, A1;

    end;

    theorem :: VECTSP_4:47

    

     Th47: (v + ( (Omega). V)) = the carrier of V by RLVECT_1: 1, Lm4;

    theorem :: VECTSP_4:48

    

     Th48: ( 0. V) in (v + W) iff (v + W) = the carrier of W by Th43, Lm4;

    theorem :: VECTSP_4:49

    v in W iff (v + W) = the carrier of W by Lm4;

    theorem :: VECTSP_4:50

    

     Th50: v in W implies ((a * v) + W) = the carrier of W by Th21, Lm4;

    theorem :: VECTSP_4:51

    

     Th51: for GF be Field, V be VectSp of GF, a be Element of GF, v be Element of V, W be Subspace of V st a <> ( 0. GF) & ((a * v) + W) = the carrier of W holds v in W

    proof

      let GF be Field, V be VectSp of GF, a be Element of GF, v be Element of V, W be Subspace of V;

      assume that

       A1: a <> ( 0. GF) and

       A2: ((a * v) + W) = the carrier of W;

      assume not v in W;

      then not (( 1_ GF) * v) in W by VECTSP_1:def 17;

      then not (((a " ) * a) * v) in W by A1, VECTSP_1:def 10;

      then not ((a " ) * (a * v)) in W by VECTSP_1:def 16;

      then

       A3: not (a * v) in W by Th21;

      ( 0. V) in W & ((a * v) + ( 0. V)) = (a * v) by Th17, RLVECT_1: 4;

      then (a * v) in { ((a * v) + u) where u be Vector of V : u in W };

      hence contradiction by A2, A3;

    end;

    theorem :: VECTSP_4:52

    for GF be Field, V be VectSp of GF, v be Element of V, W be Subspace of V holds v in W iff (( - v) + W) = the carrier of W

    proof

      let GF be Field, V be VectSp of GF, v be Element of V, W be Subspace of V;

      ( - ( 1_ GF)) <> ( 0. GF) by VECTSP_2: 3;

      then v in W iff ((( - ( 1_ GF)) * v) + W) = the carrier of W by Th50, Th51;

      hence thesis by VECTSP_1: 14;

    end;

    theorem :: VECTSP_4:53

    

     Th53: u in W iff (v + W) = ((v + u) + W)

    proof

      thus u in W implies (v + W) = ((v + u) + W)

      proof

        assume

         A1: u in W;

        thus (v + W) c= ((v + u) + W)

        proof

          let x be object;

          assume x in (v + W);

          then

          consider v1 such that

           A2: x = (v + v1) and

           A3: v1 in W;

          

           A4: ((v + u) + (v1 - u)) = (v + (u + (v1 - u))) by RLVECT_1:def 3

          .= (v + ((v1 + u) - u)) by RLVECT_1:def 3

          .= (v + (v1 + (u - u))) by RLVECT_1:def 3

          .= (v + (v1 + ( 0. V))) by VECTSP_1: 19

          .= x by A2, RLVECT_1: 4;

          (v1 - u) in W by A1, A3, Th23;

          hence thesis by A4;

        end;

        let x be object;

        assume x in ((v + u) + W);

        then

        consider v2 such that

         A5: x = ((v + u) + v2) and

         A6: v2 in W;

        

         A7: x = (v + (u + v2)) by A5, RLVECT_1:def 3;

        (u + v2) in W by A1, A6, Th20;

        hence thesis by A7;

      end;

      assume

       A8: (v + W) = ((v + u) + W);

      ( 0. V) in W & (v + ( 0. V)) = v by Th17, RLVECT_1: 4;

      then v in ((v + u) + W) by A8;

      then

      consider u1 such that

       A9: v = ((v + u) + u1) and

       A10: u1 in W;

      v = (v + (u + u1)) by A9, RLVECT_1:def 3;

      then (u + u1) = ( 0. V) by RLVECT_1: 9;

      then u = ( - u1) by VECTSP_1: 16;

      hence thesis by A10, Th22;

    end;

    theorem :: VECTSP_4:54

    u in W iff (v + W) = ((v - u) + W)

    proof

      

       A1: ( - u) in W implies u in W

      proof

        assume ( - u) in W;

        then ( - ( - u)) in W by Th22;

        hence thesis by RLVECT_1: 17;

      end;

      ( - u) in W iff (v + W) = ((v + ( - u)) + W) by Th53;

      hence thesis by A1, Th22;

    end;

    theorem :: VECTSP_4:55

    

     Th55: v in (u + W) iff (u + W) = (v + W)

    proof

      thus v in (u + W) implies (u + W) = (v + W)

      proof

        assume v in (u + W);

        then

        consider z be Element of V such that

         A1: v = (u + z) and

         A2: z in W;

        thus (u + W) c= (v + W)

        proof

          let x be object;

          assume x in (u + W);

          then

          consider v1 such that

           A3: x = (u + v1) and

           A4: v1 in W;

          (v - z) = (u + (z - z)) by A1, RLVECT_1:def 3

          .= (u + ( 0. V)) by VECTSP_1: 19

          .= u by RLVECT_1: 4;

          

          then

           A5: x = (v + (v1 + ( - z))) by A3, RLVECT_1:def 3

          .= (v + (v1 - z));

          (v1 - z) in W by A2, A4, Th23;

          hence thesis by A5;

        end;

        let x be object;

        assume x in (v + W);

        then

        consider v2 such that

         A6: x = (v + v2) & v2 in W;

        (z + v2) in W & x = (u + (z + v2)) by A1, A2, A6, Th20, RLVECT_1:def 3;

        hence thesis;

      end;

      thus thesis by Th44;

    end;

    theorem :: VECTSP_4:56

    

     Th56: u in (v1 + W) & u in (v2 + W) implies (v1 + W) = (v2 + W)

    proof

      assume that

       A1: u in (v1 + W) and

       A2: u in (v2 + W);

      

      thus (v1 + W) = (u + W) by A1, Th55

      .= (v2 + W) by A2, Th55;

    end;

    theorem :: VECTSP_4:57

    for GF be Field, V be VectSp of GF, a be Element of GF, v be Element of V, W be Subspace of V st a <> ( 1_ GF) & (a * v) in (v + W) holds v in W

    proof

      let GF be Field, V be VectSp of GF, a be Element of GF, v be Element of V, W be Subspace of V;

      assume that

       A1: a <> ( 1_ GF) and

       A2: (a * v) in (v + W);

      

       A3: (a - ( 1_ GF)) <> ( 0. GF) by A1, RLVECT_1: 21;

      consider u be Element of V such that

       A4: (a * v) = (v + u) and

       A5: u in W by A2;

      u = (u + ( 0. V)) by RLVECT_1: 4

      .= (u + (v - v)) by VECTSP_1: 19

      .= ((a * v) - v) by A4, RLVECT_1:def 3

      .= ((a * v) - (( 1_ GF) * v)) by VECTSP_1:def 17

      .= ((a - ( 1_ GF)) * v) by Lm1;

      then (((a - ( 1_ GF)) " ) * u) = ((((a - ( 1_ GF)) " ) * (a - ( 1_ GF))) * v) by VECTSP_1:def 16;

      then (( 1_ GF) * v) = (((a - ( 1_ GF)) " ) * u) by A3, VECTSP_1:def 10;

      then v = (((a - ( 1_ GF)) " ) * u) by VECTSP_1:def 17;

      hence thesis by A5, Th21;

    end;

    theorem :: VECTSP_4:58

    

     Th58: v in W implies (a * v) in (v + W)

    proof

      assume v in W;

      then (v + W) = the carrier of W & (a * v) in W by Lm4, Th21;

      hence thesis;

    end;

    theorem :: VECTSP_4:59

    v in W implies ( - v) in (v + W)

    proof

      assume v in W;

      then (( - ( 1_ GF)) * v) in (v + W) by Th58;

      hence thesis by VECTSP_1: 14;

    end;

    theorem :: VECTSP_4:60

    

     Th60: (u + v) in (v + W) iff u in W

    proof

      thus (u + v) in (v + W) implies u in W

      proof

        assume (u + v) in (v + W);

        then ex v1 st (u + v) = (v + v1) & v1 in W;

        hence thesis by RLVECT_1: 8;

      end;

      assume u in W;

      hence thesis;

    end;

    theorem :: VECTSP_4:61

    (v - u) in (v + W) iff u in W

    proof

      

       A1: (v - u) = (( - u) + v);

      

       A2: ( - u) in W implies ( - ( - u)) in W by Th22;

      u in W implies ( - u) in W by Th22;

      hence thesis by A1, A2, Th60, RLVECT_1: 17;

    end;

    theorem :: VECTSP_4:62

    u in (v + W) iff ex v1 st v1 in W & u = (v - v1)

    proof

      thus u in (v + W) implies ex v1 st v1 in W & u = (v - v1)

      proof

        assume u in (v + W);

        then

        consider v1 such that

         A1: u = (v + v1) and

         A2: v1 in W;

        take x = ( - v1);

        thus x in W by A2, Th22;

        thus thesis by A1, RLVECT_1: 17;

      end;

      given v1 such that

       A3: v1 in W and

       A4: u = (v - v1);

      ( - v1) in W by A3, Th22;

      hence thesis by A4;

    end;

    theorem :: VECTSP_4:63

    

     Th63: (ex v st v1 in (v + W) & v2 in (v + W)) iff (v1 - v2) in W

    proof

      thus (ex v st v1 in (v + W) & v2 in (v + W)) implies (v1 - v2) in W

      proof

        given v such that

         A1: v1 in (v + W) and

         A2: v2 in (v + W);

        consider u2 such that

         A3: u2 in W and

         A4: v2 = (v + u2) by A2, Th42;

        consider u1 such that

         A5: u1 in W and

         A6: v1 = (v + u1) by A1, Th42;

        (v1 - v2) = ((u1 + v) + (( - v) - u2)) by A6, A4, VECTSP_1: 17

        .= (((u1 + v) + ( - v)) - u2) by RLVECT_1:def 3

        .= ((u1 + (v + ( - v))) - u2) by RLVECT_1:def 3

        .= ((u1 + ( 0. V)) - u2) by RLVECT_1: 5

        .= (u1 - u2) by RLVECT_1: 4;

        hence thesis by A5, A3, Th23;

      end;

      assume (v1 - v2) in W;

      then

       A7: ( - (v1 - v2)) in W by Th22;

      take v1;

      thus v1 in (v1 + W) by Th44;

      (v1 + ( - (v1 - v2))) = (v1 + (( - v1) + v2)) by VECTSP_1: 17

      .= ((v1 + ( - v1)) + v2) by RLVECT_1:def 3

      .= (( 0. V) + v2) by RLVECT_1: 5

      .= v2 by RLVECT_1: 4;

      hence thesis by A7;

    end;

    theorem :: VECTSP_4:64

    

     Th64: (v + W) = (u + W) implies ex v1 st v1 in W & (v + v1) = u

    proof

      assume (v + W) = (u + W);

      then v in (u + W) by Th44;

      then

      consider u1 such that

       A1: v = (u + u1) and

       A2: u1 in W;

      take v1 = (u - v);

      ( 0. V) = ((u + u1) - v) by A1, VECTSP_1: 19

      .= (u1 + (u - v)) by RLVECT_1:def 3;

      then v1 = ( - u1) by VECTSP_1: 16;

      hence v1 in W by A2, Th22;

      

      thus (v + v1) = ((u + v) - v) by RLVECT_1:def 3

      .= (u + (v - v)) by RLVECT_1:def 3

      .= (u + ( 0. V)) by VECTSP_1: 19

      .= u by RLVECT_1: 4;

    end;

    theorem :: VECTSP_4:65

    

     Th65: (v + W) = (u + W) implies ex v1 st v1 in W & (v - v1) = u

    proof

      assume (v + W) = (u + W);

      then u in (v + W) by Th44;

      then

      consider u1 such that

       A1: u = (v + u1) and

       A2: u1 in W;

      take v1 = (v - u);

      ( 0. V) = ((v + u1) - u) by A1, VECTSP_1: 19

      .= (u1 + (v - u)) by RLVECT_1:def 3;

      then v1 = ( - u1) by VECTSP_1: 16;

      hence v1 in W by A2, Th22;

      

      thus (v - v1) = ((v - v) + u) by RLVECT_1: 29

      .= (( 0. V) + u) by VECTSP_1: 19

      .= u by RLVECT_1: 4;

    end;

    theorem :: VECTSP_4:66

    

     Th66: for W1,W2 be strict Subspace of V holds (v + W1) = (v + W2) iff W1 = W2

    proof

      let W1,W2 be strict Subspace of V;

      thus (v + W1) = (v + W2) implies W1 = W2

      proof

        assume

         A1: (v + W1) = (v + W2);

        the carrier of W1 = the carrier of W2

        proof

          

           A2: the carrier of W1 c= the carrier of V by Def2;

          thus the carrier of W1 c= the carrier of W2

          proof

            let x be object;

            assume

             A3: x in the carrier of W1;

            then

            reconsider y = x as Element of V by A2;

            set z = (v + y);

            x in W1 by A3;

            then z in (v + W2) by A1;

            then

            consider u such that

             A4: z = (v + u) and

             A5: u in W2;

            y = u by A4, RLVECT_1: 8;

            hence thesis by A5;

          end;

          let x be object;

          assume

           A6: x in the carrier of W2;

          the carrier of W2 c= the carrier of V by Def2;

          then

          reconsider y = x as Element of V by A6;

          set z = (v + y);

          x in W2 by A6;

          then z in (v + W1) by A1;

          then

          consider u such that

           A7: z = (v + u) and

           A8: u in W1;

          y = u by A7, RLVECT_1: 8;

          hence thesis by A8;

        end;

        hence thesis by Th29;

      end;

      thus thesis;

    end;

    theorem :: VECTSP_4:67

    

     Th67: for W1,W2 be strict Subspace of V st (v + W1) = (u + W2) holds W1 = W2

    proof

      let W1,W2 be strict Subspace of V;

      assume

       A1: (v + W1) = (u + W2);

      set V2 = the carrier of W2;

      set V1 = the carrier of W1;

      assume

       A2: W1 <> W2;

       A3:

      now

        set x = the Element of (V1 \ V2);

        assume (V1 \ V2) <> {} ;

        then x in V1 by XBOOLE_0:def 5;

        then

         A4: x in W1;

        then x in V by Th9;

        then

        reconsider x as Element of V;

        set z = (v + x);

        z in (u + W2) by A1, A4;

        then

        consider u1 such that

         A5: z = (u + u1) and

         A6: u1 in W2;

        x = (( 0. V) + x) by RLVECT_1: 4

        .= ((v + ( - v)) + x) by VECTSP_1: 19

        .= (( - v) + (u + u1)) by A5, RLVECT_1:def 3;

        then

         A7: ((v + (( - v) + (u + u1))) + W1) = (v + W1) by A4, Th53;

        (v + (( - v) + (u + u1))) = ((v + ( - v)) + (u + u1)) by RLVECT_1:def 3

        .= (( 0. V) + (u + u1)) by VECTSP_1: 19

        .= (u + u1) by RLVECT_1: 4;

        then ((u + u1) + W2) = ((u + u1) + W1) by A1, A6, A7, Th53;

        hence thesis by A2, Th66;

      end;

       A8:

      now

        set x = the Element of (V2 \ V1);

        assume (V2 \ V1) <> {} ;

        then x in V2 by XBOOLE_0:def 5;

        then

         A9: x in W2;

        then x in V by Th9;

        then

        reconsider x as Element of V;

        set z = (u + x);

        z in (v + W1) by A1, A9;

        then

        consider u1 such that

         A10: z = (v + u1) and

         A11: u1 in W1;

        x = (( 0. V) + x) by RLVECT_1: 4

        .= ((u + ( - u)) + x) by VECTSP_1: 19

        .= (( - u) + (v + u1)) by A10, RLVECT_1:def 3;

        then

         A12: ((u + (( - u) + (v + u1))) + W2) = (u + W2) by A9, Th53;

        (u + (( - u) + (v + u1))) = ((u + ( - u)) + (v + u1)) by RLVECT_1:def 3

        .= (( 0. V) + (v + u1)) by VECTSP_1: 19

        .= (v + u1) by RLVECT_1: 4;

        then ((v + u1) + W1) = ((v + u1) + W2) by A1, A11, A12, Th53;

        hence thesis by A2, Th66;

      end;

      V1 <> V2 by A2, Th29;

      then not V1 c= V2 or not V2 c= V1;

      hence thesis by A3, A8, XBOOLE_1: 37;

    end;

    theorem :: VECTSP_4:68

    ex C st v in C

    proof

      reconsider C = (v + W) as Coset of W by Def6;

      take C;

      thus thesis by Th44;

    end;

    theorem :: VECTSP_4:69

    C is linearly-closed iff C = the carrier of W

    proof

      thus C is linearly-closed implies C = the carrier of W

      proof

        assume

         A1: C is linearly-closed;

        consider v such that

         A2: C = (v + W) by Def6;

        C <> {} by A2, Th44;

        then ( 0. V) in (v + W) by A1, A2, Th1;

        hence thesis by A2, Th48;

      end;

      thus thesis by Lm2;

    end;

    theorem :: VECTSP_4:70

    for W1,W2 be strict Subspace of V, C1 be Coset of W1, C2 be Coset of W2 st C1 = C2 holds W1 = W2

    proof

      let W1,W2 be strict Subspace of V, C1 be Coset of W1, C2 be Coset of W2;

      (ex v1 st C1 = (v1 + W1)) & ex v2 st C2 = (v2 + W2) by Def6;

      hence thesis by Th67;

    end;

    theorem :: VECTSP_4:71

     {v} is Coset of ( (0). V)

    proof

      (v + ( (0). V)) = {v} by Th46;

      hence thesis by Def6;

    end;

    theorem :: VECTSP_4:72

    V1 is Coset of ( (0). V) implies ex v st V1 = {v}

    proof

      assume V1 is Coset of ( (0). V);

      then

      consider v such that

       A1: V1 = (v + ( (0). V)) by Def6;

      take v;

      thus thesis by A1, Th46;

    end;

    theorem :: VECTSP_4:73

    the carrier of W is Coset of W

    proof

      the carrier of W = (( 0. V) + W) by Lm3;

      hence thesis by Def6;

    end;

    theorem :: VECTSP_4:74

    the carrier of V is Coset of ( (Omega). V)

    proof

      set v = the Element of V;

      the carrier of V c= the carrier of V;

      then

      reconsider A = the carrier of V as Subset of V;

      A = (v + ( (Omega). V)) by Th47;

      hence thesis by Def6;

    end;

    theorem :: VECTSP_4:75

    V1 is Coset of ( (Omega). V) implies V1 = the carrier of V

    proof

      assume V1 is Coset of ( (Omega). V);

      then ex v st V1 = (v + ( (Omega). V)) by Def6;

      hence thesis by Th47;

    end;

    theorem :: VECTSP_4:76

    ( 0. V) in C iff C = the carrier of W

    proof

      ex v st C = (v + W) by Def6;

      hence thesis by Th48;

    end;

    theorem :: VECTSP_4:77

    

     Th77: u in C iff C = (u + W)

    proof

      thus u in C implies C = (u + W)

      proof

        assume

         A1: u in C;

        ex v st C = (v + W) by Def6;

        hence thesis by A1, Th55;

      end;

      thus thesis by Th44;

    end;

    theorem :: VECTSP_4:78

    u in C & v in C implies ex v1 st v1 in W & (u + v1) = v

    proof

      assume u in C & v in C;

      then C = (u + W) & C = (v + W) by Th77;

      hence thesis by Th64;

    end;

    theorem :: VECTSP_4:79

    u in C & v in C implies ex v1 st v1 in W & (u - v1) = v

    proof

      assume u in C & v in C;

      then C = (u + W) & C = (v + W) by Th77;

      hence thesis by Th65;

    end;

    theorem :: VECTSP_4:80

    (ex C st v1 in C & v2 in C) iff (v1 - v2) in W

    proof

      thus (ex C st v1 in C & v2 in C) implies (v1 - v2) in W

      proof

        given C such that

         A1: v1 in C & v2 in C;

        ex v st C = (v + W) by Def6;

        hence thesis by A1, Th63;

      end;

      assume (v1 - v2) in W;

      then

      consider v such that

       A2: v1 in (v + W) & v2 in (v + W) by Th63;

      reconsider C = (v + W) as Coset of W by Def6;

      take C;

      thus thesis by A2;

    end;

    theorem :: VECTSP_4:81

    u in B & u in C implies B = C

    proof

      assume

       A1: u in B & u in C;

      (ex v1 st B = (v1 + W)) & ex v2 st C = (v2 + W) by Def6;

      hence thesis by A1, Th56;

    end;

    theorem :: VECTSP_4:82

    for GF be add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive non empty doubleLoopStr, V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF, a,b be Element of GF, v be Element of V holds ((a - b) * v) = ((a * v) - (b * v)) by Lm1;