lmod_6.miz



    begin

    reserve x for set,

K for Ring,

r for Scalar of K,

V,M,M1,M2,N for LeftMod of K,

a for Vector of V,

m,m1,m2 for Vector of M,

n,n1,n2 for Vector of N,

A for Subset of V,

l for Linear_Combination of A,

W,W1,W2,W3 for Subspace of V;

    notation

      let K, V;

      synonym Submodules (V) for Subspaces (V);

    end

    theorem :: LMOD_6:1

    M1 = the ModuleStr of M2 implies (x in M1 iff x in M2);

    theorem :: LMOD_6:2

    for v be Vector of the ModuleStr of V st a = v holds (r * a) = (r * v)

    proof

      let v be Vector of the ModuleStr of V such that

       A1: a = v;

      

      thus (r * a) = (the lmult of V . (r,a)) by VECTSP_1:def 12

      .= (r * v) by A1, VECTSP_1:def 12;

    end;

    theorem :: LMOD_6:3

    

     Th3: the ModuleStr of V is strict Subspace of V

    proof

      ( (Omega). V) = the ModuleStr of V by VECTSP_4:def 4;

      hence thesis;

    end;

    theorem :: LMOD_6:4

    

     Th4: V is Subspace of ( (Omega). V)

    proof

      set W = ( (Omega). V);

      

       A1: W = the ModuleStr of V by VECTSP_4:def 4;

      then

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

      ( dom the lmult of W) = [:the carrier of K, the carrier of W:] by FUNCT_2:def 1;

      then

       A3: the lmult of V = (the lmult of W | [:the carrier of K, the carrier of V:]) by A1, RELAT_1: 68;

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

      then the addF of V = (the addF of W || the carrier of V) by A1, RELAT_1: 68;

      hence thesis by A1, A2, A3, VECTSP_4:def 2;

    end;

    begin

    definition

      let K;

      :: original: trivial

      redefine

      :: LMOD_6:def1

      attr K is trivial means ( 0. K) = ( 1_ K);

      compatibility

      proof

        thus K is trivial implies ( 0. K) = ( 1_ K);

        assume

         A1: ( 0. K) = ( 1_ K);

        now

          let x be Scalar of K;

          

          thus x = (x * ( 1_ K))

          .= ( 0. K) by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: LMOD_6:5

    

     Th5: K is trivial implies (for r holds r = ( 0. K)) & for a holds a = ( 0. V)

    proof

      assume K is trivial;

      then

       A1: ( 0. K) = ( 1_ K);

       A2:

      now

        let a;

        

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

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

      end;

      now

        let r;

        

        thus r = (r * ( 1_ K))

        .= ( 0. K) by A1;

      end;

      hence thesis by A2;

    end;

    theorem :: LMOD_6:6

    K is trivial implies V is trivial by Th5;

    theorem :: LMOD_6:7

    V is trivial iff the ModuleStr of V = ( (0). V)

    proof

      set X = the carrier of ( (0). V);

      reconsider W = the ModuleStr of V as strict Subspace of V by Th3;

      reconsider Z = ( (0). V) as Subspace of W by VECTSP_4: 39;

       A1:

      now

        assume W <> Z;

        then

        consider a such that

         A2: not a in Z by VECTSP_4: 32;

         not a in X by A2;

        then not a in {( 0. V)} by VECTSP_4:def 3;

        then a <> ( 0. V) by TARSKI:def 1;

        hence V is non trivial;

      end;

      now

        assume V is non trivial;

        then

        consider a such that

         A3: a <> ( 0. V);

         not a in {( 0. V)} by A3, TARSKI:def 1;

        then not a in X by VECTSP_4:def 3;

        hence W <> ( (0). V);

      end;

      hence thesis by A1;

    end;

    begin

    definition

      let K, V;

      let W be strict Subspace of V;

      :: LMOD_6:def2

      func @ W -> Element of ( Submodules V) equals W;

      coherence by VECTSP_5:def 3;

    end

    theorem :: LMOD_6:8

    

     Th8: for A be Subset of W holds A is Subset of V

    proof

      let A be Subset of W;

      the carrier of W c= the carrier of V by VECTSP_4:def 2;

      hence thesis by XBOOLE_1: 1;

    end;

    definition

      let K, V, W;

      let A be Subset of W;

      :: LMOD_6:def3

      func @ A -> Subset of V equals A;

      coherence by Th8;

    end

    registration

      let K, V, W;

      let A be non empty Subset of W;

      cluster ( @ A) -> non empty;

      coherence ;

    end

    theorem :: LMOD_6:9

    x in ( [#] V) iff x in V;

    theorem :: LMOD_6:10

    x in ( @ ( [#] W)) iff x in W;

    theorem :: LMOD_6:11

    

     Th11: A c= ( [#] ( Lin A))

    proof

      let x be object;

      assume x in A;

      then x in ( Lin A) by MOD_3: 5;

      hence thesis;

    end;

    theorem :: LMOD_6:12

    

     Th12: A <> {} & A is linearly-closed implies ( Sum l) in A

    proof

      assume

       A1: A <> {} & A is linearly-closed;

      now

        per cases ;

          suppose ( 0. K) <> ( 1_ K);

          hence thesis by A1, VECTSP_6: 14;

        end;

          suppose ( 0. K) = ( 1_ K);

          then K is trivial;

          then ( Sum l) = ( 0. V) by Th5;

          hence thesis by A1, VECTSP_4: 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: LMOD_6:13

    ( 0. V) in A & A is linearly-closed implies A = ( [#] ( Lin A))

    proof

      assume

       A1: ( 0. V) in A & A is linearly-closed;

      thus A c= ( [#] ( Lin A)) by Th11;

      let x be object;

      assume x in ( [#] ( Lin A));

      then x in ( Lin A);

      then ex l st x = ( Sum l) by MOD_3: 4;

      hence thesis by A1, Th12;

    end;

    begin

    definition

      let K, V, a;

      :: LMOD_6:def4

      func <:a:> -> strict Subspace of V equals ( Lin {a});

      correctness ;

    end

    begin

    definition

      let K, M, N;

      :: LMOD_6:def5

      pred M c= N means M is Subspace of N;

      reflexivity by VECTSP_4: 24;

    end

    theorem :: LMOD_6:14

    

     Th14: for x be object holds M c= N implies (x in M implies x in N) & (x is Vector of M implies x is Vector of N) by VECTSP_4: 9, VECTSP_4: 10;

    theorem :: LMOD_6:15

    M c= N implies ( 0. M) = ( 0. N) & (m1 = n1 & m2 = n2 implies (m1 + m2) = (n1 + n2)) & (m = n implies (r * m) = (r * n)) & (m = n implies ( - n) = ( - m)) & (m1 = n1 & m2 = n2 implies (m1 - m2) = (n1 - n2)) & ( 0. N) in M & ( 0. M) in N & (n1 in M & n2 in M implies (n1 + n2) in M) & (n in M implies (r * n) in M) & (n in M implies ( - n) in M) & (n1 in M & n2 in M implies (n1 - n2) in M) by VECTSP_4: 11, VECTSP_4: 13, VECTSP_4: 14, VECTSP_4: 15, VECTSP_4: 16, VECTSP_4: 17, VECTSP_4: 19, VECTSP_4: 20, VECTSP_4: 21, VECTSP_4: 22, VECTSP_4: 23;

    theorem :: LMOD_6:16

    M1 c= N & M2 c= N implies ( 0. M1) = ( 0. M2) & ( 0. M1) in M2 & (the carrier of M1 c= the carrier of M2 implies M1 c= M2) & ((for n st n in M1 holds n in M2) implies M1 c= M2) & (the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2) & ( (0). M1) c= M2 by VECTSP_4: 12, VECTSP_4: 18, VECTSP_4: 27, VECTSP_4: 28, VECTSP_4: 29, VECTSP_4: 40;

    theorem :: LMOD_6:17

    for V,M be strict LeftMod of K holds V c= M & M c= V implies V = M by VECTSP_4: 25;

    theorem :: LMOD_6:18

    V c= M & M c= N implies V c= N by VECTSP_4: 26;

    theorem :: LMOD_6:19

    M c= N implies ( (0). M) c= N by VECTSP_4: 38;

    theorem :: LMOD_6:20

    M c= N implies ( (0). N) c= M by VECTSP_4: 39;

    theorem :: LMOD_6:21

    M c= N implies M c= ( (Omega). N)

    proof

      assume M c= N;

      then

       A1: M is Subspace of N;

      N is Subspace of ( (Omega). N) by Th4;

      then M is Subspace of ( (Omega). N) by A1, VECTSP_4: 26;

      hence thesis;

    end;

    theorem :: LMOD_6:22

    W1 c= (W1 + W2) & W2 c= (W1 + W2) by VECTSP_5: 7;

    theorem :: LMOD_6:23

    (W1 /\ W2) c= W1 & (W1 /\ W2) c= W2 by VECTSP_5: 15;

    theorem :: LMOD_6:24

    W1 c= W2 implies (W1 /\ W3) c= (W2 /\ W3) by VECTSP_5: 17;

    theorem :: LMOD_6:25

    W1 c= W3 implies (W1 /\ W2) c= W3 by VECTSP_5: 18;

    theorem :: LMOD_6:26

    W1 c= W2 & W1 c= W3 implies W1 c= (W2 /\ W3) by VECTSP_5: 19;

    theorem :: LMOD_6:27

    (W1 /\ W2) c= (W1 + W2) by VECTSP_5: 23;

    theorem :: LMOD_6:28

    ((W1 /\ W2) + (W2 /\ W3)) c= (W2 /\ (W1 + W3)) by VECTSP_5: 26;

    theorem :: LMOD_6:29

    W1 c= W2 implies (W2 /\ (W1 + W3)) = ((W1 /\ W2) + (W2 /\ W3)) by VECTSP_5: 27;

    theorem :: LMOD_6:30

    (W2 + (W1 /\ W3)) c= ((W1 + W2) /\ (W2 + W3)) by VECTSP_5: 28;

    theorem :: LMOD_6:31

    W1 c= W2 implies (W2 + (W1 /\ W3)) = ((W1 + W2) /\ (W2 + W3)) by VECTSP_5: 29;

    theorem :: LMOD_6:32

    W1 c= W2 implies W1 c= (W2 + W3) by VECTSP_5: 33;

    theorem :: LMOD_6:33

    W1 c= W3 & W2 c= W3 implies (W1 + W2) c= W3 by VECTSP_5: 34;

    theorem :: LMOD_6:34

    for A,B be Subset of V st A c= B holds ( Lin A) c= ( Lin B) by MOD_3: 10;

    theorem :: LMOD_6:35

    for A,B be Subset of V holds ( Lin (A /\ B)) c= (( Lin A) /\ ( Lin B)) by MOD_3: 13;

    theorem :: LMOD_6:36

    

     Th36: M1 c= M2 implies ( [#] M1) c= ( [#] M2)

    proof

      assume

       A1: M1 c= M2;

      let x be object;

      assume x in ( [#] M1);

      then x in M1;

      then x in M2 by A1, Th14;

      hence thesis;

    end;

    theorem :: LMOD_6:37

    

     Th37: W1 c= W2 iff for a st a in W1 holds a in W2 by VECTSP_4: 8, VECTSP_4: 28;

    theorem :: LMOD_6:38

    

     Th38: W1 c= W2 iff ( [#] W1) c= ( [#] W2)

    proof

      thus W1 c= W2 implies ( [#] W1) c= ( [#] W2) by Th36;

      assume ( [#] W1) c= ( [#] W2);

      then for a st a in W1 holds a in W2;

      hence thesis by Th37;

    end;

    theorem :: LMOD_6:39

    W1 c= W2 iff ( @ ( [#] W1)) c= ( @ ( [#] W2)) by Th38;

    theorem :: LMOD_6:40

    ( (0). W) c= V & ( (0). V) c= W & ( (0). W1) c= W2 by VECTSP_4: 38, VECTSP_4: 39, VECTSP_4: 40;