vectsp_2.miz



    begin

    reserve FS for non empty doubleLoopStr;

    reserve F for Field;

    

     Lm1: for L be non empty multLoopStr st L is well-unital holds ( 1. L) = ( 1_ L) by GROUP_1:def 4;

    registration

      cluster strict Abelian add-associative right_zeroed right_complementable unital distributive for non empty doubleLoopStr;

      existence

      proof

        set F = the strict Field;

        F is unital distributive;

        hence thesis;

      end;

    end

    definition

      let IT be non empty multLoopStr_0;

      :: VECTSP_2:def1

      attr IT is domRing-like means

      : Def1: for x,y be Element of IT holds (x * y) = ( 0. IT) implies x = ( 0. IT) or y = ( 0. IT);

    end

    registration

      cluster strict non degenerated commutative almost_left_invertible domRing-like for Ring;

      existence

      proof

        set F = the strict Field;

        for x,y be Scalar of F holds (x * y) = ( 0. F) implies x = ( 0. F) or y = ( 0. F) by VECTSP_1: 12;

        then F is domRing-like;

        hence thesis;

      end;

    end

    definition

      mode comRing is commutative Ring;

    end

    definition

      mode domRing is domRing-like non degenerated comRing;

    end

    theorem :: VECTSP_2:1

    F is domRing

    proof

      for x,y be Scalar of F holds (x * y) = ( 0. F) implies x = ( 0. F) or y = ( 0. F) by VECTSP_1: 12;

      hence thesis by Def1;

    end;

    registration

      cluster commutative left_unital -> well-unital for non empty multLoopStr;

      coherence

      proof

        let F be non empty multLoopStr;

        assume

         A1: F is commutative left_unital;

        let x be Scalar of F;

        for F be commutative non empty multMagma, x,y be Element of F holds (x * y) = (y * x);

        then (x * ( 1. F)) = (( 1. F) * x) by A1;

        hence thesis by A1;

      end;

      cluster commutative right_unital -> well-unital for non empty multLoopStr;

      coherence

      proof

        let F be non empty multLoopStr;

        assume

         A2: F is commutative right_unital;

        let x be Element of F;

        for F be commutative non empty multMagma, x,y be Element of F holds (x * y) = (y * x);

        then (x * ( 1. F)) = (( 1. F) * x) by A2;

        hence thesis by A2;

      end;

    end

    reserve R for Abelian add-associative right_zeroed right_complementable non empty addLoopStr,

x,y,z for Scalar of R;

    

     Lm2: (x + y) = z implies x = (z - y)

    proof

      assume

       A1: (x + y) = z;

      

      thus x = (x + ( 0. R)) by RLVECT_1: 4

      .= (x + (y + ( - y))) by RLVECT_1:def 10

      .= (z - y) by A1, RLVECT_1:def 3;

    end;

    

     Lm3: x = (z - y) implies (x + y) = z

    proof

      assume x = (z - y);

      

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

      .= (z + ( 0. R)) by RLVECT_1:def 10

      .= z by RLVECT_1: 4;

      hence thesis;

    end;

    theorem :: VECTSP_2:2

    ((x + y) = z iff x = (z - y)) & ((x + y) = z iff y = (z - x)) by Lm2, Lm3;

    theorem :: VECTSP_2:3

    

     Th3: for R be add-associative right_zeroed right_complementable non empty addLoopStr, x be Element of R holds x = ( 0. R) iff ( - x) = ( 0. R)

    proof

      let R be add-associative right_zeroed right_complementable non empty addLoopStr, x be Element of R;

      thus x = ( 0. R) implies ( - x) = ( 0. R) by RLVECT_1: 12;

      assume ( - x) = ( 0. R);

      then ( - ( - x)) = ( 0. R) by RLVECT_1: 12;

      hence thesis by RLVECT_1: 17;

    end;

    theorem :: VECTSP_2:4

    for R be add-associative right_zeroed Abelian right_complementable non empty addLoopStr holds for x,y be Element of R holds ex z be Element of R st x = (y + z) & x = (z + y)

    proof

      let R be add-associative right_zeroed Abelian right_complementable non empty addLoopStr;

      let x,y be Element of R;

      take z = (( - y) + x);

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

      .= (x + ( 0. R)) by RLVECT_1: 5

      .= x by RLVECT_1: 4;

      hence thesis;

    end;

    reserve SF for Skew-Field,

x,y,z for Scalar of SF;

    theorem :: VECTSP_2:5

    for F be add-associative right_zeroed right_complementable distributive non degenerated non empty doubleLoopStr holds for x,y be Element of F holds (x * y) = ( 1. F) implies x <> ( 0. F) & y <> ( 0. F);

    theorem :: VECTSP_2:6

    

     Th6: for SF be non degenerated almost_left_invertible associative add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr, x be Element of SF holds x <> ( 0. SF) implies ex y be Element of SF st (x * y) = ( 1. SF)

    proof

      let SF be non degenerated almost_left_invertible associative add-associative right_zeroed right_complementable well-unital right_unital distributive non empty doubleLoopStr, x be Element of SF;

      assume x <> ( 0. SF);

      then

      consider y be Element of SF such that

       A1: (y * x) = ( 1. SF) by VECTSP_1:def 9;

      take y;

      y <> ( 0. SF) by A1;

      then

      consider z be Element of SF such that

       A2: (z * y) = ( 1. SF) by VECTSP_1:def 9;

      z = (z * (y * x)) by A1

      .= (( 1. SF) * x) by A2, GROUP_1:def 3

      .= x;

      hence thesis by A2;

    end;

    theorem :: VECTSP_2:7

    

     Th7: for SF be add-associative right_zeroed right_complementable distributive non degenerated almost_left_invertible associative well-unital non empty doubleLoopStr holds for x,y be Element of SF st (y * x) = ( 1. SF) holds (x * y) = ( 1. SF)

    proof

      let SF be non degenerated almost_left_invertible associative add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr;

      let x,y be Element of SF;

      assume

       A1: (y * x) = ( 1. SF);

      then x <> ( 0. SF);

      then

      consider z be Element of SF such that

       A2: (x * z) = ( 1_ SF) by Th6;

      y = (y * (x * z)) by A2

      .= (( 1_ SF) * z) by A1, GROUP_1:def 3

      .= z;

      hence thesis by A2;

    end;

    theorem :: VECTSP_2:8

    

     Th8: for SF be non degenerated almost_left_invertible associative Abelian add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr, x,y,z be Element of SF holds (x * y) = (x * z) & x <> ( 0. SF) implies y = z

    proof

      let SF be non degenerated almost_left_invertible associative Abelian add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr, x,y,z be Element of SF;

      assume that

       A1: (x * y) = (x * z) and

       A2: x <> ( 0. SF);

      consider u be Element of SF such that

       A3: (x * u) = ( 1_ SF) by A2, Th6;

      

       A4: (u * x) = ( 1_ SF) by A3, Th7;

      

      then y = ((u * x) * y)

      .= (u * (x * z)) by A1, GROUP_1:def 3

      .= (( 1_ SF) * z) by A4, GROUP_1:def 3

      .= z;

      hence thesis;

    end;

    notation

      let SF be non degenerated almost_left_invertible associative add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr, x be Element of SF;

      synonym x " for / x;

    end

    definition

      let SF be non degenerated almost_left_invertible associative add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr, x be Element of SF;

      assume

       A1: x <> ( 0. SF);

      :: original: "

      redefine

      :: VECTSP_2:def2

      func x " means

      : Def2: (it * x) = ( 1. SF);

      compatibility

      proof

        let IT be Element of SF;

        

         A2: x is left_invertible by A1, ALGSTR_0:def 39;

        then

        consider y be Element of SF such that

         A3: (y * x) = ( 1. SF);

        x is right_invertible

        proof

          take y;

          thus thesis by A3, Th7;

        end;

        then

        consider x1 be Element of SF such that

         A4: (x * x1) = ( 1. SF);

        x is right_mult-cancelable

        proof

          let y,z be Element of SF;

          assume

           A5: (y * x) = (z * x);

          

          thus y = (y * ( 1. SF))

          .= ((z * x) * x1) by A4, A5, GROUP_1:def 3

          .= (z * ( 1. SF)) by A4, GROUP_1:def 3

          .= z;

        end;

        hence thesis by A2, ALGSTR_0:def 30;

      end;

    end

    ::$Canceled

    theorem :: VECTSP_2:9

    

     Th9: x <> ( 0. SF) implies (x * (x " )) = ( 1. SF) & ((x " ) * x) = ( 1. SF)

    proof

      assume x <> ( 0. SF);

      then ((x " ) * x) = ( 1_ SF) by Def2;

      hence thesis by Th7;

    end;

    theorem :: VECTSP_2:10

    

     Th10: (y * x) = ( 1_ SF) implies x = (y " ) & y = (x " )

    proof

      

       A1: (y * x) = ( 1_ SF) implies y = (x " )

      proof

        assume

         A2: (y * x) = ( 1_ SF);

        then x <> ( 0. SF);

        hence thesis by A2, Def2;

      end;

      (y * x) = ( 1_ SF) implies x = (y " )

      proof

        assume (y * x) = ( 1_ SF);

        then y <> ( 0. SF) & (x * y) = ( 1_ SF) by Th7;

        hence thesis by Def2;

      end;

      hence thesis by A1;

    end;

    theorem :: VECTSP_2:11

    

     Th11: x <> ( 0. SF) & y <> ( 0. SF) implies ((x " ) * (y " )) = ((y * x) " )

    proof

      assume

       A1: x <> ( 0. SF);

      assume

       A2: y <> ( 0. SF);

      (((x " ) * (y " )) * (y * x)) = ((x " ) * ((y " ) * (y * x))) by GROUP_1:def 3

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

      .= ((x " ) * (( 1_ SF) * x)) by A2, Th9

      .= ((x " ) * x)

      .= ( 1_ SF) by A1, Th9;

      hence thesis by Th10;

    end;

    theorem :: VECTSP_2:12

    (x * y) = ( 0. SF) implies x = ( 0. SF) or y = ( 0. SF)

    proof

      now

        assume that

         A1: (x * y) = ( 0. SF) and

         A2: x <> ( 0. SF);

        (x * y) = (x * ( 0. SF)) by A1;

        hence y = ( 0. SF) by A2, Th8;

      end;

      hence thesis;

    end;

    theorem :: VECTSP_2:13

    

     Th13: x <> ( 0. SF) implies (x " ) <> ( 0. SF)

    proof

      assume

       A1: x <> ( 0. SF);

      assume (x " ) = ( 0. SF);

      then (x * (x " )) = ( 0. SF);

      then ( 1. SF) = ( 0. SF) by A1, Th9;

      hence contradiction;

    end;

    theorem :: VECTSP_2:14

    

     Th14: x <> ( 0. SF) implies ((x " ) " ) = x

    proof

      assume

       A1: x <> ( 0. SF);

      then

       A2: (x " ) <> ( 0. SF) by Th13;

      ((x " ) " ) = (((x " ) " ) * ( 1_ SF))

      .= (((x " ) " ) * ((x " ) * x)) by A1, Th9

      .= ((((x " ) " ) * (x " )) * x) by GROUP_1:def 3;

      then ((x " ) " ) = (( 1_ SF) * x) by A2, Th9;

      hence thesis;

    end;

    theorem :: VECTSP_2:15

    x <> ( 0. SF) implies (( 1_ SF) / x) = (x " ) & (( 1_ SF) / (x " )) = x by Th14;

    theorem :: VECTSP_2:16

    x <> ( 0. SF) implies (x * (( 1_ SF) / x)) = ( 1_ SF) & ((( 1_ SF) / x) * x) = ( 1_ SF) by Th9;

    theorem :: VECTSP_2:17

    x <> ( 0. SF) implies (x / x) = ( 1_ SF) by Th9;

    theorem :: VECTSP_2:18

    

     Th18: y <> ( 0. SF) & z <> ( 0. SF) implies (x / y) = ((x * z) / (y * z))

    proof

      assume

       A1: y <> ( 0. SF);

      assume

       A2: z <> ( 0. SF);

      

      thus (x / y) = ((x * ( 1_ SF)) * (y " ))

      .= ((x * (z * (z " ))) * (y " )) by A2, Th9

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

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

      .= ((x * z) / (y * z)) by A1, A2, Th11;

    end;

    theorem :: VECTSP_2:19

    

     Th19: y <> ( 0. SF) implies ( - (x / y)) = (( - x) / y) & (x / ( - y)) = ( - (x / y))

    proof

      assume y <> ( 0. SF);

      then

       A1: ( - y) <> ( 0. SF) by Th3;

      thus

       A2: ( - (x / y)) = (( - x) / y) by VECTSP_1: 9;

      ( - ( 1. SF)) <> ( 0. SF) by Th3;

      then (x / ( - y)) = ((x * ( - ( 1_ SF))) / (( - y) * ( - ( 1_ SF)))) by A1, Th18;

      

      then (x / ( - y)) = (( - (x * ( 1_ SF))) / (( - y) * ( - ( 1_ SF)))) by VECTSP_1: 8

      .= (( - x) / (( - y) * ( - ( 1_ SF))))

      .= (( - x) / ( - (( - y) * ( 1_ SF)))) by VECTSP_1: 8

      .= (( - x) / (( - ( - y)) * ( 1_ SF)))

      .= (( - x) / (y * ( 1_ SF))) by RLVECT_1: 17

      .= ( - (x / y)) by A2;

      hence thesis;

    end;

    theorem :: VECTSP_2:20

    z <> ( 0. SF) implies ((x / z) + (y / z)) = ((x + y) / z) & ((x / z) - (y / z)) = ((x - y) / z)

    proof

      z <> ( 0. SF) implies ((x / z) - (y / z)) = ((x - y) / z)

      proof

        assume z <> ( 0. SF);

        

        hence ((x / z) - (y / z)) = ((x / z) + (( - y) / z)) by Th19

        .= ((x - y) / z) by VECTSP_1:def 7;

      end;

      hence thesis by VECTSP_1:def 7;

    end;

    theorem :: VECTSP_2:21

    y <> ( 0. SF) & z <> ( 0. SF) implies (x / (y / z)) = ((x * z) / y)

    proof

      assume

       A1: y <> ( 0. SF);

      assume

       A2: z <> ( 0. SF);

      then (z " ) <> ( 0. SF) by Th13;

      

      hence (x / (y / z)) = (x * (((z " ) " ) * (y " ))) by A1, Th11

      .= (x * (z * (y " ))) by A2, Th14

      .= ((x * z) / y) by GROUP_1:def 3;

    end;

    theorem :: VECTSP_2:22

    y <> ( 0. SF) implies ((x / y) * y) = x

    proof

      assume

       A1: y <> ( 0. SF);

      

      thus ((x / y) * y) = (x * ((y " ) * y)) by GROUP_1:def 3

      .= (x * ( 1_ SF)) by A1, Th9

      .= x;

    end;

    definition

      let FS be 1-sorted;

      struct ( addLoopStr) RightModStr over FS (# the carrier -> set,

the addF -> BinOp of the carrier,

the ZeroF -> Element of the carrier,

the rmult -> Function of [: the carrier, the carrier of FS:], the carrier #)

       attr strict strict;

    end

    registration

      let FS be 1-sorted;

      cluster non empty for RightModStr over FS;

      existence

      proof

        set A = the non empty set, a = the BinOp of A, Z = the Element of A, r = the Function of [:A, the carrier of FS:], A;

        take RightModStr (# A, a, Z, r #);

        thus the carrier of RightModStr (# A, a, Z, r #) is non empty;

      end;

    end

    registration

      let FS be 1-sorted;

      let A be non empty set, a be BinOp of A, Z be Element of A, r be Function of [:A, the carrier of FS:], A;

      cluster RightModStr (# A, a, Z, r #) -> non empty;

      coherence ;

    end

    definition

      let FS;

      let RMS be non empty RightModStr over FS;

      mode Scalar of RMS is Element of FS;

      mode Vector of RMS is Element of RMS;

    end

    definition

      let FS1,FS2 be 1-sorted;

      struct ( ModuleStr over FS1, RightModStr over FS2) BiModStr over FS1,FS2 (# the carrier -> set,

the addF -> BinOp of the carrier,

the ZeroF -> Element of the carrier,

the lmult -> Function of [:the carrier of FS1, the carrier:], the carrier,

the rmult -> Function of [: the carrier, the carrier of FS2:], the carrier #)

       attr strict strict;

    end

    registration

      let FS1,FS2 be 1-sorted;

      cluster non empty for BiModStr over FS1, FS2;

      existence

      proof

        set A = the non empty set, a = the BinOp of A, Z = the Element of A, l = the Function of [:the carrier of FS1, A:], A, r = the Function of [:A, the carrier of FS2:], A;

        take BiModStr (# A, a, Z, l, r #);

        thus the carrier of BiModStr (# A, a, Z, l, r #) is non empty;

      end;

    end

    registration

      let FS1,FS2 be 1-sorted;

      let A be non empty set, a be BinOp of A, Z be Element of A, l be Function of [:the carrier of FS1, A:], A, r be Function of [:A, the carrier of FS2:], A;

      cluster BiModStr (# A, a, Z, l, r #) -> non empty;

      coherence ;

    end

    reserve R,R1,R2 for Ring;

    definition

      let R be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      :: VECTSP_2:def3

      func AbGr R -> strict AbGroup equals addLoopStr (# the carrier of R, the addF of R, ( 0. R) #);

      coherence

      proof

        reconsider IT = addLoopStr (# the carrier of R, the addF of R, ( 0. R) #) as non empty addLoopStr;

        

         A1: for x,y,z be Element of IT holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. IT)) = x & ex v be Element of IT st (x + v) = ( 0. IT)

        proof

          let x,y,z be Element of IT;

          reconsider x9 = x, y9 = y, z9 = z as Scalar of R;

          

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

          .= (y + x);

          

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

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

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

          

          thus (x + ( 0. IT)) = (x9 + ( 0. R))

          .= x by RLVECT_1: 4;

          consider b be Scalar of R such that

           A2: (x9 + b) = ( 0. R) by ALGSTR_0:def 11;

          reconsider b9 = b as Element of IT;

          take b9;

          thus thesis by A2;

        end;

        IT is right_complementable

        proof

          let x be Element of IT;

          reconsider x9 = x as Scalar of R;

          consider b be Scalar of R such that

           A3: (x9 + b) = ( 0. R) by ALGSTR_0:def 11;

          reconsider b9 = b as Element of IT;

          take b9;

          thus thesis by A3;

        end;

        hence thesis by A1, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

      end;

    end

    deffunc LEFTMODULE( Ring) = ModuleStr (# the carrier of $1, the addF of $1, ( 0. $1), the multF of $1 #);

    

     Lm4: LEFTMODULE(R) is Abelian add-associative right_zeroed right_complementable

    proof

      

       A1: for x,y,z be Scalar of R holds for x9,y9,z9 be Element of LEFTMODULE(R) st x = x9 & y = y9 & z = z9 holds (x + y) = (x9 + y9);

      thus LEFTMODULE(R) is Abelian

      proof

        let x,y be Element of LEFTMODULE(R);

        reconsider x9 = x, y9 = y as Scalar of R;

        

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

        .= (y + x);

      end;

      thus LEFTMODULE(R) is add-associative

      proof

        let x,y,z be Element of LEFTMODULE(R);

        reconsider x9 = x, y9 = y, z9 = z as Scalar of R;

        

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

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

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

      end;

      thus LEFTMODULE(R) is right_zeroed

      proof

        let x be Element of LEFTMODULE(R);

        reconsider x9 = x as Scalar of R;

        

        thus (x + ( 0. LEFTMODULE(R))) = (x9 + ( 0. R))

        .= x by RLVECT_1: 4;

      end;

      let x be Element of LEFTMODULE(R);

      reconsider x9 = x as Scalar of R;

      consider b9 be Scalar of R such that

       A2: (x9 + b9) = ( 0. R) by ALGSTR_0:def 11;

      reconsider b = b9 as Element of LEFTMODULE(R);

      take b;

      thus thesis by A2;

    end;

    registration

      let R;

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

      existence

      proof

         LEFTMODULE(R) is Abelian add-associative right_zeroed right_complementable by Lm4;

        hence thesis;

      end;

    end

    definition

      let R;

      :: VECTSP_2:def4

      func LeftModule R -> Abelian add-associative right_zeroed right_complementable strict non empty ModuleStr over R equals ModuleStr (# the carrier of R, the addF of R, ( 0. R), the multF of R #);

      coherence by Lm4;

    end

    deffunc RIGHTMODULE( Ring) = RightModStr (# the carrier of $1, the addF of $1, ( 0. $1), the multF of $1 #);

    

     Lm5: RIGHTMODULE(R) is Abelian add-associative right_zeroed right_complementable

    proof

      

       A1: for x,y,z be Scalar of R holds for x9,y9,z9 be Element of RIGHTMODULE(R) st x = x9 & y = y9 & z = z9 holds (x + y) = (x9 + y9);

      thus RIGHTMODULE(R) is Abelian

      proof

        let x,y be Element of RIGHTMODULE(R);

        reconsider x9 = x, y9 = y as Scalar of R;

        

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

        .= (y + x);

      end;

      thus RIGHTMODULE(R) is add-associative

      proof

        let x,y,z be Element of RIGHTMODULE(R);

        reconsider x9 = x, y9 = y, z9 = z as Scalar of R;

        

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

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

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

      end;

      thus RIGHTMODULE(R) is right_zeroed

      proof

        let x be Element of RIGHTMODULE(R);

        reconsider x9 = x as Scalar of R;

        

        thus (x + ( 0. RIGHTMODULE(R))) = (x9 + ( 0. R))

        .= x by RLVECT_1: 4;

      end;

      let x be Element of RIGHTMODULE(R);

      reconsider x9 = x as Scalar of R;

      consider b9 be Scalar of R such that

       A2: (x9 + b9) = ( 0. R) by ALGSTR_0:def 11;

      reconsider b = b9 as Element of RIGHTMODULE(R);

      take b;

      thus thesis by A2;

    end;

    registration

      let R;

      cluster Abelian add-associative right_zeroed right_complementable strict for non empty RightModStr over R;

      existence

      proof

         RIGHTMODULE(R) is Abelian add-associative right_zeroed right_complementable by Lm5;

        hence thesis;

      end;

    end

    definition

      let R;

      :: VECTSP_2:def5

      func RightModule R -> Abelian add-associative right_zeroed right_complementable strict non empty RightModStr over R equals RightModStr (# the carrier of R, the addF of R, ( 0. R), the multF of R #);

      coherence by Lm5;

    end

    definition

      let R be non empty 1-sorted, V be non empty RightModStr over R;

      let x be Element of R;

      let v be Element of V;

      :: VECTSP_2:def6

      func v * x -> Element of V equals (the rmult of V . (v,x));

      coherence ;

    end

    deffunc BIMODULE( Ring, Ring) = BiModStr (# { 0 }, op2 , op0 , ( pr2 (the carrier of $1, { 0 })), ( pr1 ( { 0 },the carrier of $2)) #);

    

     Lm6: BIMODULE(R1,R2) is Abelian add-associative right_zeroed right_complementable

    proof

      set G = BiModStr (# { 0 }, op2 , op0 , ( pr2 (the carrier of R1, { 0 })), ( pr1 ( { 0 },the carrier of R2)) #);

       A1:

      now

        let x,y,z be Element of G;

        

         A2: (x + ( 0. G)) = {} by TARSKI:def 1;

        (x + y) = {} & ((x + y) + z) = {} by TARSKI:def 1;

        hence (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. G)) = x & ex x9 be Element of G st (x + x9) = ( 0. G) by A2, TARSKI:def 1;

      end;

      G is right_complementable

      proof

        let x be Element of G;

        take x;

        thus thesis by TARSKI:def 1;

      end;

      hence thesis by A1;

    end;

    registration

      let R1, R2;

      cluster Abelian add-associative right_zeroed right_complementable strict for non empty BiModStr over R1, R2;

      existence

      proof

         BIMODULE(R1,R2) is Abelian add-associative right_zeroed right_complementable by Lm6;

        hence thesis;

      end;

    end

    definition

      let R1, R2;

      :: VECTSP_2:def7

      func BiModule (R1,R2) -> Abelian add-associative right_zeroed right_complementable strict non empty BiModStr over R1, R2 equals BiModStr (# { 0 }, op2 , op0 , ( pr2 (the carrier of R1, { 0 })), ( pr1 ( { 0 },the carrier of R2)) #);

      coherence by Lm6;

    end

    theorem :: VECTSP_2:23

    

     Th23: for x,y be Scalar of R holds for v,w be Vector of ( LeftModule R) holds (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1. R) * v) = v

    proof

      set MLT = the multF of R;

      set LS = ModuleStr (# the carrier of R, the addF of R, ( 0. R), MLT #);

      for x,y be Scalar of R holds for v,w be Vector of LS holds (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1_ R) * v) = v

      proof

        let x,y be Scalar of R;

        let v,w be Vector of LS;

        reconsider v9 = v, w9 = w as Scalar of R;

        

        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

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

        

        thus (( 1_ R) * v) = (( 1_ R) * v9)

        .= v;

      end;

      hence thesis;

    end;

    registration

      let R;

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

      existence

      proof

        take ( LeftModule R);

        thus for x be Scalar of R holds for v,w be Vector of ( LeftModule R) holds (x * (v + w)) = ((x * v) + (x * w)) by Th23;

        thus for x,y be Scalar of R holds for v be Vector of ( LeftModule R) holds ((x + y) * v) = ((x * v) + (y * v)) by Th23;

        thus for x,y be Scalar of R holds for v be Vector of ( LeftModule R) holds ((x * y) * v) = (x * (y * v)) by Th23;

        thus for v be Vector of ( LeftModule R) holds (( 1. R) * v) = v by Th23;

        thus thesis;

      end;

    end

    definition

      let R;

      mode LeftMod of R is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over R;

    end

    

     Lm7: ( LeftModule R) is vector-distributive scalar-distributive scalar-associative scalar-unital by Th23;

    registration

      let R;

      cluster ( LeftModule R) -> Abelian add-associative right_zeroed right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Lm7;

    end

    theorem :: VECTSP_2:24

    

     Th24: for x,y be Scalar of R holds for v,w be Vector of ( RightModule R) holds ((v + w) * x) = ((v * x) + (w * x)) & (v * (x + y)) = ((v * x) + (v * y)) & (v * (y * x)) = ((v * y) * x) & (v * ( 1_ R)) = v

    proof

      set MLT = the multF of R;

      set LS = RightModStr (# the carrier of R, the addF of R, ( 0. R), MLT #);

      for x,y be Scalar of R holds for v,w be Vector of LS holds ((v + w) * x) = ((v * x) + (w * x)) & (v * (x + y)) = ((v * x) + (v * y)) & (v * (y * x)) = ((v * y) * x) & (v * ( 1_ R)) = v

      proof

        let x,y be Scalar of R;

        let v,w be Vector of LS;

        reconsider v9 = v, w9 = w as Scalar of R;

        

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

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

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

        

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

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

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

        

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

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

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

        

        thus (v * ( 1_ R)) = (v9 * ( 1_ R))

        .= v;

      end;

      hence thesis;

    end;

    definition

      let R be non empty doubleLoopStr;

      let IT be non empty RightModStr over R;

      :: VECTSP_2:def8

      attr IT is RightMod-like means

      : Def8: for x,y be Scalar of R holds for v,w be Vector of IT holds ((v + w) * x) = ((v * x) + (w * x)) & (v * (x + y)) = ((v * x) + (v * y)) & (v * (y * x)) = ((v * y) * x) & (v * ( 1_ R)) = v;

    end

    registration

      let R;

      cluster Abelian add-associative right_zeroed right_complementable RightMod-like strict for non empty RightModStr over R;

      existence

      proof

        take ( RightModule R);

        thus ( RightModule R) is Abelian add-associative right_zeroed right_complementable;

        thus for x,y be Scalar of R holds for v,w be Vector of ( RightModule R) holds ((v + w) * x) = ((v * x) + (w * x)) & (v * (x + y)) = ((v * x) + (v * y)) & (v * (y * x)) = ((v * y) * x) & (v * ( 1_ R)) = v by Th24;

        thus thesis;

      end;

    end

    definition

      let R;

      mode RightMod of R is Abelian add-associative right_zeroed right_complementable RightMod-like non empty RightModStr over R;

    end

    

     Lm8: ( RightModule R) is RightMod-like by Th24;

    registration

      let R;

      cluster ( RightModule R) -> Abelian add-associative right_zeroed right_complementable RightMod-like;

      coherence by Lm8;

    end

    

     Lm9: for x,y be Scalar of R1 holds for p,q be Scalar of R2 holds for v,w be Vector of ( BiModule (R1,R2)) holds (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1_ R1) * v) = v & ((v + w) * p) = ((v * p) + (w * p)) & (v * (p + q)) = ((v * p) + (v * q)) & (v * (q * p)) = ((v * q) * p) & (v * ( 1_ R2)) = v & (x * (v * p)) = ((x * v) * p)

    proof

      set a = {} ;

      set G = ( BiModule (R1,R2));

      let x,y be Scalar of R1, p,q be Scalar of R2, v,w be Vector of G;

      

       A1: ((x * y) * v) = a & (( 1_ R1) * v) = a by TARSKI:def 1;

      (x * (v + w)) = a & ((x + y) * v) = a by TARSKI:def 1;

      hence (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1_ R1) * v) = v by A1, TARSKI:def 1;

      

       A2: (v * (q * p)) = a & (v * ( 1_ R2)) = a by TARSKI:def 1;

      

       A3: (x * (v * p)) = a by TARSKI:def 1;

      ((v + w) * p) = a & (v * (p + q)) = a by TARSKI:def 1;

      hence thesis by A2, A3, TARSKI:def 1;

    end;

    definition

      let R1, R2;

      let IT be non empty BiModStr over R1, R2;

      :: VECTSP_2:def9

      attr IT is BiMod-like means

      : Def9: for x be Scalar of R1 holds for p be Scalar of R2 holds for v be Vector of IT holds (x * (v * p)) = ((x * v) * p);

    end

    registration

      let R1, R2;

      cluster Abelian add-associative right_zeroed right_complementable RightMod-like vector-distributive scalar-distributive scalar-associative scalar-unital BiMod-like strict for non empty BiModStr over R1, R2;

      existence

      proof

        take ( BiModule (R1,R2));

        thus ( BiModule (R1,R2)) is Abelian add-associative right_zeroed right_complementable;

        for x,y be Scalar of R1 holds for p,q be Scalar of R2 holds for v,w be Vector of ( BiModule (R1,R2)) holds (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1_ R1) * v) = v & ((v + w) * p) = ((v * p) + (w * p)) & (v * (p + q)) = ((v * p) + (v * q)) & (v * (q * p)) = ((v * q) * p) & (v * ( 1_ R2)) = v & (x * (v * p)) = ((x * v) * p) by Lm9;

        hence thesis;

      end;

    end

    definition

      let R1, R2;

      mode BiMod of R1,R2 is Abelian add-associative right_zeroed right_complementable RightMod-like vector-distributive scalar-distributive scalar-associative scalar-unital BiMod-like non empty BiModStr over R1, R2;

    end

    theorem :: VECTSP_2:25

    for V be non empty BiModStr over R1, R2 holds (for x,y be Scalar of R1 holds for p,q be Scalar of R2 holds for v,w be Vector of V holds (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1_ R1) * v) = v & ((v + w) * p) = ((v * p) + (w * p)) & (v * (p + q)) = ((v * p) + (v * q)) & (v * (q * p)) = ((v * q) * p) & (v * ( 1_ R2)) = v & (x * (v * p)) = ((x * v) * p)) iff V is RightMod-like vector-distributive scalar-distributive scalar-associative scalar-unital BiMod-like;

    theorem :: VECTSP_2:26

    

     Th26: ( BiModule (R1,R2)) is BiMod of R1, R2

    proof

      for x,y be Scalar of R1, p,q be Scalar of R2, v,w be Vector of ( BiModule (R1,R2)) holds (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1_ R1) * v) = v & ((v + w) * p) = ((v * p) + (w * p)) & (v * (p + q)) = ((v * p) + (v * q)) & (v * (q * p)) = ((v * q) * p) & (v * ( 1_ R2)) = v & (x * (v * p)) = ((x * v) * p) by Lm9;

      hence thesis by Def8, Def9, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

    end;

    registration

      let R1, R2;

      cluster ( BiModule (R1,R2)) -> Abelian add-associative right_zeroed right_complementable RightMod-like vector-distributive scalar-distributive scalar-associative scalar-unital BiMod-like;

      coherence by Th26;

    end

    theorem :: VECTSP_2:27

    for L be non empty multLoopStr st L is well-unital holds ( 1. L) = ( 1_ L) by Lm1;

    begin

    theorem :: VECTSP_2:28

    for K be add-associative right_zeroed right_complementable right-distributive right_unital non empty doubleLoopStr holds for a be Element of K holds (a * ( - ( 1. K))) = ( - a)

    proof

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

      let x be Element of K;

      

      thus (x * ( - ( 1. K))) = (x * (( 0. K) - ( 1. K))) by RLVECT_1: 14

      .= ((x * ( 0. K)) - (x * ( 1. K))) by VECTSP_1: 11

      .= (( 0. K) - (x * ( 1. K)))

      .= ( - (x * ( 1. K))) by RLVECT_1: 14

      .= ( - x);

    end;

    theorem :: VECTSP_2:29

    for K be add-associative right_zeroed right_complementable left-distributive left_unital non empty doubleLoopStr holds for a be Element of K holds (( - ( 1. K)) * a) = ( - a)

    proof

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

      let x be Element of K;

      

      thus (( - ( 1. K)) * x) = ((( 0. K) - ( 1. K)) * x) by RLVECT_1: 14

      .= ((( 0. K) * x) - (( 1. K) * x)) by VECTSP_1: 13

      .= (( 0. K) - (( 1. K) * x))

      .= ( - (( 1. K) * x)) by RLVECT_1: 14

      .= ( - x);

    end;

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

F for non degenerated almost_left_invertible Ring,

x for Scalar of F,

V for add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F,

v for Vector of V;

    theorem :: VECTSP_2:30

    (x * v) = ( 0. V) iff x = ( 0. F) or v = ( 0. V)

    proof

      (x * v) = ( 0. V) implies x = ( 0. F) or v = ( 0. V)

      proof

        assume (x * v) = ( 0. V);

        

        then

         A1: (((x " ) * x) * v) = ((x " ) * ( 0. V)) by VECTSP_1:def 16

        .= ( 0. V) by VECTSP_1: 14;

        assume x <> ( 0. F);

        then ( 0. V) = (( 1_ F) * v) by A1, Th9;

        hence thesis by VECTSP_1:def 17;

      end;

      hence thesis by VECTSP_1: 14;

    end;

    theorem :: VECTSP_2:31

    x <> ( 0. F) implies ((x " ) * (x * v)) = v

    proof

      assume

       A1: x <> ( 0. F);

      ((x " ) * (x * v)) = (((x " ) * x) * v) by VECTSP_1:def 16

      .= (( 1_ F) * v) by A1, Th9

      .= v by VECTSP_1:def 17;

      hence thesis;

    end;

    reserve V for add-associative right_zeroed right_complementable RightMod-like non empty RightModStr over R;

    reserve x for Scalar of R;

    reserve v,w for Vector of V;

    theorem :: VECTSP_2:32

    

     Th32: (v * ( 0. R)) = ( 0. V) & (v * ( - ( 1_ R))) = ( - v) & (( 0. V) * x) = ( 0. V)

    proof

      (v + (v * ( 0. R))) = ((v * ( 1_ R)) + (v * ( 0. R))) by Def8

      .= (v * (( 1_ R) + ( 0. R))) by Def8

      .= (v * ( 1_ R)) by RLVECT_1: 4

      .= v by Def8

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

      hence

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

      ((v * ( - ( 1_ R))) + v) = ((v * ( - ( 1_ R))) + (v * ( 1_ R))) by Def8

      .= (v * (( - ( 1_ R)) + ( 1_ R))) by Def8

      .= ( 0. V) by A1, RLVECT_1: 5;

      then ((v * ( - ( 1_ R))) + (v + ( - v))) = (( 0. V) + ( - v)) by RLVECT_1:def 3;

      

      then (( 0. V) + ( - v)) = ((v * ( - ( 1_ R))) + ( 0. V)) by RLVECT_1: 5

      .= (v * ( - ( 1_ R))) by RLVECT_1: 4;

      hence (v * ( - ( 1_ R))) = ( - v) by RLVECT_1: 4;

      (( 0. V) * x) = (v * (( 0. R) * x)) by A1, Def8

      .= ( 0. V) by A1;

      hence thesis;

    end;

    theorem :: VECTSP_2:33

    

     Th33: ( - (v * x)) = (v * ( - x)) & (w - (v * x)) = (w + (v * ( - x)))

    proof

      

       A1: ( - (v * x)) = ((v * x) * ( - ( 1_ R))) by Th32

      .= (v * (x * ( - ( 1_ R)))) by Def8

      .= (v * ( - (x * ( 1_ R)))) by VECTSP_1: 8;

      hence ( - (v * x)) = (v * ( - x));

      thus thesis by A1;

    end;

    theorem :: VECTSP_2:34

    

     Th34: (( - v) * x) = ( - (v * x))

    proof

      (( - v) * x) = ((v * ( - ( 1_ R))) * x) by Th32

      .= (v * (( - ( 1_ R)) * x)) by Def8

      .= (v * ( - (( 1_ R) * x))) by VECTSP_1: 9

      .= (v * ( - x));

      hence thesis by Th33;

    end;

    theorem :: VECTSP_2:35

    ((v - w) * x) = ((v * x) - (w * x))

    proof

      ((v - w) * x) = ((v + ( - w)) * x)

      .= ((v * x) + (( - w) * x)) by Def8

      .= ((v * x) + ( - (w * x))) by Th34;

      hence thesis;

    end;

    reserve F for non degenerated almost_left_invertible Ring;

    reserve x for Scalar of F;

    reserve V for add-associative right_zeroed right_complementable RightMod-like non empty RightModStr over F;

    reserve v for Vector of V;

    theorem :: VECTSP_2:36

    (v * x) = ( 0. V) iff x = ( 0. F) or v = ( 0. V)

    proof

      (v * x) = ( 0. V) implies x = ( 0. F) or v = ( 0. V)

      proof

        assume (v * x) = ( 0. V);

        

        then

         A1: (v * (x * (x " ))) = (( 0. V) * (x " )) by Def8

        .= ( 0. V) by Th32;

        assume x <> ( 0. F);

        then ( 0. V) = (v * ( 1_ F)) by A1, Th9;

        hence thesis by Def8;

      end;

      hence thesis by Th32;

    end;

    theorem :: VECTSP_2:37

    x <> ( 0. F) implies ((v * x) * (x " )) = v

    proof

      assume

       A1: x <> ( 0. F);

      ((v * x) * (x " )) = (v * (x * (x " ))) by Def8

      .= (v * ( 1_ F)) by A1, Th9

      .= v by Def8;

      hence thesis;

    end;

    registration

      cluster almost_left_invertible -> domRing-like for associative well-unital add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      coherence

      proof

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

        assume

         A1: L is almost_left_invertible;

        for x,y be Element of L holds (x * y) = ( 0. L) implies x = ( 0. L) or y = ( 0. L)

        proof

          let x,y be Element of L;

          assume

           A2: (x * y) = ( 0. L);

          now

            assume that

             A3: x <> ( 0. L) and

             A4: y <> ( 0. L);

            consider xx be Element of L such that

             A5: (xx * x) = ( 1. L) by A1, A3;

            y = (( 1. L) * y)

            .= (xx * (x * y)) by A5, GROUP_1:def 3

            .= ( 0. L) by A2;

            hence contradiction by A4;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end