vectsp_1.miz



    begin

    definition

      :: VECTSP_1:def1

      func G_Real -> strict addLoopStr equals addLoopStr (# REAL , addreal , ( In ( 0 , REAL )) #);

      coherence ;

    end

    registration

      cluster G_Real -> non empty;

      coherence ;

    end

    registration

      cluster the carrier of G_Real -> real-membered;

      coherence ;

    end

    registration

      let a,b be Element of G_Real , x,y be Real;

      identify x + y with a + b when a = x, b = y;

      compatibility by BINOP_2:def 9;

    end

    registration

      cluster G_Real -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        thus for x,y be Element of G_Real holds (x + y) = (y + x);

        thus for x,y,z be Element of G_Real holds ((x + y) + z) = (x + (y + z));

        thus for x be Element of G_Real holds (x + ( 0. G_Real )) = x;

        let x be Element of G_Real ;

        reconsider x9 = x as Element of REAL ;

        reconsider y = ( - x9) as Element of G_Real by XREAL_0:def 1;

        take y;

        thus thesis;

      end;

    end

    registration

      let a be Element of G_Real , x be Real;

      identify - x with - a when a = x;

      compatibility

      proof

        reconsider b = ( - x) as Element of G_Real by XREAL_0:def 1;

        assume x = a;

        then (b + a) = ( 0. G_Real );

        hence thesis by RLVECT_1: 6;

      end;

    end

    registration

      let a,b be Element of G_Real , x,y be Real;

      identify x - y with a - b when a = x, b = y;

      compatibility ;

    end

    registration

      cluster strict add-associative right_zeroed right_complementable Abelian for non empty addLoopStr;

      existence

      proof

        take G_Real ;

        thus thesis;

      end;

    end

    definition

      mode AddGroup is add-associative right_zeroed right_complementable non empty addLoopStr;

    end

    definition

      mode AbGroup is Abelian AddGroup;

    end

    definition

      let IT be non empty doubleLoopStr;

      :: VECTSP_1:def2

      attr IT is right-distributive means

      : Def2: for a,b,c be Element of IT holds (a * (b + c)) = ((a * b) + (a * c));

      :: VECTSP_1:def3

      attr IT is left-distributive means

      : Def3: for a,b,c be Element of IT holds ((b + c) * a) = ((b * a) + (c * a));

    end

    definition

      let IT be non empty multLoopStr;

      :: VECTSP_1:def4

      attr IT is right_unital means

      : Def4: for x be Element of IT holds (x * ( 1. IT)) = x;

    end

    definition

      :: VECTSP_1:def5

      func F_Real -> strict doubleLoopStr equals doubleLoopStr (# REAL , addreal , multreal , ( In (1, REAL )), ( In ( 0 , REAL )) #);

      correctness ;

    end

    registration

      cluster F_Real -> non empty;

      coherence ;

    end

    registration

      cluster the carrier of F_Real -> real-membered;

      coherence ;

    end

    registration

      let a,b be Element of F_Real , x,y be Real;

      identify x + y with a + b when a = x, b = y;

      compatibility by BINOP_2:def 9;

    end

    registration

      let a,b be Element of F_Real , x,y be Real;

      identify x * y with a * b when a = x, b = y;

      compatibility by BINOP_2:def 11;

    end

    definition

      let IT be non empty multLoopStr;

      :: VECTSP_1:def6

      attr IT is well-unital means

      : Def6: for x be Element of IT holds (x * ( 1. IT)) = x & (( 1. IT) * x) = x;

    end

    

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

    proof

      let L be non empty multLoopStr;

      assume L is well-unital;

      then (for h be Element of L holds (h * ( 1. L)) = h & (( 1. L) * h) = h) & L is unital;

      hence thesis by GROUP_1:def 4;

    end;

    registration

      cluster F_Real -> well-unital;

      coherence ;

    end

    registration

      cluster well-unital for non empty multLoopStr_0;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    registration

      let L be well-unital non empty multLoopStr_0;

      let x be Element of L;

      reduce (x * ( 1. L)) to x;

      reducibility by Def6;

      reduce (( 1. L) * x) to x;

      reducibility by Def6;

    end

    definition

      let IT be non empty doubleLoopStr;

      :: VECTSP_1:def7

      attr IT is distributive means

      : Def7: for x,y,z be Element of IT holds (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x));

    end

    definition

      let IT be non empty multLoopStr;

      :: VECTSP_1:def8

      attr IT is left_unital means

      : Def8: for x be Element of IT holds (( 1. IT) * x) = x;

    end

    definition

      let IT be non empty multLoopStr_0;

      :: original: almost_left_invertible

      redefine

      :: VECTSP_1:def9

      attr IT is almost_left_invertible means

      : Def9: for x be Element of IT st x <> ( 0. IT) holds ex y be Element of IT st (y * x) = ( 1. IT);

      compatibility

      proof

        thus IT is almost_left_invertible implies for x be Element of IT st x <> ( 0. IT) holds ex y be Element of IT st (y * x) = ( 1. IT) by ALGSTR_0:def 27;

        assume

         A1: for x be Element of IT st x <> ( 0. IT) holds ex y be Element of IT st (y * x) = ( 1. IT);

        let x be Element of IT;

        assume x <> ( 0. IT);

        hence ex y be Element of IT st (y * x) = ( 1. IT) by A1;

      end;

    end

    set FR = F_Real ;

    reconsider jj = 1 as Real;

    registration

      cluster F_Real -> unital;

      coherence

      proof

        reconsider e = jj as Element of FR;

        take e;

        thus thesis;

      end;

    end

    registration

      cluster F_Real -> add-associative right_zeroed right_complementable Abelian commutative associative left_unital right_unital distributive almost_left_invertible non degenerated;

      coherence

      proof

        thus for x,y,z be Element of F_Real holds ((x + y) + z) = (x + (y + z));

        thus for x be Element of F_Real holds (x + ( 0. F_Real )) = x;

        thus F_Real is right_complementable

        proof

          let x be Element of F_Real ;

          reconsider x9 = x as Element of REAL ;

          reconsider y = ( - x9) as Element of F_Real by XREAL_0:def 1;

          take y;

          thus thesis;

        end;

        thus for x,y be Element of F_Real holds (x + y) = (y + x);

        thus for x,y be Element of F_Real holds (x * y) = (y * x);

        thus for x,y,z be Element of F_Real holds ((x * y) * z) = (x * (y * z));

        thus for x be Element of F_Real holds (( 1. F_Real ) * x) = x;

        thus for x be Element of F_Real holds (x * ( 1. F_Real )) = x;

        thus for x,y,z be Element of F_Real holds (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x));

        hereby

          let x be Element of F_Real ;

          reconsider x9 = x as Element of REAL ;

          assume

           A1: x <> ( 0. F_Real );

          reconsider y = (x9 " ) as Element of F_Real by XREAL_0:def 1;

          take y;

          thus (y * x) = ( 1. F_Real ) by A1, XCMPLX_0:def 7;

        end;

        thus ( 0. F_Real ) <> ( 1. F_Real );

      end;

    end

    registration

      let a be Element of F_Real , x be Real;

      identify - x with - a when a = x;

      compatibility

      proof

        reconsider b = ( - x) as Element of FR by XREAL_0:def 1;

        assume x = a;

        then (b + a) = ( 0. FR);

        hence thesis by RLVECT_1: 6;

      end;

    end

    registration

      let a,b be Element of F_Real , x,y be Real;

      identify x - y with a - b when a = x, b = y;

      compatibility ;

    end

    registration

      cluster distributive -> left-distributive right-distributive for non empty doubleLoopStr;

      coherence ;

      cluster left-distributive right-distributive -> distributive for non empty doubleLoopStr;

      coherence ;

    end

    registration

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

      coherence ;

      cluster left_unital right_unital -> unital for non empty multLoopStr;

      coherence ;

    end

    registration

      cluster commutative associative for non empty multMagma;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    registration

      cluster commutative associative unital for non empty multLoopStr;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    registration

      cluster add-associative right_zeroed right_complementable Abelian commutative associative left_unital right_unital distributive almost_left_invertible non degenerated well-unital strict for non empty doubleLoopStr;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    definition

      mode Ring is Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

    end

    definition

      mode Skew-Field is non degenerated almost_left_invertible Ring;

    end

    definition

      mode Field is commutative Skew-Field;

    end

    registration

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

      coherence ;

    end

    ::$Canceled

    theorem :: VECTSP_1:5

    for F be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x,y,z be Element of F holds (x <> ( 0. F) & (x * y) = (x * z)) implies y = z

    proof

      let F be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x,y,z be Element of F;

      assume x <> ( 0. F);

      then

      consider x1 be Element of F such that

       A1: (x1 * x) = ( 1. F) by Def9;

      

       A2: ((x1 * x) * y) = (x1 * (x * y)) & (x1 * (x * z)) = ((x1 * x) * z) by GROUP_1:def 3;

      assume (x * y) = (x * z);

      then ((x * x1) * y) = z by A1, A2, Def8;

      hence thesis by A1;

    end;

    notation

      let F be associative commutative well-unital almost_left_invertible non empty doubleLoopStr, x be Element of F;

      synonym x " for / x;

    end

    definition

      let F be associative commutative well-unital almost_left_invertible non empty doubleLoopStr, x be Element of F;

      assume

       A1: x <> ( 0. F);

      :: original: "

      redefine

      :: VECTSP_1:def10

      func x " means

      : Def10: (it * x) = ( 1. F);

      compatibility

      proof

        let IT be Element of F;

        

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

        then

        consider x1 be Element of F such that

         A3: (x1 * x) = ( 1. F);

        x is right_mult-cancelable

        proof

          let y,z be Element of F;

          assume

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

          

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

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

          .= (z * ( 1. F)) by A3, GROUP_1:def 3

          .= z;

        end;

        hence thesis by A2, ALGSTR_0:def 30;

      end;

    end

    registration

      let a be non zero Element of F_Real , x be Real;

      identify x " with a " when a = x;

      compatibility

      proof

        reconsider b = (x " ) as Element of FR by XREAL_0:def 1;

        

         A1: a <> ( 0. F_Real );

        assume x = a;

        then (b * a) = ( 1. FR) by A1, XCMPLX_0:def 7;

        hence thesis by A1, Def10;

      end;

    end

    registration

      let a,b be non zero Element of F_Real , x,y be Real;

      identify x / y with a / b when a = x, b = y;

      compatibility ;

    end

    ::$Canceled

    theorem :: VECTSP_1:6

    

     Th2: for F be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, x be Element of F holds (x * ( 0. F)) = ( 0. F)

    proof

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

      let x be Element of F;

      ((x * ( 0. F)) + ( 0. F)) = ((x * (( 0. F) + ( 0. F))) + ( 0. F)) by RLVECT_1: 4

      .= (x * (( 0. F) + ( 0. F))) by RLVECT_1: 4

      .= ((x * ( 0. F)) + (x * ( 0. F))) by Def2;

      hence thesis by RLVECT_1: 8;

    end;

    registration

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

      let x be Element of F;

      let y be zero Element of F;

      reduce (x * y) to y;

      reducibility

      proof

        y = ( 0. F) by STRUCT_0:def 12;

        hence thesis by Th2;

      end;

    end

    theorem :: VECTSP_1:7

    

     Th3: for F be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, x be Element of F holds (( 0. F) * x) = ( 0. F)

    proof

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

      let x be Element of F;

      ((( 0. F) * x) + ( 0. F)) = (((( 0. F) + ( 0. F)) * x) + ( 0. F)) by RLVECT_1: 4

      .= ((( 0. F) + ( 0. F)) * x) by RLVECT_1: 4

      .= ((( 0. F) * x) + (( 0. F) * x)) by Def3;

      hence thesis by RLVECT_1: 8;

    end;

    registration

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

      let x be zero Element of F;

      let y be Element of F;

      reduce (x * y) to x;

      reducibility

      proof

        x = ( 0. F) by STRUCT_0:def 12;

        hence thesis by Th3;

      end;

    end

    theorem :: VECTSP_1:8

    

     Th4: for F be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, x,y be Element of F holds (x * ( - y)) = ( - (x * y))

    proof

      let F be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, x,y be Element of F;

      ((x * y) + (x * ( - y))) = (x * (y + ( - y))) by Def2

      .= (x * ( 0. F)) by RLVECT_1:def 10

      .= ( 0. F);

      hence thesis by RLVECT_1:def 10;

    end;

    theorem :: VECTSP_1:9

    

     Th5: for F be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, x,y be Element of F holds (( - x) * y) = ( - (x * y))

    proof

      let F be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, x,y be Element of F;

      ((x * y) + (( - x) * y)) = ((x + ( - x)) * y) by Def3

      .= (( 0. F) * y) by RLVECT_1:def 10

      .= ( 0. F);

      hence thesis by RLVECT_1:def 10;

    end;

    theorem :: VECTSP_1:10

    

     Th6: for F be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, x,y be Element of F holds (( - x) * ( - y)) = (x * y)

    proof

      let F be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, x,y be Element of F;

      

      thus (( - x) * ( - y)) = ( - (x * ( - y))) by Th5

      .= ( - ( - (x * y))) by Th4

      .= (x * y) by RLVECT_1: 17;

    end;

    theorem :: VECTSP_1:11

    for F be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, x,y,z be Element of F holds (x * (y - z)) = ((x * y) - (x * z))

    proof

      let F be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, x,y,z be Element of F;

      (x * (y - z)) = ((x * y) + (x * ( - z))) by Def2

      .= ((x * y) - (x * z)) by Th4;

      hence thesis;

    end;

    theorem :: VECTSP_1:12

    

     Th8: for F be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr, x,y be Element of F holds (x * y) = ( 0. F) iff x = ( 0. F) or y = ( 0. F)

    proof

      let F be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr, x,y be Element of F;

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

      proof

        assume

         A1: (x * y) = ( 0. F);

        assume

         A2: x <> ( 0. F);

        ((x " ) * ( 0. F)) = (((x " ) * x) * y) by A1, GROUP_1:def 3

        .= (( 1. F) * y) by A2, Def10

        .= y;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: VECTSP_1:13

    for K be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr holds for a,b,c be Element of K holds ((a - b) * c) = ((a * c) - (b * c))

    proof

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

      let y,z,x be Element of K;

      

      thus ((y - z) * x) = ((y * x) + (( - z) * x)) by Def3

      .= ((y * x) - (z * x)) by Th5;

    end;

    definition

      let F be 1-sorted;

      struct ( addLoopStr) ModuleStr over F (# the carrier -> set,

the addF -> BinOp of the carrier,

the ZeroF -> Element of the carrier,

the lmult -> Function of [:the carrier of F, the carrier:], the carrier #)

       attr strict strict;

    end

    registration

      let F be 1-sorted;

      cluster non empty strict for ModuleStr over F;

      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 F, A:], A;

        take ModuleStr (# A, a, Z, l #);

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

        thus thesis;

      end;

    end

    registration

      let F 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 F, A:], A;

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

      coherence ;

    end

    definition

      let F be 1-sorted;

      mode Scalar of F is Element of F;

    end

    definition

      let F be 1-sorted;

      let VS be ModuleStr over F;

      mode Scalar of VS is Scalar of F;

      mode Vector of VS is Element of VS;

    end

    definition

      let F be non empty 1-sorted, V be non empty ModuleStr over F;

      let x be Element of F;

      let v be Element of V;

      :: VECTSP_1:def11

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

      coherence ;

    end

    definition

      let F be non empty addLoopStr;

      :: VECTSP_1:def12

      func comp F -> UnOp of the carrier of F means for x be Element of F holds (it . x) = ( - x);

      existence

      proof

        deffunc F( Element of F) = ( - $1);

        thus ex f be UnOp of the carrier of F st for x be Element of F holds (f . x) = F(x) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        let f,g be UnOp of the carrier of F such that

         A1: for x be Element of F holds (f . x) = ( - x) and

         A2: for x be Element of F holds (g . x) = ( - x);

        now

          let x be object;

          assume x in the carrier of F;

          then

          reconsider y = x as Element of F;

          

          thus (f . x) = ( - y) by A1

          .= (g . x) by A2;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

     Lm2:

    now

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

      let MLT be Function of [:the carrier of F, the carrier of F:], the carrier of F;

      set GF = ModuleStr (# the carrier of F, the addF of F, ( 0. F), MLT #);

      thus GF is Abelian

      proof

        let x,y be Element of GF;

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

        

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

        .= (y + x);

      end;

      thus GF is add-associative

      proof

        let x,y,z be Element of GF;

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

        

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

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

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

      end;

      thus GF is right_zeroed

      proof

        let x be Element of GF;

        reconsider x9 = x as Element of F;

        

        thus (x + ( 0. GF)) = (x9 + ( 0. F))

        .= x by RLVECT_1: 4;

      end;

      thus GF is right_complementable

      proof

        let x be Element of GF;

        reconsider x9 = x as Element of F;

        consider t be Element of F such that

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

        reconsider t9 = t as Element of GF;

        take t9;

        thus thesis by A1;

      end;

    end;

     Lm3:

    now

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

      let MLT be Function of [:the carrier of F, the carrier of F:], the carrier of F such that

       A1: MLT = the multF of F;

      let x,y be Element of F;

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

      let v,w be Element of LS;

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

      

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

      .= ((x * v9) + (x * w9)) by Def7

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

      

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

      .= ((x * v9) + (y * v9)) by Def7

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

      

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

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

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

      

      thus (( 1. F) * v) = (( 1. F) * v9) by A1

      .= v;

    end;

    definition

      let F be non empty doubleLoopStr;

      let IT be non empty ModuleStr over F;

      :: VECTSP_1:def13

      attr IT is vector-distributive means

      : Def13: for x be Element of F holds for v,w be Element of IT holds (x * (v + w)) = ((x * v) + (x * w));

      :: VECTSP_1:def14

      attr IT is scalar-distributive means

      : Def14: for x,y be Element of F holds for v be Element of IT holds ((x + y) * v) = ((x * v) + (y * v));

      :: VECTSP_1:def15

      attr IT is scalar-associative means

      : Def15: for x,y be Element of F holds for v be Element of IT holds ((x * y) * v) = (x * (y * v));

      :: VECTSP_1:def16

      attr IT is scalar-unital means

      : Def16: for v be Element of IT holds (( 1. F) * v) = v;

    end

    registration

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

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

      existence

      proof

        take V = ModuleStr (# the carrier of F, the addF of F, ( 0. F), the multF of F #);

        thus for x,y be Element of F holds for v be Element of V holds ((x + y) * v) = ((x * v) + (y * v)) by Lm3;

        thus for x be Element of F holds for v,w be Element of V holds (x * (v + w)) = ((x * v) + (x * w)) by Lm3;

        thus for x,y be Element of F holds for v be Element of V holds ((x * y) * v) = (x * (y * v)) by Lm3;

        thus for v be Element of V holds (( 1. F) * v) = v by Lm3;

        thus thesis by Lm2;

      end;

    end

    definition

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

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

    end

    reserve F for Field,

x for Element of F,

V for VectSp of F,

v for Element of V;

    theorem :: VECTSP_1:14

    

     Th10: for F be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, x be Element of F holds for V be add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty ModuleStr over F, v be Element of V holds (( 0. F) * v) = ( 0. V) & (( - ( 1. F)) * v) = ( - v) & (x * ( 0. V)) = ( 0. V)

    proof

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

      let x be Element of F;

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

      (v + (( 0. F) * v)) = ((( 1. F) * v) + (( 0. F) * v)) by Def16

      .= ((( 1. F) + ( 0. F)) * v) by Def14

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

      .= v by Def16

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

      hence

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

      ((( - ( 1. F)) * v) + v) = ((( - ( 1. F)) * v) + (( 1. F) * v)) by Def16

      .= ((( 1. F) + ( - ( 1. F))) * v) by Def14

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

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

      

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

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

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

      (x * ( 0. V)) = ((x * ( 0. F)) * v) by A1, Def15

      .= ( 0. V) by A1;

      hence thesis;

    end;

    theorem :: VECTSP_1:15

    (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 Def15

        .= ( 0. V) by Th10;

        assume x <> ( 0. F);

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

        hence thesis by Def16;

      end;

      hence thesis by Th10;

    end;

    theorem :: VECTSP_1:16

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds (v + w) = ( 0. V) iff ( - v) = w

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V;

      (v + w) = ( 0. V) implies ( - v) = w

      proof

        assume

         A1: (v + w) = ( 0. V);

        

        thus w = (( 0. V) + w) by RLVECT_1: 4

        .= ((( - v) + v) + w) by RLVECT_1: 5

        .= (( - v) + ( 0. V)) by A1, RLVECT_1:def 3

        .= ( - v) by RLVECT_1: 4;

      end;

      hence thesis by RLVECT_1: 5;

    end;

    

     Lm4: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds ( - (w + ( - v))) = (v - w)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V;

      ( - (w + ( - v))) = (( - ( - v)) - w) by RLVECT_1: 30;

      hence thesis by RLVECT_1: 17;

    end;

    

     Lm5: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds ( - (( - v) - w)) = (w + v)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V;

      ( - (( - v) - w)) = (w + ( - ( - v))) by RLVECT_1: 33;

      hence thesis by RLVECT_1: 17;

    end;

    theorem :: VECTSP_1:17

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, u,v,w be Element of V holds ( - (v + w)) = (( - w) - v) & ( - (w + ( - v))) = (v - w) & ( - (v - w)) = (w + ( - v)) & ( - (( - v) - w)) = (w + v) & (u - (w + v)) = ((u - v) - w) by Lm4, Lm5, RLVECT_1: 27, RLVECT_1: 30, RLVECT_1: 33;

    theorem :: VECTSP_1:18

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds (( 0. V) - v) = ( - v) & (v - ( 0. V)) = v by RLVECT_1: 13, RLVECT_1: 14;

    theorem :: VECTSP_1:19

    

     Th15: for F be add-associative right_zeroed right_complementable non empty addLoopStr, x,y be Element of F holds ((x + ( - y)) = ( 0. F) iff x = y) & ((x - y) = ( 0. F) iff x = y)

    proof

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

      (x + ( - y)) = ( 0. F) implies x = y

      proof

        assume (x + ( - y)) = ( 0. F);

        then (x + (( - y) + y)) = (( 0. F) + y) by RLVECT_1:def 3;

        then (x + ( 0. F)) = (( 0. F) + y) by RLVECT_1: 5;

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

        hence thesis by RLVECT_1: 4;

      end;

      hence thesis by RLVECT_1: 5;

    end;

    theorem :: VECTSP_1:20

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

    proof

      assume

       A1: x <> ( 0. F);

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

      .= (( 1. F) * v) by A1, Def10

      .= v by Def16;

      hence thesis;

    end;

    theorem :: VECTSP_1:21

    

     Th17: for F be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable non empty ModuleStr over F, x be Element of F, v,w be Element of V holds ( - (x * v)) = (( - x) * v) & (w - (x * v)) = (w + (( - x) * v))

    proof

      let F be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable non empty ModuleStr over F, x be Element of F, v,w be Element of V;

      

       A1: ( - (x * v)) = (( - ( 1. F)) * (x * v)) by Th10

      .= ((( - ( 1. F)) * x) * v) by Def15

      .= (( - (( 1. F) * x)) * v) by Th5;

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

      thus thesis by A1;

    end;

    registration

      cluster commutative left_unital -> right_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;

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

        hence thesis by A1;

      end;

    end

    theorem :: VECTSP_1:22

    

     Th18: for F be add-associative right_zeroed right_complementable Abelian associative well-unital right_unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable non empty ModuleStr over F, x be Element of F, v be Element of V holds (x * ( - v)) = ( - (x * v))

    proof

      let F be add-associative right_zeroed right_complementable Abelian associative well-unital right_unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable non empty ModuleStr over F, x be Element of F, v be Element of V;

      (x * ( - v)) = (x * (( - ( 1. F)) * v)) by Th10

      .= ((x * ( - ( 1. F))) * v) by Def15

      .= (( - (x * ( 1. F))) * v) by Th4

      .= (( - x) * v);

      hence thesis by Th17;

    end;

    theorem :: VECTSP_1:23

    for F be add-associative right_zeroed right_complementable Abelian associative well-unital right_unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable non empty ModuleStr over F, x be Element of F, v,w be Element of V holds (x * (v - w)) = ((x * v) - (x * w))

    proof

      let F be add-associative right_zeroed right_complementable Abelian associative well-unital right_unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable non empty ModuleStr over F, x be Element of F, v,w be Element of V;

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

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

      hence thesis;

    end;

    theorem :: VECTSP_1:24

    

     Th20: for F be add-associative right_zeroed right_complementable commutative associative well-unital non degenerated almost_left_invertible distributive non empty doubleLoopStr, x be Element of F holds x <> ( 0. F) implies ((x " ) " ) = x

    proof

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

      assume

       A1: x <> ( 0. F);

      x <> ( 0. F) implies (x " ) <> ( 0. F)

      proof

        assume

         A2: x <> ( 0. F);

        assume not thesis;

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

        hence contradiction;

      end;

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

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

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

      then ((x " ) " ) = (x * ( 1. F));

      hence thesis;

    end;

    registration

      let F be add-associative right_zeroed right_complementable commutative associative well-unital almost_left_invertible distributive non degenerated doubleLoopStr;

      let x be non zero Element of F;

      reduce ((x " ) " ) to x;

      reducibility

      proof

        x <> ( 0. F);

        hence thesis by Th20;

      end;

    end

    theorem :: VECTSP_1:25

    for F be Field, x be Element of F holds x <> ( 0. F) implies (x " ) <> ( 0. F) & ( - (x " )) <> ( 0. F)

    proof

      let F be Field, x be Element of F;

      assume

       A1: x <> ( 0. F);

      hereby

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

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

        hence contradiction;

      end;

      assume ( - (x " )) = ( 0. F);

      then (( 1. F) * (x " )) = (( - ( 1. F)) * ( 0. F)) by Th6;

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

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

      hence contradiction;

    end;

    theorem :: VECTSP_1:26

    

     Th22: (( 1. F_Real ) + ( 1. F_Real )) <> ( 0. F_Real );

    definition

      let IT be non empty addLoopStr;

      :: VECTSP_1:def17

      attr IT is Fanoian means for a be Element of IT st (a + a) = ( 0. IT) holds a = ( 0. IT);

    end

    registration

      cluster Fanoian for non empty addLoopStr;

      existence

      proof

        take F = F_Real ;

        let a be Element of F such that

         A1: (a + a) = ( 0. F);

        a = (( 1. F) * a);

        then (a + a) = ((( 1. F) + ( 1. F)) * a) by Def7;

        hence thesis by A1, Th8, Th22;

      end;

    end

    definition

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

      :: original: Fanoian

      redefine

      :: VECTSP_1:def18

      attr F is Fanoian means (( 1. F) + ( 1. F)) <> ( 0. F);

      compatibility

      proof

        thus F is Fanoian implies (( 1. F) + ( 1. F)) <> ( 0. F);

        assume

         A1: (( 1. F) + ( 1. F)) <> ( 0. F);

        let a be Element of F such that

         A2: (a + a) = ( 0. F);

        a = (( 1. F) * a);

        then (a + a) = ((( 1. F) + ( 1. F)) * a) by Def7;

        hence thesis by A1, A2, Th8;

      end;

    end

    registration

      cluster strict Fanoian for Field;

      existence

      proof

         F_Real is Fanoian;

        hence thesis;

      end;

    end

    theorem :: VECTSP_1:27

    for F be add-associative right_zeroed right_complementable non empty addLoopStr, a,b be Element of F holds (a - b) = ( 0. F) implies a = b by Th15;

    theorem :: VECTSP_1:28

    

     Th24: for F be add-associative right_zeroed right_complementable non empty addLoopStr, a be Element of F holds ( - a) = ( 0. F) implies a = ( 0. F)

    proof

      let F be add-associative right_zeroed right_complementable non empty addLoopStr, a be Element of F;

      ( - ( - a)) = a by RLVECT_1: 17;

      hence thesis by RLVECT_1: 12;

    end;

    theorem :: VECTSP_1:29

    for F be add-associative right_zeroed right_complementable non empty addLoopStr, a,b be Element of F holds (a - b) = ( 0. F) implies (b - a) = ( 0. F)

    proof

      let F be add-associative right_zeroed right_complementable non empty addLoopStr, a,b be Element of F;

      (a - b) = ( - (b - a)) by RLVECT_1: 33;

      hence thesis by Th24;

    end;

    theorem :: VECTSP_1:30

    for a,b,c be Element of F holds (a <> ( 0. F) & ((a * c) - b) = ( 0. F) implies c = (b * (a " ))) & (a <> ( 0. F) & (b - (c * a)) = ( 0. F) implies c = (b * (a " )))

    proof

      let a,b,c be Element of F;

      thus

       A1: a <> ( 0. F) & ((a * c) - b) = ( 0. F) implies c = (b * (a " ))

      proof

        assume a <> ( 0. F);

        then

         A2: ((a " ) * a) = ( 1. F) by Def10;

        assume ((a * c) - b) = ( 0. F);

        then ((a " ) * (a * c)) = (b * (a " )) by RLVECT_1: 21;

        then (((a " ) * a) * c) = (b * (a " )) by GROUP_1:def 3;

        hence thesis by A2;

      end;

      assume

       A3: a <> ( 0. F);

      assume (b - (c * a)) = ( 0. F);

      then ( - (b - (c * a))) = ( 0. F) by RLVECT_1: 12;

      hence thesis by A1, A3, RLVECT_1: 33;

    end;

    theorem :: VECTSP_1:31

    for F be add-associative right_zeroed right_complementable non empty addLoopStr, a,b be Element of F holds (a + b) = ( - (( - b) + ( - a)))

    proof

      let F be add-associative right_zeroed right_complementable non empty addLoopStr, a,b be Element of F;

      

      thus (a + b) = ( - ( - (a + b))) by RLVECT_1: 17

      .= ( - (( - b) + ( - a))) by RLVECT_1: 31;

    end;

    theorem :: VECTSP_1:32

    for F be add-associative right_zeroed right_complementable non empty addLoopStr, a,b,c be Element of F holds ((b + a) - (c + a)) = (b - c)

    proof

      let F be add-associative right_zeroed right_complementable non empty addLoopStr, a,b,c be Element of F;

      

      thus ((b + a) - (c + a)) = ((b + a) + (( - a) + ( - c))) by RLVECT_1: 31

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

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

      .= ((b + ( 0. F)) + ( - c)) by RLVECT_1: 5

      .= (b - c) by RLVECT_1: 4;

    end;

    theorem :: VECTSP_1:33

    for G be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of G holds ( - (( - v) + w)) = (( - w) + v)

    proof

      let G be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of G;

      

      thus ( - (( - v) + w)) = (( - w) + ( - ( - v))) by RLVECT_1: 31

      .= (( - w) + v) by RLVECT_1: 17;

    end;

    theorem :: VECTSP_1:34

    for G be Abelian add-associative non empty addLoopStr, u,v,w be Element of G holds ((u - v) - w) = ((u - w) - v)

    proof

      let G be Abelian add-associative non empty addLoopStr, u,v,w be Element of G;

      

      thus ((u - v) - w) = ((u + ( - v)) + ( - w))

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

      .= ((u - w) - v);

    end;

    theorem :: VECTSP_1:35

    for B be AbGroup holds multMagma (# the carrier of B, the addF of B #) is commutative Group

    proof

      let B be AbGroup;

      set G = multMagma (# the carrier of B, the addF of B #);

      

       A1: for a,b be Element of G, x,y be Element of B st a = x & b = y holds (a * b) = (x + y);

      

       A2: G is associative Group-like

      proof

        reconsider e = ( 0. B) as Element of G;

        thus for a,b,c be Element of G holds ((a * b) * c) = (a * (b * c))

        proof

          let a,b,c be Element of G;

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

          

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

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

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

        end;

        take e;

        let a be Element of G;

        reconsider x = a as Element of B;

        

        thus (a * e) = (x + ( 0. B))

        .= a by RLVECT_1: 4;

        reconsider b = ( - x) as Element of G;

        

        thus (e * a) = (x + ( 0. B)) by A1

        .= a by RLVECT_1: 4;

        take b;

        

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

        .= e by RLVECT_1: 5;

        

        thus (b * a) = (x + ( - x)) by A1

        .= e by RLVECT_1: 5;

      end;

      now

        let a,b be Element of G;

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

        

        thus (a * b) = (y + x) by A1

        .= (b * a);

      end;

      hence thesis by A2, GROUP_1:def 12;

    end;

    begin

    theorem :: VECTSP_1:36

    for L be add-associative right_zeroed right_complementable right-distributive unital non empty doubleLoopStr holds for n be Element of NAT st n > 0 holds (( power L) . (( 0. L),n)) = ( 0. L)

    proof

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

      let n be Element of NAT ;

      assume n > 0 ;

      then

       A1: n >= ( 0 + 1) by NAT_1: 13;

      n = ((n - 1) + 1)

      .= ((n -' 1) + 1) by A1, XREAL_0:def 2, XREAL_1: 19;

      

      hence (( power L) . (( 0. L),n)) = ((( power L) . (( 0. L),(n -' 1))) * ( 0. L)) by GROUP_1:def 7

      .= ( 0. L);

    end;

    registration

      cluster well-unital for non empty multLoopStr;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    registration

      let S be well-unital non empty multLoopStr;

      identify 1. S with 1_ S;

      compatibility by Lm1;

    end

    theorem :: VECTSP_1:37

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

    definition

      let G,H be non empty addMagma;

      let f be Function of G, H;

      :: VECTSP_1:def19

      attr f is additive means for x,y be Element of G holds (f . (x + y)) = ((f . x) + (f . y));

    end

    registration

      let L be right_unital non empty multLoopStr;

      let x be Element of L;

      reduce (x * ( 1. L)) to x;

      reducibility by Def4;

    end

    registration

      let L be left_unital non empty multLoopStr;

      let x be Element of L;

      reduce (( 1. L) * x) to x;

      reducibility by Def8;

    end