lmod_7.miz

    begin

    scheme :: LMOD_7:sch1

    ElementEq { A() -> set , P[ object] } :

for X1,X2 be Element of A() st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2;

      let X1,X2 be Element of A() such that

       A1: for x be object holds x in X1 iff P[x] and

       A2: for x be object holds x in X2 iff P[x];

      for x be object holds x in X1 iff x in X2 by A1, A2;

      hence thesis by TARSKI: 2;

    end;

    scheme :: LMOD_7:sch2

    UnOpEq { A() -> non empty set , F( Element of A()) -> object } :

for f1,f2 be UnOp of A() st (for a be Element of A() holds (f1 . a) = F(a)) & (for a be Element of A() holds (f2 . a) = F(a)) holds f1 = f2;

      let f1,f2 be UnOp of A() such that

       A1: for a be Element of A() holds (f1 . a) = F(a) and

       A2: for a be Element of A() holds (f2 . a) = F(a);

      now

        let a be Element of A();



        thus (f1 . a) = F(a) by A1

        .= (f2 . a) by A2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: LMOD_7:sch3

    TriOpEq { A() -> non empty set , F( Element of A(), Element of A(), Element of A()) -> object } :

for f1,f2 be TriOp of A() st (for a,b,c be Element of A() holds (f1 . (a,b,c)) = F(a,b,c)) & (for a,b,c be Element of A() holds (f2 . (a,b,c)) = F(a,b,c)) holds f1 = f2;

      let f1,f2 be TriOp of A() such that

       A1: for a,b,c be Element of A() holds (f1 . (a,b,c)) = F(a,b,c) and

       A2: for a,b,c be Element of A() holds (f2 . (a,b,c)) = F(a,b,c);

      now

        let a,b,c be Element of A();



        thus (f1 . (a,b,c)) = F(a,b,c) by A1

        .= (f2 . (a,b,c)) by A2;

      end;

      hence thesis by MULTOP_1: 3;

    end;

    scheme :: LMOD_7:sch4

    QuaOpEq { A() -> non empty set , F( Element of A(), Element of A(), Element of A(), Element of A()) -> object } :

for f1,f2 be QuaOp of A() st (for a,b,c,d be Element of A() holds (f1 . (a,b,c,d)) = F(a,b,c,d)) & (for a,b,c,d be Element of A() holds (f2 . (a,b,c,d)) = F(a,b,c,d)) holds f1 = f2;

      let f1,f2 be QuaOp of A() such that

       A1: for a,b,c,d be Element of A() holds (f1 . (a,b,c,d)) = F(a,b,c,d) and

       A2: for a,b,c,d be Element of A() holds (f2 . (a,b,c,d)) = F(a,b,c,d);

      now

        let a,b,c,d be Element of A();



        thus (f1 . (a,b,c,d)) = F(a,b,c,d) by A1

        .= (f2 . (a,b,c,d)) by A2;

      end;

      hence thesis by MULTOP_1: 6;

    end;

    scheme :: LMOD_7:sch5

    Fraenkel1Ex { A,D() -> non empty set , F( object) -> Element of D() , P[ object] } :

ex S be Subset of D() st S = { F(x) where x be Element of A() : P[x] };

      reconsider S = { F(x) where x be Element of A() : P[x] } as Subset of D() from DOMAIN_1:sch 8;

      take S;

      thus thesis;

    end;

    scheme :: LMOD_7:sch6

    Fr0 { A() -> non empty set , x() -> Element of A() , P[ object] } :

P[x()]

      provided

       A1: x() in { a where a be Element of A() : P[a] };

      ex a be Element of A() st x() = a & P[a] by A1;

      hence thesis;

    end;

    scheme :: LMOD_7:sch7

    Fr1 { X() -> set , A() -> non empty set , a() -> Element of A() , P[ object] } :

a() in X() iff P[a()]

      provided

       A1: X() = { a where a be Element of A() : P[a] };

      thus a() in X() implies P[a()]

      proof

        assume a() in X();

        then

         A2: a() in { a where a be Element of A() : P[a] } by A1;

        thus P[a()] from Fr0( A2);

      end;

      assume P[a()];

      hence thesis by A1;

    end;

    scheme :: LMOD_7:sch8

    Fr2 { X() -> set , A() -> non empty set , a() -> Element of A() , P[ object] } :

P[a()]

      provided

       A1: a() in X()

       and

       A2: X() = { a where a be Element of A() : P[a] };



       A3: a() in { a where a be Element of A() : P[a] } by A1, A2;

      thus P[a()] from Fr0( A3);

    end;

    scheme :: LMOD_7:sch9

    Fr3 { x() -> set , X() -> set , A() -> non empty set , P[ object] } :

x() in X() iff ex a be Element of A() st x() = a & P[a]

      provided

       A1: X() = { a where a be Element of A() : P[a] };

      thus thesis by A1;

    end;

    scheme :: LMOD_7:sch10

    Fr4 { D1,D2() -> non empty set , B() -> set , a() -> Element of D1() , F( object) -> set , P,Q[ object, object] } :

a() in F(B) iff for b be Element of D2() st b in B() holds P[a(), b]

      provided

       A1: F(B) = { a where a be Element of D1() : Q[a, B()] }

       and

       A2: Q[a(), B()] iff for b be Element of D2() st b in B() holds P[a(), b];

      thus a() in F(B) implies for b be Element of D2() st b in B() holds P[a(), b]

      proof

        defpred X[ set] means Q[$1, B()];

        assume a() in F(B);

        then

         A3: a() in { a where a be Element of D1() : X[a] } by A1;

         X[a()] from Fr0( A3);

        hence thesis by A2;

      end;

      assume for b be Element of D2() st b in B() holds P[a(), b];

      hence thesis by A1, A2;

    end;

    begin

    reserve x for set,

K for Ring,

r for Scalar of K,

V for LeftMod of K,

a,b,a1,a2 for Vector of V,

A,A1,A2 for Subset of V,

l for Linear_Combination of A,

W for Subspace of V,

Li for FinSequence of ( Submodules V);



     Lm1: for G be AbGroup, a,b,c be Element of G holds ( - (a - b)) = (( - a) - ( - b)) & ((a - b) + c) = ((a + c) - b)

    proof

      let G be AbGroup, a,b,c be Element of G;



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

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

      thus thesis by RLVECT_1:def 3;

    end;

    theorem :: LMOD_7:1



     Th1: K is non trivial & A is linearly-independent implies not ( 0. V) in A

    proof

      assume that

       A1: K is non trivial and

       A2: A is linearly-independent;

      ( 0. K) <> ( 1_ K) by A1, LMOD_6:def 1;

      then K is non degenerated;

      hence thesis by A2, VECTSP_7: 2;

    end;

    theorem :: LMOD_7:2



     Th2: not a in A implies (l . a) = ( 0. K)

    proof

      assume

       A1: not a in A;

      ( Carrier l) c= A by VECTSP_6:def 4;

      then not a in ( Carrier l) by A1;

      hence thesis by VECTSP_6: 2;

    end;

    theorem :: LMOD_7:3

    K is trivial implies (for l holds ( Carrier l) = {} ) & ( Lin A) is trivial

    proof

      assume

       A1: K is trivial;

      thus

       A2: for l holds ( Carrier l) = {}

      proof

        let l;

        assume

         A3: ( Carrier l) <> {} ;

        set x = the Element of ( Carrier l);

        ex a st (x = a) & ((l . a) <> ( 0. K)) by A3, VECTSP_6: 1;

        hence contradiction by A1;

      end;

      now

        let a be Vector of ( Lin A);

        a in ( Lin A);

        then

        consider l such that

         A4: a = ( Sum l) by MOD_3: 4;

        ( Carrier l) = {} by A2;

        then a = ( 0. V) by A4, VECTSP_6: 19;

        hence a = ( 0. ( Lin A)) by VECTSP_4: 11;

      end;

      hence thesis;

    end;

    theorem :: LMOD_7:4



     Th4: V is non trivial implies for A st A is base holds A <> {}

    proof

      assume

       A1: V is non trivial;

      let A such that

       A2: A is base and

       A3: A = {} ;



       A4: A = ( {} the carrier of V) by A3;

       the ModuleStr of V = ( Lin A) by A2, VECTSP_7:def 3

      .= ( (0). V) by A4, MOD_3: 6;

      hence contradiction by A1, LMOD_6: 7;

    end;

    theorem :: LMOD_7:5



     Th5: (A1 \/ A2) is linearly-independent & A1 misses A2 implies (( Lin A1) /\ ( Lin A2)) = ( (0). V)

    proof

      assume that

       A1: (A1 \/ A2) is linearly-independent and

       A2: (A1 /\ A2) = {} ;

      reconsider P = (( Lin A1) /\ ( Lin A2)) as strict Subspace of V;

      set Z = the carrier of P;



       A3: Z = (the carrier of ( Lin A1) /\ the carrier of ( Lin A2)) by VECTSP_5:def 2;

       A4:

      now

        let x;

        assume

         A5: x in Z;

        then

         A6: x in the carrier of ( Lin A1) by A3, XBOOLE_0:def 4;



         A7: x in the carrier of ( Lin A2) by A3, A5, XBOOLE_0:def 4;



         A8: x in ( Lin A1) by A6;



         A9: x in ( Lin A2) by A7;

        consider l1 be Linear_Combination of A1 such that

         A10: x = ( Sum l1) by A8, MOD_3: 4;

        consider l2 be Linear_Combination of A2 such that

         A11: x = ( Sum l2) by A9, MOD_3: 4;



         A12: ( Carrier l1) c= A1 by VECTSP_6:def 4;

        ( Carrier l2) c= A2 by VECTSP_6:def 4;

        then

         A13: (( Carrier l1) \/ ( Carrier l2)) c= (A1 \/ A2) by A12, XBOOLE_1: 13;

        ( Carrier (l1 - l2)) c= (( Carrier l1) \/ ( Carrier l2)) by VECTSP_6: 41;

        then ( Carrier (l1 - l2)) c= (A1 \/ A2) by A13, XBOOLE_1: 1;

        then

        reconsider l = (l1 - l2) as Linear_Combination of (A1 \/ A2) by VECTSP_6:def 4;

        ( Sum l) = (( Sum l1) - ( Sum l2)) by VECTSP_6: 47

        .= ( 0. V) by A10, A11, VECTSP_1: 19;

        then

         A14: ( Carrier l) = {} by A1, VECTSP_7:def 1;

        ( Carrier l1) = {}

        proof

          assume

           A15: ( Carrier l1) <> {} ;

          set x = the Element of ( Carrier l1);

          consider b such that

           A16: x = b and

           A17: (l1 . b) <> ( 0. K) by A15, VECTSP_6: 1;

          b in A1 by A12, A15, A16, TARSKI:def 3;

          then

           A18: not b in A2 by A2, XBOOLE_0:def 4;

          ( 0. K) = (l . b) by A14, VECTSP_6: 2

          .= ((l1 . b) - (l2 . b)) by VECTSP_6: 40;



          then (l1 . b) = (l2 . b) by RLVECT_1: 21

          .= ( 0. K) by A18, Th2;

          hence contradiction by A17;

        end;

        hence x = ( 0. V) by A10, VECTSP_6: 19;

      end;

      ( 0. V) in (( Lin A1) /\ ( Lin A2)) by VECTSP_4: 17;

      then for x be object holds x in Z iff x = ( 0. V) by A4;

      then Z = {( 0. V)} by TARSKI:def 1;

      hence thesis by VECTSP_4:def 3;

    end;

    theorem :: LMOD_7:6



     Th6: A is base & A = (A1 \/ A2) & A1 misses A2 implies V is_the_direct_sum_of (( Lin A1),( Lin A2))

    proof

      assume that

       A1: A is base and

       A2: A = (A1 \/ A2) and

       A3: A1 misses A2;

      set W = the ModuleStr of V;



       A4: A is linearly-independent by A1, VECTSP_7:def 3;

      ( Lin A) = W by A1, VECTSP_7:def 3;

      then

       A5: W = (( Lin A1) + ( Lin A2)) by A2, MOD_3: 12;

      (( Lin A1) /\ ( Lin A2)) = ( (0). V) by A2, A3, A4, Th5;

      hence thesis by A5, VECTSP_5:def 4;

    end;

    begin

    definition

      let K, V;

      :: LMOD_7:def1

      mode SUBMODULE_DOMAIN of V -> non empty set means

      : Def1: x in it implies x is strict Subspace of V;

      existence

      proof

        set a = the strict Subspace of V;

        set D = {a};

        take D;

        thus thesis by TARSKI:def 1;

      end;

    end

    definition

      let K, V;

      :: original: Submodules

      redefine

      func Submodules (V) -> SUBMODULE_DOMAIN of V ;

      coherence

      proof

        now

          let x;

          assume x in ( Submodules V);

          then ex W be strict Subspace of V st (W = x) by VECTSP_5:def 3;

          hence x is strict Subspace of V;

        end;

        hence thesis by Def1;

      end;

    end

    definition

      let K, V;

      let D be SUBMODULE_DOMAIN of V;

      :: original: Element

      redefine

      mode Element of D -> strict Subspace of V ;

      coherence by Def1;

    end

    registration

      let K, V;

      let D be SUBMODULE_DOMAIN of V;

      cluster strict for Element of D;

      existence

      proof

        set x = the Element of D;

        take x;

        thus thesis;

      end;

    end

    definition

      let K, V;

      assume

       A1: V is non trivial;

      :: LMOD_7:def2

      mode LINE of V -> strict Subspace of V means ex a st a <> ( 0. V) & it = <:a:>;

      existence

      proof

        consider a such that

         A2: a <> ( 0. V) by A1;

        take <:a:>;

        thus thesis by A2;

      end;

    end

    definition

      let K, V;

      :: LMOD_7:def3

      mode LINE_DOMAIN of V -> non empty set means

      : Def3: x in it implies x is LINE of V;

      existence

      proof

        set a = the LINE of V;

        set D = {a};

        take D;

        thus thesis by TARSKI:def 1;

      end;

    end

    definition

      let K, V;

      :: LMOD_7:def4

      func lines (V) -> LINE_DOMAIN of V means for x be object holds x in it iff x is LINE of V;

      existence

      proof

        set D = { a where a be Element of ( Submodules V) : a is LINE of V };

        set a1 = the LINE of V;

        reconsider a2 = a1 as Element of ( Submodules V) by VECTSP_5:def 3;

        a2 in D;

        then

        reconsider D as non empty set;

         A1:

        now

          let x;

          assume x in D;

          then ex a be Element of ( Submodules V) st (x = a) & (a is LINE of V);

          hence x is LINE of V;

        end;

        then

        reconsider D9 = D as LINE_DOMAIN of V by Def3;

        take D9;

        now

          let x be object;

          thus x in D9 implies x is LINE of V by A1;

          thus x is LINE of V implies x in D9

          proof

            assume

             A2: x is LINE of V;

            then

            reconsider x1 = x as Element of ( Submodules V) by VECTSP_5:def 3;

            x1 in D by A2;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let D1,D2 be LINE_DOMAIN of V such that

         A3: for x be object holds x in D1 iff x is LINE of V and

         A4: for x be object holds x in D2 iff x is LINE of V;

        now

          let x be object;

          x in D1 iff x is LINE of V by A3;

          hence x in D1 iff x in D2 by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let K, V;

      let D be LINE_DOMAIN of V;

      :: original: Element

      redefine

      mode Element of D -> LINE of V ;

      coherence by Def3;

    end

    definition

      let K, V;

      assume that

       A1: V is non trivial and

       A2: V is free;

      :: LMOD_7:def5

      mode HIPERPLANE of V -> strict Subspace of V means ex a st a <> ( 0. V) & V is_the_direct_sum_of ( <:a:>,it );

      existence

      proof

        consider A be Subset of V such that

         A3: A is base by A2, VECTSP_7:def 4;

        reconsider A as Subset of V;



         A4: A is linearly-independent by A3, VECTSP_7:def 3;



         A5: A <> {} by A1, A3, Th4;

        set x = the Element of A;

        reconsider a = x as Vector of V by A5, TARSKI:def 3;

        reconsider A1 = {a} as Subset of V;

        set A2 = (A \ A1);

        set H = ( Lin A2);

        A1 c= A by A5, ZFMISC_1: 31;

        then

         A6: A = (A1 \/ A2) by XBOOLE_1: 45;

        A1 misses A2 by XBOOLE_1: 79;

        then

         A7: V is_the_direct_sum_of (( Lin A1),H) by A3, A6, Th6;



         A8: ex a st a <> ( 0. V) & V is_the_direct_sum_of ( <:a:>,H)

        proof

          take a;

          thus thesis by A1, A4, A5, A7, Th1, LMOD_6: 6, LMOD_6:def 4;

        end;

        take H;

        thus thesis by A8;

      end;

    end

    definition

      let K, V;

      :: LMOD_7:def6

      mode HIPERPLANE_DOMAIN of V -> non empty set means

      : Def6: x in it implies x is HIPERPLANE of V;

      existence

      proof

        set a = the HIPERPLANE of V;

        set D = {a};

        take D;

        thus thesis by TARSKI:def 1;

      end;

    end

    definition

      let K, V;

      :: LMOD_7:def7

      func hiperplanes (V) -> HIPERPLANE_DOMAIN of V means for x be object holds x in it iff x is HIPERPLANE of V;

      existence

      proof

        set D = { a where a be Element of ( Submodules V) : a is HIPERPLANE of V };

        set a1 = the HIPERPLANE of V;

        reconsider a2 = a1 as Element of ( Submodules V) by VECTSP_5:def 3;

        a2 in D;

        then

        reconsider D as non empty set;

         A1:

        now

          let x;

          assume x in D;

          then ex a be Element of ( Submodules V) st (x = a) & (a is HIPERPLANE of V);

          hence x is HIPERPLANE of V;

        end;

        then

        reconsider D9 = D as HIPERPLANE_DOMAIN of V by Def6;

        take D9;

        now

          let x be object;

          thus x in D9 implies x is HIPERPLANE of V by A1;

          thus x is HIPERPLANE of V implies x in D9

          proof

            assume x is HIPERPLANE of V;

            then

            reconsider W = x as HIPERPLANE of V;

            reconsider x1 = W as Element of ( Submodules V) by VECTSP_5:def 3;

            x1 in D;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let D1,D2 be HIPERPLANE_DOMAIN of V such that

         A2: for x be object holds x in D1 iff x is HIPERPLANE of V and

         A3: for x be object holds x in D2 iff x is HIPERPLANE of V;

        now

          let x be object;

          x in D1 iff x is HIPERPLANE of V by A2;

          hence x in D1 iff x in D2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let K, V;

      let D be HIPERPLANE_DOMAIN of V;

      :: original: Element

      redefine

      mode Element of D -> HIPERPLANE of V ;

      coherence by Def6;

    end

    begin

    definition

      let K, V, Li;

      :: LMOD_7:def8

      func Sum Li -> Element of ( Submodules V) equals (( SubJoin V) $$ Li);

      coherence ;

      :: LMOD_7:def9

      func /\ Li -> Element of ( Submodules V) equals (( SubMeet V) $$ Li);

      coherence ;

    end

    theorem :: LMOD_7:7

    ( SubJoin V) is commutative associative & ( SubJoin V) is having_a_unity & ( (0). V) = ( the_unity_wrt ( SubJoin V))

    proof

      set S0 = ( Submodules V), S1 = ( SubJoin V);

      reconsider L = LattStr (# S0 qua non empty set, S1 qua BinOp of S0, ( SubMeet V) qua BinOp of S0 #) as Lattice by VECTSP_5: 57;

      S1 = the L_join of L;

      hence S1 is commutative associative;

      set e = ( (0). V);

      reconsider e9 = ( @ e) as Element of S0 qua non empty set;



       A1: e9 = e by LMOD_6:def 2;

      now

        let a9 be Element of S0 qua non empty set;

        reconsider b = a9 as Element of S0;

        reconsider a = b as strict Subspace of V;



        thus (S1 . (e9,a9)) = (e + a) by A1, VECTSP_5:def 7

        .= a9 by VECTSP_5: 9;



        thus (S1 . (a9,e9)) = (a + e) by A1, VECTSP_5:def 7

        .= a9 by VECTSP_5: 9;

      end;

      then

       A2: e9 is_a_unity_wrt S1 qua BinOp of S0 by BINOP_1: 3;

      hence S1 is having_a_unity by SETWISEO:def 2;

      thus thesis by A1, A2, BINOP_1:def 8;

    end;

    theorem :: LMOD_7:8

    ( SubMeet V) is commutative associative & ( SubMeet V) is having_a_unity & ( (Omega). V) = ( the_unity_wrt ( SubMeet V))

    proof

      set S0 = ( Submodules V), S2 = ( SubMeet V);

      reconsider L = LattStr (# S0 qua non empty set, ( SubJoin V) qua BinOp of S0, S2 qua BinOp of S0 #) as Lattice by VECTSP_5: 57;

      S2 = the L_meet of L;

      hence S2 is commutative associative;

      set e = ( (Omega). V);

      reconsider e9 = ( @ e) as Element of S0 qua non empty set;



       A1: e9 = e by LMOD_6:def 2;

      now

        let a9 be Element of S0 qua non empty set;

        reconsider b = a9 as Element of S0;

        reconsider a = b as strict Subspace of V;



        thus (S2 qua BinOp of S0 . (e9,a9)) = (e /\ a) by A1, VECTSP_5:def 8

        .= a9 by VECTSP_5: 21;



        thus (S2 qua BinOp of S0 . (a9,e9)) = (a /\ e) by A1, VECTSP_5:def 8

        .= a9 by VECTSP_5: 21;

      end;

      then

       A2: e9 is_a_unity_wrt S2 qua BinOp of S0 by BINOP_1: 3;

      hence S2 is having_a_unity by SETWISEO:def 2;

      thus thesis by A1, A2, BINOP_1:def 8;

    end;

    begin

    definition

      let K, V, A1, A2;

      :: LMOD_7:def10

      func A1 + A2 -> Subset of V means x in it iff ex a1, a2 st a1 in A1 & a2 in A2 & x = (a1 + a2);

      existence

      proof

        set S = { (a1 + a2) : a1 in A1 & a2 in A2 };

         A1:

        now

          let x;

          assume x in S;

          then ex a1, a2 st (x = (a1 + a2)) & (a1 in A1) & (a2 in A2);

          hence ex a1, a2 st a1 in A1 & a2 in A2 & x = (a1 + a2);

        end;

        now

          let x be object;

          assume x in S;

          then ex a1, a2 st (x = (a1 + a2)) & (a1 in A1) & (a2 in A2);

          hence x in the carrier of V;

        end;

        then

        reconsider S9 = S as Subset of V by TARSKI:def 3;

        take S9;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be Subset of V such that

         A2: x in D1 iff ex a1, a2 st a1 in A1 & a2 in A2 & x = (a1 + a2) and

         A3: x in D2 iff ex a1, a2 st a1 in A1 & a2 in A2 & x = (a1 + a2);

        now

          let x be object;

          x in D1 iff ex a1, a2 st a1 in A1 & a2 in A2 & x = (a1 + a2) by A2;

          hence x in D1 iff x in D2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    begin

    definition

      let K, V, A;

      assume

       A1: A <> {} ;

      :: LMOD_7:def11

      mode Vector of A -> Vector of V means

      : Def11: it is Element of A;

      existence

      proof

        consider x be Element of V such that

         A2: x in A by A1, SUBSET_1: 4;

        take x;

        thus thesis by A2;

      end;

    end

    theorem :: LMOD_7:9

    A1 <> {} & A1 c= A2 implies for x st x is Vector of A1 holds x is Vector of A2

    proof

      assume that

       A1: A1 <> {} and

       A2: A1 c= A2;

      let x;

      assume x is Vector of A1;

      then

      reconsider a = x as Vector of A1;

      a is Element of A1 by A1, Def11;

      then a in A2 by A1, A2, TARSKI:def 3;

      hence thesis by Def11;

    end;

    theorem :: LMOD_7:10



     Th10: a2 in (a1 + W) iff (a1 - a2) in W

    proof

      (a1 - (a1 - a2)) = ((a1 - a1) + a2) by RLVECT_1: 29

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

      .= a2 by RLVECT_1:def 4;

      hence thesis by VECTSP_4: 61;

    end;

    theorem :: LMOD_7:11



     Th11: (a1 + W) = (a2 + W) iff (a1 - a2) in W by VECTSP_4: 55, Th10;

    definition

      let K, V, W;

      :: LMOD_7:def12

      func V .. W -> set means

      : Def12: x in it iff ex a st x = (a + W);

      existence

      proof

        take the set of all (a + W);

        thus thesis;

      end;

      uniqueness

      proof

        defpred X[ set] means ex a st $1 = (a + W);

        thus for S1,S2 be set st (for x holds x in S1 iff X[x]) & (for x holds x in S2 iff X[x]) holds S1 = S2 from XFAMILY:sch 3;

      end;

    end

    registration

      let K, V, W;

      cluster (V .. W) -> non empty;

      coherence

      proof

        (a + W) in (V .. W) by Def12;

        hence thesis;

      end;

    end

    definition

      let K, V, W, a;

      :: LMOD_7:def13

      func a .. W -> Element of (V .. W) equals (a + W);

      coherence by Def12;

    end

    theorem :: LMOD_7:12



     Th12: for x be Element of (V .. W) holds ex a st x = (a .. W)

    proof

      let x be Element of (V .. W);

      consider a such that

       A1: x = (a + W) by Def12;

      take a;

      thus thesis by A1;

    end;

    theorem :: LMOD_7:13

    (a1 .. W) = (a2 .. W) iff (a1 - a2) in W by Th11;

    reserve S1,S2 for Element of (V .. W);

    definition

      let K, V, W, S1;

      :: LMOD_7:def14

      func - S1 -> Element of (V .. W) means S1 = (a .. W) implies it = (( - a) .. W);

      existence

      proof

        consider a1 such that

         A1: S1 = (a1 .. W) by Th12;

         A2:

        now

          let a be Vector of V;

          assume S1 = (a .. W);

          then (a1 - a) in W by A1, Th11;

          then ( - (a1 - a)) in W by VECTSP_4: 22;

          then (( - a1) - ( - a)) in W by Lm1;

          hence (( - a1) .. W) = (( - a) .. W) by Th11;

        end;

        take (( - a1) .. W);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let S,T be Element of (V .. W) such that

         A3: S1 = (a .. W) implies S = (( - a) .. W) and

         A4: S1 = (a .. W) implies T = (( - a) .. W);

        consider a1 such that

         A5: S1 = (a1 .. W) by Th12;



        thus S = (( - a1) .. W) by A3, A5

        .= T by A4, A5;

      end;

      let S2;

      :: LMOD_7:def15

      func S1 + S2 -> Element of (V .. W) means

      : Def15: S1 = (a1 .. W) & S2 = (a2 .. W) implies it = ((a1 + a2) .. W);

      existence

      proof

        consider a1 such that

         A6: S1 = (a1 .. W) by Th12;

        consider a2 such that

         A7: S2 = (a2 .. W) by Th12;

         A8:

        now

          let b1,b2 be Vector of V such that

           A9: S1 = (b1 .. W) and

           A10: S2 = (b2 .. W);



           A11: (a1 - b1) in W by A6, A9, Th11;

          (a2 - b2) in W by A7, A10, Th11;

          then

           A12: ((a1 - b1) + (a2 - b2)) in W by A11, VECTSP_4: 20;

          ((a1 - b1) + (a2 - b2)) = (((a1 - b1) + a2) - b2) by RLVECT_1:def 3

          .= (((a1 + a2) - b1) - b2) by Lm1

          .= ((a1 + a2) - (b1 + b2)) by VECTSP_1: 17;

          hence ((a1 + a2) .. W) = ((b1 + b2) .. W) by A12, Th11;

        end;

        take ((a1 + a2) .. W);

        thus thesis by A8;

      end;

      uniqueness

      proof

        let S,T be Element of (V .. W) such that

         A13: S1 = (a1 .. W) & S2 = (a2 .. W) implies S = ((a1 + a2) .. W) and

         A14: S1 = (a1 .. W) & S2 = (a2 .. W) implies T = ((a1 + a2) .. W);

        consider a1 such that

         A15: S1 = (a1 .. W) by Th12;

        consider a2 such that

         A16: S2 = (a2 .. W) by Th12;



        thus S = ((a1 + a2) .. W) by A13, A15, A16

        .= T by A14, A15, A16;

      end;

    end

    definition

      let K, V, W;

      deffunc U( Element of (V .. W)) = ( - $1);

      :: LMOD_7:def16

      func COMPL W -> UnOp of (V .. W) means (it . S1) = ( - S1);

      existence

      proof

        thus ex U be UnOp of (V .. W) st for S1 holds (U . S1) = U(S1) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        thus for U1,U2 be UnOp of (V .. W) st (for S1 holds (U1 . S1) = U(S1)) & (for S1 holds (U2 . S1) = U(S1)) holds U1 = U2 from UnOpEq;

      end;

      deffunc U( Element of (V .. W), Element of (V .. W)) = ($1 + $2);

      :: LMOD_7:def17

      func ADD W -> BinOp of (V .. W) means

      : Def17: (it . (S1,S2)) = (S1 + S2);

      existence

      proof

        thus ex B be BinOp of (V .. W) st for S1, S2 holds (B . (S1,S2)) = U(S1,S2) from BINOP_1:sch 4;

      end;

      uniqueness

      proof

        thus for B1,B2 be BinOp of (V .. W) st (for S1, S2 holds (B1 . (S1,S2)) = U(S1,S2)) & (for S1, S2 holds (B2 . (S1,S2)) = U(S1,S2)) holds B1 = B2 from BINOP_2:sch 2;

      end;

    end

    definition

      let K, V, W;

      :: LMOD_7:def18

      func V . W -> strict addLoopStr equals addLoopStr (# (V .. W), ( ADD W), (( 0. V) .. W) #);

      coherence ;

    end

    registration

      let K, V, W;

      cluster (V . W) -> non empty;

      coherence ;

    end

    theorem :: LMOD_7:14

    (a .. W) is Element of (V . W);

    definition

      let K, V, W, a;

      :: LMOD_7:def19

      func a . W -> Element of (V . W) equals (a .. W);

      coherence ;

    end

    theorem :: LMOD_7:15



     Th15: for x be Element of (V . W) holds ex a st x = (a . W)

    proof

      let x be Element of (V . W);

      consider a such that

       A1: x = (a .. W) by Th12;

      take a;

      thus thesis by A1;

    end;

    theorem :: LMOD_7:16

    (a1 . W) = (a2 . W) iff (a1 - a2) in W by Th11;

    theorem :: LMOD_7:17



     Th17: ((a . W) + (b . W)) = ((a + b) . W) & ( 0. (V . W)) = (( 0. V) . W)

    proof



      thus ((a . W) + (b . W)) = ((a .. W) + (b .. W)) by Def17

      .= ((a + b) . W) by Def15;

      thus thesis;

    end;

    registration

      let K, V, W;

      cluster (V . W) -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        set G = (V . W);

        hereby

          let x,y be Element of G;

          consider a be Vector of V such that

           A1: x = (a . W) by Th15;

          consider b be Vector of V such that

           A2: y = (b . W) by Th15;

          (x + y) = ((a + b) . W) by A1, A2, Th17;

          hence (x + y) = (y + x) by A1, A2, Th17;

        end;

        hereby

          let x,y,z be Element of G;

          consider a be Vector of V such that

           A3: x = (a . W) by Th15;

          consider b be Vector of V such that

           A4: y = (b . W) by Th15;

          consider c be Vector of V such that

           A5: z = (c . W) by Th15;



           A6: (x + y) = ((a + b) . W) by A3, A4, Th17;



           A7: (y + z) = ((b + c) . W) by A4, A5, Th17;



          thus ((x + y) + z) = (((a + b) + c) . W) by A5, A6, Th17

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

          .= (x + (y + z)) by A3, A7, Th17;

        end;

        hereby

          let x be Element of G;

          consider a be Vector of V such that

           A8: x = (a . W) by Th15;

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



          hence (x + ( 0. G)) = ((a + ( 0. V)) . W) by A8, Th17

          .= x by A8, RLVECT_1: 4;

        end;

        let x be Element of G;

        consider a be Vector of V such that

         A9: x = (a . W) by Th15;

        consider b be Vector of V such that

         A10: (a + b) = ( 0. V) by ALGSTR_0:def 11;

        reconsider b9 = (b . W) as Element of G;

        take b9;



        thus (x + b9) = (( 0. V) . W) by A9, A10, Th17

        .= ( 0. G);

      end;

    end

    reserve S for Element of (V . W);

    definition

      let K, V, W, r, S;

      :: LMOD_7:def20

      func r * S -> Element of (V . W) means

      : Def20: S = (a . W) implies it = ((r * a) . W);

      existence

      proof

        consider a1 such that

         A1: S = (a1 . W) by Th15;

         A2:

        now

          let a;

          assume S = (a . W);

          then (a - a1) in W by A1, Th11;

          then (r * (a - a1)) in W by VECTSP_4: 21;

          then ((r * a) - (r * a1)) in W by VECTSP_1: 23;

          hence ((r * a) . W) = ((r * a1) . W) by Th11;

        end;

        take ((r * a1) . W);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let S1,S2 be Element of (V . W) such that

         A3: S = (a . W) implies S1 = ((r * a) . W) and

         A4: S = (a . W) implies S2 = ((r * a) . W);

        consider a1 such that

         A5: S = (a1 . W) by Th15;



        thus S1 = ((r * a1) . W) by A3, A5

        .= S2 by A4, A5;

      end;

    end

    definition

      let K, V, W;

      :: LMOD_7:def21

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

      : Def21: (it . (r,S)) = (r * S);

      existence

      proof

        deffunc U( Scalar of K, Element of (V . W)) = ($1 * $2);

        consider F be Function of [:the carrier of K, the carrier of (V . W):], the carrier of (V . W) such that

         A1: (F . (r,S)) = U(r,S) from BINOP_1:sch 4;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Function of [:the carrier of K, the carrier of (V . W):], the carrier of (V . W) such that

         A2: (F . (r,S)) = (r * S) and

         A3: (G . (r,S)) = (r * S);

        now

          let r, S;



          thus (F . (r,S)) = (r * S) by A2

          .= (G . (r,S)) by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    begin

    definition

      let K, V, W;

      :: LMOD_7:def22

      func V / W -> strict ModuleStr over K equals ModuleStr (# the carrier of (V . W), the addF of (V . W), (( 0. V) . W), ( LMULT W) #);

      coherence ;

    end

    registration

      let K, V, W;

      cluster (V / W) -> non empty;

      coherence ;

    end

    theorem :: LMOD_7:18

    (a . W) is Vector of (V / W);

    theorem :: LMOD_7:19

    for x be Vector of (V / W) holds x is Element of (V . W);

    definition

      let K, V, W, a;

      :: LMOD_7:def23

      func a / W -> Vector of (V / W) equals (a . W);

      coherence ;

    end

    theorem :: LMOD_7:20



     Th20: for x be Vector of (V / W) holds ex a st x = (a / W)

    proof

      let x be Vector of (V / W);

      consider a such that

       A1: x = (a . W) by Th15;

      take a;

      thus thesis by A1;

    end;

    theorem :: LMOD_7:21

    (a1 / W) = (a2 / W) iff (a1 - a2) in W by Th11;

    theorem :: LMOD_7:22



     Th22: ((a / W) + (b / W)) = ((a + b) / W) & (r * (a / W)) = ((r * a) / W)

    proof



      thus ((a / W) + (b / W)) = ((a . W) + (b . W))

      .= ((a + b) / W) by Th17;



      thus (r * (a / W)) = (( LMULT W) . (r,(a . W))) by VECTSP_1:def 12

      .= (r * (a . W) qua Element of (V . W)) by Def21

      .= ((r * a) / W) by Def20;

    end;



     Lm2: (V / W) is Abelian add-associative right_zeroed right_complementable

    proof



       A1: for x,y,z be Element of (V . W), x9,y9,z9 be Vector of (V / W) st x = x9 & y = y9 & z = z9 holds (x + y) = (x9 + y9);

      thus (V / W) is Abelian

      proof

        let x,y be Vector of (V / W);

        reconsider x9 = x, y9 = y as Element of (V . W);



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

        .= (y + x) by A1;

      end;

      hereby

        let x,y,z be Vector of (V / W);

        reconsider x9 = x, y9 = y, z9 = z as Element of (V . W);



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

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

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

      end;

      hereby

        let x be Vector of (V / W);

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



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

        .= x by RLVECT_1: 4;

      end;

      let x be Vector of (V / W);

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

      consider b be Element of (V . W) such that

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

      reconsider b9 = b as Vector of (V / W);

      take b9;

      thus thesis by A2;

    end;

    theorem :: LMOD_7:23



     Th23: (V / W) is strict LeftMod of K

    proof

      now

        let x,y be Scalar of K, v,w be Vector of (V / W);

        consider a such that

         A1: v = (a / W) by Th20;

        consider b such that

         A2: w = (b / W) by Th20;



         A3: ((x * a) / W) = (x * v) by A1, Th22;



         A4: ((x * b) / W) = (x * w) by A2, Th22;



         A5: ((y * a) / W) = (y * v) by A1, Th22;



        thus (x * (v + w)) = (x * ((a + b) / W)) by A1, A2, Th22

        .= ((x * (a + b)) / W) by Th22

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

        .= ((x * v) + (x * w)) by A3, A4, Th22;



        thus ((x + y) * v) = (((x + y) * a) / W) by A1, Th22

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

        .= ((x * v) + (y * v)) by A3, A5, Th22;



        thus ((x * y) * v) = (((x * y) * a) / W) by A1, Th22

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

        .= (x * ((y * a) / W)) by Th22

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



        thus (( 1_ K) * v) = ((( 1_ K) * a) / W) by A1, Th22

        .= v by A1, VECTSP_1:def 17;

      end;

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

    end;

    registration

      let K, V, W;

      cluster (V / W) -> vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Th23;

    end