matrix_1.miz



    begin

    reserve x,y,z for object,

i,j,n,m for Nat,

D for non empty set,

K for non empty doubleLoopStr,

s,t for FinSequence,

a,a1,a2,b1,b2,d for Element of D,

p,p1,p2,q,r for FinSequence of D,

F for add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr;

    definition

      let K be non empty 1-sorted;

      mode Matrix of K is Matrix of the carrier of K;

      let n;

      mode Matrix of n,K is Matrix of n, n, the carrier of K;

      let m;

      mode Matrix of n,m,K is Matrix of n, m, the carrier of K;

    end

    reserve A,B for Matrix of n, K;

    definition

      let K, n;

      :: MATRIX_1:def1

      func n -Matrices_over K -> set equals (n -tuples_on (n -tuples_on the carrier of K));

      coherence ;

      :: MATRIX_1:def2

      func 0. (K,n) -> Matrix of n, K equals (n |-> (n |-> ( 0. K)));

      coherence by MATRIX_0: 10;

      :: MATRIX_1:def3

      func 1. (K,n) -> Matrix of n, K means

      : Def3: (for i st [i, i] in ( Indices it ) holds (it * (i,i)) = ( 1. K)) & for i, j st [i, j] in ( Indices it ) & i <> j holds (it * (i,j)) = ( 0. K);

      existence

      proof

        defpred P[ set, set, set] means ($1 = $2 implies $3 = ( 1. K)) & ($1 <> $2 implies $3 = ( 0. K));

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        

         A1: for i, j st [i, j] in [:( Seg n1), ( Seg n1):] holds ex x be Element of K st P[i, j, x]

        proof

          let i, j;

          assume [i, j] in [:( Seg n1), ( Seg n1):];

          i = j implies P[i, j, ( 1. K)];

          hence thesis;

        end;

        consider M be Matrix of n1, K such that

         A2: for i, j st [i, j] in ( Indices M) holds P[i, j, (M * (i,j))] from MATRIX_0:sch 2( A1);

        reconsider M as Matrix of n, K;

        take M;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of n, K;

        assume that

         A3: for i st [i, i] in ( Indices M1) holds (M1 * (i,i)) = ( 1. K) and

         A4: for i, j st [i, j] in ( Indices M1) & i <> j holds (M1 * (i,j)) = ( 0. K) and

         A5: for i st [i, i] in ( Indices M2) holds (M2 * (i,i)) = ( 1. K) and

         A6: for i, j st [i, j] in ( Indices M2) & i <> j holds (M2 * (i,j)) = ( 0. K);

        

         A7: ( Indices M1) = ( Indices M2) by MATRIX_0: 26;

         A8:

        now

          let i, j;

          assume

           A9: [i, j] in ( Indices M1);

           A10:

          now

            assume

             A11: i <> j;

            then (M1 * (i,j)) = ( 0. K) by A4, A9;

            hence (M1 * (i,j)) = (M2 * (i,j)) by A7, A6, A9, A11;

          end;

          now

            assume

             A12: i = j;

            then (M1 * (i,j)) = ( 1. K) by A3, A9;

            hence (M1 * (i,j)) = (M2 * (i,j)) by A7, A5, A9, A12;

          end;

          hence (M1 * (i,j)) = (M2 * (i,j)) by A10;

        end;

        

         A13: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

        ( len M1) = n & ( width M1) = n by MATRIX_0: 24;

        hence thesis by A8, A13, MATRIX_0: 21;

      end;

      let A;

      :: MATRIX_1:def4

      func - A -> Matrix of n, K means

      : Def4: for i, j holds [i, j] in ( Indices A) implies (it * (i,j)) = ( - (A * (i,j)));

      existence

      proof

        deffunc F( Nat, Nat) = ( - (A * ($1,$2)));

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        consider M be Matrix of n1, K such that

         A14: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        ( Indices A) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then

         A15: ( Indices A) = ( Indices M) by MATRIX_0: 24;

        reconsider M as Matrix of n, K;

        take M;

        thus thesis by A14, A15;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of n, K;

        assume that

         A16: for i, j st [i, j] in ( Indices A) holds (M1 * (i,j)) = ( - (A * (i,j))) and

         A17: for i, j st [i, j] in ( Indices A) holds (M2 * (i,j)) = ( - (A * (i,j)));

         A18:

        now

          let i, j;

          assume

           A19: [i, j] in ( Indices A);

          then (M1 * (i,j)) = ( - (A * (i,j))) by A16;

          hence (M1 * (i,j)) = (M2 * (i,j)) by A17, A19;

        end;

        ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then ( Indices A) = ( Indices M1) by MATRIX_0: 24;

        hence thesis by A18, MATRIX_0: 27;

      end;

      let B;

      :: MATRIX_1:def5

      func A + B -> Matrix of n, K means

      : Def5: for i, j holds [i, j] in ( Indices A) implies (it * (i,j)) = ((A * (i,j)) + (B * (i,j)));

      existence

      proof

        deffunc F( Nat, Nat) = ((A * ($1,$2)) + (B * ($1,$2)));

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        consider M be Matrix of n1, K such that

         A20: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        ( Indices A) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then

         A21: ( Indices A) = ( Indices M) by MATRIX_0: 24;

        reconsider M as Matrix of n, K;

        take M;

        thus thesis by A20, A21;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of n, K;

        assume that

         A22: for i, j st [i, j] in ( Indices A) holds (M1 * (i,j)) = ((A * (i,j)) + (B * (i,j))) and

         A23: for i, j st [i, j] in ( Indices A) holds (M2 * (i,j)) = ((A * (i,j)) + (B * (i,j)));

         A24:

        now

          let i, j;

          assume

           A25: [i, j] in ( Indices A);

          then (M1 * (i,j)) = ((A * (i,j)) + (B * (i,j))) by A22;

          hence (M1 * (i,j)) = (M2 * (i,j)) by A23, A25;

        end;

        ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then ( Indices A) = ( Indices M1) by MATRIX_0: 24;

        hence thesis by A24, MATRIX_0: 27;

      end;

    end

    registration

      let K, n;

      cluster (n -Matrices_over K) -> non empty;

      coherence ;

    end

    theorem :: MATRIX_1:1

    

     Th1: [i, j] in ( Indices ( 0. (K,n))) implies (( 0. (K,n)) * (i,j)) = ( 0. K)

    proof

      reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

      set M = ( 0. (K,n));

      assume

       A1: [i, j] in ( Indices M);

      then

       A2: [i, j] in [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      then j in ( Seg n) by ZFMISC_1: 87;

      then

       A3: ((n1 |-> ( 0. K)) . j) = ( 0. K) by FUNCOP_1: 7;

      i in ( Seg n) by A2, ZFMISC_1: 87;

      then (M . i) = (n1 |-> ( 0. K)) by FUNCOP_1: 7;

      hence thesis by A1, A3, MATRIX_0:def 5;

    end;

    theorem :: MATRIX_1:2

    

     Th2: x is Element of (n -Matrices_over K) iff x is Matrix of n, K

    proof

      thus x is Element of (n -Matrices_over K) implies x is Matrix of n, K

      proof

        assume x is Element of (n -Matrices_over K);

        then

        reconsider x as Element of (n -tuples_on (n -tuples_on the carrier of K));

        

         A1: ( len x) = n by CARD_1:def 7;

        ex m st for y st y in ( rng x) holds ex q be FinSequence of K st y = q & ( len q) = m

        proof

          take n;

          let y;

          

           A2: ( rng x) c= (n -tuples_on the carrier of K) by FINSEQ_1:def 4;

          assume y in ( rng x);

          then

          reconsider q = y as Element of (n -tuples_on the carrier of K) by A2;

          reconsider q as FinSequence of K;

          take q;

          thus thesis by CARD_1:def 7;

        end;

        then

        reconsider x as Matrix of the carrier of K by MATRIX_0: 9;

        for q be FinSequence of K st q in ( rng x) holds ( len q) = n

        proof

          let q be FinSequence of K;

          

           A3: ( rng x) c= (n -tuples_on the carrier of K) by FINSEQ_1:def 4;

          assume q in ( rng x);

          then

          reconsider q as Element of (n -tuples_on the carrier of K) by A3;

          ( len q) = n by CARD_1:def 7;

          hence thesis;

        end;

        hence thesis by A1, MATRIX_0:def 2;

      end;

      assume x is Matrix of n, K;

      then

      reconsider x as Matrix of n, K;

      

       A4: ( len x) = n by MATRIX_0:def 2;

      then

      reconsider x as Element of (n -tuples_on (the carrier of K * )) by FINSEQ_2: 92;

      ( rng x) c= (n -tuples_on the carrier of K)

      proof

        let y be object;

        assume

         A5: y in ( rng x);

        ( rng x) c= (the carrier of K * ) by FINSEQ_1:def 4;

        then

        reconsider p = y as FinSequence of K by A5, FINSEQ_1:def 11;

        ( len p) = n by A5, MATRIX_0:def 2;

        then p is Element of (n -tuples_on the carrier of K) by FINSEQ_2: 92;

        hence thesis;

      end;

      then x is FinSequence of (n -tuples_on the carrier of K) by FINSEQ_1:def 4;

      hence thesis by A4, FINSEQ_2: 92;

    end;

    definition

      let K be non empty ZeroStr;

      let M be Matrix of K;

      :: MATRIX_1:def6

      attr M is diagonal means

      : def6: for i, j st [i, j] in ( Indices M) & (M * (i,j)) <> ( 0. K) holds i = j;

    end

    registration

      let n, K;

      cluster diagonal for Matrix of n, K;

      existence

      proof

        take ( 1. (K,n));

        let i, j;

        thus thesis by Def3;

      end;

    end

    reserve A,A9,B,B9,C for Matrix of n, F;

    theorem :: MATRIX_1:3

    

     Th3: (A + B) = (B + A)

    proof

      

       A1: ( Indices A) = ( Indices (A + B)) by MATRIX_0: 26;

      

       A2: ( Indices A) = ( Indices B) by MATRIX_0: 26;

      now

        let i, j;

        assume

         A3: [i, j] in ( Indices (A + B));

        

        hence ((A + B) * (i,j)) = ((A * (i,j)) + (B * (i,j))) by A1, Def5

        .= ((B + A) * (i,j)) by A2, A1, A3, Def5;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIX_1:4

    

     Th4: ((A + B) + C) = (A + (B + C))

    proof

      

       A1: ( Indices A) = ( Indices ((A + B) + C)) by MATRIX_0: 26;

      

       A2: ( Indices A) = ( Indices (A + B)) by MATRIX_0: 26;

      

       A3: ( Indices A) = ( Indices B) by MATRIX_0: 26;

      now

        let i, j;

        assume

         A4: [i, j] in ( Indices ((A + B) + C));

        

        hence (((A + B) + C) * (i,j)) = (((A + B) * (i,j)) + (C * (i,j))) by A1, A2, Def5

        .= (((A * (i,j)) + (B * (i,j))) + (C * (i,j))) by A1, A4, Def5

        .= ((A * (i,j)) + ((B * (i,j)) + (C * (i,j)))) by RLVECT_1:def 3

        .= ((A * (i,j)) + ((B + C) * (i,j))) by A3, A1, A4, Def5

        .= ((A + (B + C)) * (i,j)) by A1, A4, Def5;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIX_1:5

    

     Th5: (A + ( 0. (F,n))) = A

    proof

      

       A1: ( Indices A) = ( Indices (A + ( 0. (F,n)))) by MATRIX_0: 26;

      

       A2: ( Indices A) = ( Indices ( 0. (F,n))) by MATRIX_0: 26;

      now

        let i, j;

        assume

         A3: [i, j] in ( Indices (A + ( 0. (F,n))));

        

        hence ((A + ( 0. (F,n))) * (i,j)) = ((A * (i,j)) + (( 0. (F,n)) * (i,j))) by A1, Def5

        .= ((A * (i,j)) + ( 0. F)) by A1, A2, A3, Th1

        .= (A * (i,j)) by RLVECT_1: 4;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIX_1:6

    

     Th6: (A + ( - A)) = ( 0. (F,n))

    proof

      

       A1: ( Indices A) = ( Indices (A + ( - A))) by MATRIX_0: 26;

      

       A2: ( Indices A) = ( Indices ( 0. (F,n))) by MATRIX_0: 26;

      now

        let i, j;

        assume

         A3: [i, j] in ( Indices (A + ( - A)));

        

        hence ((A + ( - A)) * (i,j)) = ((A * (i,j)) + (( - A) * (i,j))) by A1, Def5

        .= ((A * (i,j)) + ( - (A * (i,j)))) by A1, A3, Def4

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

        .= (( 0. (F,n)) * (i,j)) by A2, A1, A3, Th1;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    definition

      let F, n;

      :: MATRIX_1:def7

      func n -G_Matrix_over F -> strict AbGroup means the carrier of it = (n -Matrices_over F) & (for A, B holds (the addF of it . (A,B)) = (A + B)) & ( 0. it ) = ( 0. (F,n));

      existence

      proof

        reconsider A0 = ( 0. (F,n)) as Element of (n -Matrices_over F);

        defpred P[ Element of (n -Matrices_over F), Element of (n -Matrices_over F), Element of (n -Matrices_over F)] means ex A, B st $1 = A & $2 = B & $3 = (A + B);

        

         A1: for a,b be Element of (n -Matrices_over F) holds ex c be Element of (n -Matrices_over F) st P[a, b, c]

        proof

          let a,b be Element of (n -Matrices_over F);

          reconsider B = b as Matrix of n, F by Th2;

          reconsider A = a as Matrix of n, F by Th2;

          reconsider c = (A + B) as Element of (n -Matrices_over F) by Th2;

          take c;

          thus thesis;

        end;

        consider h be BinOp of (n -Matrices_over F) such that

         A2: for a,b be Element of (n -Matrices_over F) holds P[a, b, (h . (a,b))] from BINOP_1:sch 3( A1);

        set G = addLoopStr (# (n -Matrices_over F), h, A0 #);

        

         A3: (h . (A,B)) = (A + B)

        proof

          A is Element of (n -Matrices_over F) & B is Element of (n -Matrices_over F) by Th2;

          then ex A9, B9 st A = A9 & B = B9 & (h . (A,B)) = (A9 + B9) by A2;

          hence thesis;

        end;

        

         A4: for a be Element of (n -Matrices_over F) holds ex b be Element of (n -Matrices_over F) st ex A st a = A & b = ( - A)

        proof

          let a be Element of (n -Matrices_over F);

          reconsider A = a as Matrix of n, F by Th2;

          reconsider b = ( - A) as Element of (n -Matrices_over F) by Th2;

          take b;

          thus thesis;

        end;

        G is Abelian add-associative right_zeroed right_complementable

        proof

          thus G is Abelian

          proof

            let a,b be Element of G;

            reconsider A = a, B = b as Matrix of n, F by Th2;

            

            thus (a + b) = (A + B) by A3

            .= (B + A) by Th3

            .= (b + a) by A3;

          end;

          hereby

            let a,b,c be Element of G;

            reconsider A = a, B = b, C = c as Matrix of n, F by Th2;

            

            thus ((a + b) + c) = (h . ((A + B),C)) by A3

            .= ((A + B) + C) by A3

            .= (A + (B + C)) by Th4

            .= (h . (A,(B + C))) by A3

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

          end;

          hereby

            let a be Element of G;

            reconsider A = a as Matrix of n, F by Th2;

            

            thus (a + ( 0. G)) = (A + ( 0. (F,n))) by A3

            .= a by Th5;

          end;

          let a be Element of G;

          consider b be Element of (n -Matrices_over F) such that

           A5: ex A st a = A & b = ( - A) by A4;

          consider A such that

           A6: a = A and

           A7: b = ( - A) by A5;

          reconsider b = ( - A) as Element of G by A7;

          take b;

          

          thus (a + b) = (A + ( - A)) by A3, A6

          .= ( 0. G) by Th6;

        end;

        then

        reconsider G as strict AbGroup;

        take G;

        thus thesis by A3;

      end;

      uniqueness

      proof

        thus for G1,G2 be strict AbGroup st the carrier of G1 = (n -Matrices_over F) & (for A, B holds (the addF of G1 . (A,B)) = (A + B)) & ( 0. G1) = ( 0. (F,n)) & the carrier of G2 = (n -Matrices_over F) & (for A, B holds (the addF of G2 . (A,B)) = (A + B)) & ( 0. G2) = ( 0. (F,n)) holds G1 = G2

        proof

          let G1,G2 be strict AbGroup;

          assume that

           A8: the carrier of G1 = (n -Matrices_over F) and

           A9: for A, B holds (the addF of G1 . (A,B)) = (A + B) and

           A10: ( 0. G1) = ( 0. (F,n)) & the carrier of G2 = (n -Matrices_over F) and

           A11: for A, B holds (the addF of G2 . (A,B)) = (A + B) and

           A12: ( 0. G2) = ( 0. (F,n));

          now

            let a,b be Element of G1;

            reconsider A = a, B = b as Matrix of n, F by A8, Th2;

            

            thus (the addF of G1 . (a,b)) = (A + B) by A9

            .= (the addF of G2 . (a,b)) by A11;

          end;

          hence thesis by A8, A10, A12, BINOP_1: 2;

        end;

      end;

    end

    begin

    reserve i,j,n for Nat,

K for Field,

a,b for Element of K;

    definition

      let n, K;

      let M be Matrix of n, K;

      :: MATRIX_1:def8

      attr M is upper_triangular means for i, j st [i, j] in ( Indices M) & i > j holds (M * (i,j)) = ( 0. K);

      :: MATRIX_1:def9

      attr M is lower_triangular means for i, j st [i, j] in ( Indices M) & i < j holds (M * (i,j)) = ( 0. K);

    end

    registration

      let n, K;

      cluster -> upper_triangular lower_triangular for diagonal Matrix of n, K;

      coherence by def6;

    end

    registration

      let n, K;

      cluster lower_triangular upper_triangular for Matrix of n, K;

      existence

      proof

        set M = the diagonal Matrix of n, K;

        take M;

        thus thesis;

      end;

    end

    theorem :: MATRIX_1:7

    (((n,n) --> a) + ((n,n) --> b)) = ((n,n) --> (a + b))

    proof

      

       A1: ( Indices ((n,n) --> a)) = ( Indices ((n,n) --> (a + b))) by MATRIX_0: 26;

      

       A2: ( Indices ((n,n) --> a)) = ( Indices ((n,n) --> b)) by MATRIX_0: 26;

      now

        let i, j;

        assume

         A3: [i, j] in ( Indices ((n,n) --> (a + b)));

        then (((n,n) --> a) * (i,j)) = a by A1, MATRIX_0: 46;

        then ((((n,n) --> a) * (i,j)) + (((n,n) --> b) * (i,j))) = (a + b) by A2, A1, A3, MATRIX_0: 46;

        hence ((((n,n) --> a) * (i,j)) + (((n,n) --> b) * (i,j))) = (((n,n) --> (a + b)) * (i,j)) by A3, MATRIX_0: 46;

      end;

      hence thesis by A1, Def5;

    end;

    begin

    reserve x,y,x1,x2,y1,y2 for set,

i,j,k,l,n,m for Nat,

D for non empty set,

K for Field,

s,s2 for FinSequence,

a,b,c,d for Element of D,

q,r for FinSequence of D,

a9,b9 for Element of K;

    definition

      let IT be set;

      :: MATRIX_1:def10

      attr IT is permutational means

      : Def3: ex n st for x st x in IT holds x is Permutation of ( Seg n);

    end

    registration

      cluster permutational non empty for set;

      existence

      proof

        set n = the Nat;

        set p = the Permutation of ( Seg n);

        take P = {p};

        thus P is permutational

        proof

          take n;

          let x;

          assume x in P;

          hence thesis by TARSKI:def 1;

        end;

        thus thesis;

      end;

    end

    definition

      let P be permutational non empty set;

      :: MATRIX_1:def11

      func len P -> Nat means

      : Def4: ex s st s in P & it = ( len s);

      existence

      proof

        set x = the Element of P;

        consider n such that

         A1: for y st y in P holds y is Permutation of ( Seg n) by Def3;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        reconsider q = x as Permutation of ( Seg n) by A1;

        

         A2: ( dom q) = ( Seg n) by FUNCT_2: 52;

        then

        reconsider q as FinSequence by FINSEQ_1:def 2;

        take n, q;

        thus thesis by A2, FINSEQ_1:def 3;

      end;

      uniqueness

      proof

        let n1,n2 be Nat;

        given s1 be FinSequence such that

         A3: s1 in P and

         A4: n1 = ( len s1);

        consider n such that

         A5: for y st y in P holds y is Permutation of ( Seg n) by Def3;

        s1 is Function of ( Seg n), ( Seg n) by A3, A5;

        then n in NAT & ( dom s1) = ( Seg n) by FUNCT_2: 52, ORDINAL1:def 12;

        then

         A6: ( len s1) = n by FINSEQ_1:def 3;

        given s2 such that

         A7: s2 in P and

         A8: n2 = ( len s2);

        s2 is Permutation of ( Seg n) by A7, A5;

        then ( dom s2) = ( Seg n) by FUNCT_2: 52;

        hence thesis by A4, A8, A6, FINSEQ_1:def 3;

      end;

    end

    definition

      let P be permutational non empty set;

      :: original: len

      redefine

      func len P -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    definition

      let P be permutational non empty set;

      :: original: Element

      redefine

      mode Element of P -> Permutation of ( Seg ( len P)) ;

      coherence

      proof

        let x be Element of P;

        consider n such that

         A1: for y st y in P holds y is Permutation of ( Seg n) by Def3;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        reconsider q = x as Permutation of ( Seg n) by A1;

        

         A2: ( dom q) = ( Seg n) by FUNCT_2: 52;

        then

        reconsider q as FinSequence by FINSEQ_1:def 2;

        ( len q) = n by A2, FINSEQ_1:def 3;

        then ( Seg ( len P)) = ( Seg n) by Def4;

        hence thesis by A1;

      end;

    end

    theorem :: MATRIX_1:8

    ex P be permutational non empty set st ( len P) = n

    proof

      set p = the Permutation of ( Seg n);

      set P = {p};

      now

        take n;

        let x;

        assume x in P;

        hence x is Permutation of ( Seg n) by TARSKI:def 1;

      end;

      then

      reconsider P as permutational non empty set by Def3;

      take P;

      ( len P) = n

      proof

        set x = the Element of P;

        reconsider y = x as Function of ( Seg n), ( Seg n) by TARSKI:def 1;

        

         A1: ( dom y) = ( Seg n) by FUNCT_2: 52;

        then

        reconsider s = y as FinSequence by FINSEQ_1:def 2;

        n in NAT & ( len P) = ( len s) by Def4, ORDINAL1:def 12;

        hence thesis by A1, FINSEQ_1:def 3;

      end;

      hence thesis;

    end;

    definition

      let n;

      :: MATRIX_1:def12

      func Permutations n -> set means

      : Def5: x in it iff x is Permutation of ( Seg n);

      existence

      proof

        defpred P[ object] means $1 is Permutation of ( Seg n);

        consider P be set such that

         A1: for x be object holds x in P iff x in ( Funcs (( Seg n),( Seg n))) & P[x] from XBOOLE_0:sch 1;

        take P;

        let x;

        thus x in P implies x is Permutation of ( Seg n) by A1;

        assume

         A2: x is Permutation of ( Seg n);

        then x in ( Funcs (( Seg n),( Seg n))) by FUNCT_2: 9;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P1,P2 be set;

        assume that

         A3: for x holds x in P1 iff x is Permutation of ( Seg n) and

         A4: for x holds x in P2 iff x is Permutation of ( Seg n);

         A5:

        now

          let x be object;

          assume x in P2;

          then x is Permutation of ( Seg n) by A4;

          hence x in P1 by A3;

        end;

        now

          let x be object;

          assume x in P1;

          then x is Permutation of ( Seg n) by A3;

          hence x in P2 by A4;

        end;

        hence thesis by A5, TARSKI: 2;

      end;

    end

    registration

      let n;

      cluster ( Permutations n) -> permutational non empty;

      coherence

      proof

        defpred P[ object] means $1 is Permutation of ( Seg n);

        consider P be set such that

         A1: for x be object holds x in P iff x in ( Funcs (( Seg n),( Seg n))) & P[x] from XBOOLE_0:sch 1;

        ( idseq n) in ( Funcs (( Seg n),( Seg n))) by FUNCT_2: 9;

        then

        reconsider P as non empty set by A1;

        now

          take n;

          let x;

          assume x in P;

          hence x is Permutation of ( Seg n) by A1;

        end;

        then

        reconsider P as permutational non empty set by Def3;

        x in P iff x is Permutation of ( Seg n) by A1, FUNCT_2: 9;

        hence thesis by Def5;

      end;

    end

    theorem :: MATRIX_1:9

    ( len ( Permutations n)) = n

    proof

      set x = the Element of ( Permutations n);

      reconsider q = x as Permutation of ( Seg n) by Def5;

      

       A1: ( dom q) = ( Seg n) by FUNCT_2: 52;

      then

      reconsider q as FinSequence by FINSEQ_1:def 2;

      n in NAT by ORDINAL1:def 12;

      then ( len q) = n by A1, FINSEQ_1:def 3;

      hence thesis by Def4;

    end;

    theorem :: MATRIX_1:10

    ( Permutations 1) = {( idseq 1)}

    proof

      

       A1: ( Permutations 1) c= {( idseq 1)}

      proof

        let p be object;

        assume p in ( Permutations 1);

        then

        reconsider q = p as Permutation of ( Seg 1) by Def5;

        

         A2: ( dom q) = ( Seg 1) by FUNCT_2: 52;

        ( rng q) = ( Seg 1) & 1 in {1} by FUNCT_2:def 3, TARSKI:def 1;

        then (q . 1) in ( Seg 1) by FINSEQ_1: 2, FUNCT_2: 4;

        then

         A3: (q . 1) = 1 by FINSEQ_1: 2, TARSKI:def 1;

        reconsider q as FinSequence by A2, FINSEQ_1:def 2;

        ( len q) = 1 by A2, FINSEQ_1:def 3;

        then q = ( idseq 1) by A3, FINSEQ_1: 40, FINSEQ_2: 50;

        hence thesis by TARSKI:def 1;

      end;

       {( idseq 1)} c= ( Permutations 1)

      proof

        let x be object;

        assume x in {( idseq 1)};

        then x = ( idseq 1) by TARSKI:def 1;

        hence thesis by Def5;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    begin

    reserve p,q for Element of ( Permutations n);

    definition

      let n;

      :: MATRIX_1:def13

      func Group_of_Perm (n) -> strict multMagma means

      : Def6: the carrier of it = ( Permutations n) & for q,p be Element of ( Permutations n) holds (the multF of it . (q,p)) = (p * q);

      existence

      proof

        defpred P[ Element of ( Permutations n), Element of ( Permutations n), set] means $3 = ($2 * $1);

        

         A1: for q,p be Element of ( Permutations n) holds ex z be Element of ( Permutations n) st P[q, p, z]

        proof

          let q,p be Element of ( Permutations n);

          reconsider p, q as Permutation of ( Seg n) by Def5;

          reconsider z = (p * q) as Element of ( Permutations n) by Def5;

          take z;

          thus thesis;

        end;

        consider o be BinOp of ( Permutations n) such that

         A2: for q,p be Element of ( Permutations n) holds P[q, p, (o . (q,p))] from BINOP_1:sch 3( A1);

        take multMagma (# ( Permutations n), o #);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let G1,G2 be strict multMagma;

        assume that

         A3: the carrier of G1 = ( Permutations n) and

         A4: for q,p be Element of ( Permutations n) holds (the multF of G1 . (q,p)) = (p * q) and

         A5: the carrier of G2 = ( Permutations n) and

         A6: for q,p be Element of ( Permutations n) holds (the multF of G2 . (q,p)) = (p * q);

        now

          let q,p be Element of G1;

          reconsider q9 = q, p9 = p as Element of ( Permutations n) by A3;

          

          thus (the multF of G1 . (q,p)) = (p9 * q9) by A4

          .= (the multF of G2 . (q,p)) by A6;

        end;

        hence thesis by A3, A5, BINOP_1: 2;

      end;

    end

    registration

      let n;

      cluster ( Group_of_Perm n) -> non empty;

      coherence

      proof

        the carrier of ( Group_of_Perm n) = ( Permutations n) by Def6;

        hence the carrier of ( Group_of_Perm n) is non empty;

      end;

    end

    theorem :: MATRIX_1:11

    

     Th5: ( idseq n) is Element of ( Group_of_Perm n)

    proof

      the carrier of ( Group_of_Perm n) = ( Permutations n) by Def6;

      hence thesis by Def5;

    end;

    theorem :: MATRIX_1:12

    

     Th6: (p * ( idseq n)) = p & (( idseq n) * p) = p

    proof

      

       A1: ( Seg n) = {} implies ( Seg n) = {} ;

      p is Permutation of ( Seg n) by Def5;

      then

       A2: ( rng p) = ( Seg n) by FUNCT_2:def 3;

      p is Function of ( Seg n), ( Seg n) by Def5;

      then ( dom p) = ( Seg n) by A1, FUNCT_2:def 1;

      hence thesis by A2, RELAT_1: 52, RELAT_1: 54;

    end;

    theorem :: MATRIX_1:13

    

     Th7: (p * (p " )) = ( idseq n) & ((p " ) * p) = ( idseq n)

    proof

      p is Permutation of ( Seg n) by Def5;

      hence thesis by FUNCT_2: 61;

    end;

    theorem :: MATRIX_1:14

    

     Th8: (p " ) is Element of ( Group_of_Perm n)

    proof

      reconsider p as Permutation of ( Seg n) by Def5;

      (p " ) is Element of ( Permutations n) by Def5;

      hence thesis by Def6;

    end;

    registration

      let n;

      cluster ( Group_of_Perm n) -> associative Group-like;

      coherence

      proof

        

         A1: ex e be Element of ( Group_of_Perm n) st for p be Element of ( Group_of_Perm n) holds (p * e) = p & (e * p) = p & ex g be Element of ( Group_of_Perm n) st (p * g) = e & (g * p) = e

        proof

          reconsider e = ( idseq n) as Element of ( Group_of_Perm n) by Th5;

          take e;

          reconsider e9 = ( idseq n) as Element of ( Permutations n) by Def5;

          

           A2: for p be Element of ( Group_of_Perm n) holds ex g be Element of ( Group_of_Perm n) st (p * g) = e & (g * p) = e

          proof

            let p be Element of ( Group_of_Perm n);

            reconsider q = p as Element of ( Permutations n) by Def6;

            reconsider r = q as Permutation of ( Seg n) by Def5;

            reconsider f = (r " ) as Element of ( Permutations n) by Def5;

            reconsider g = f as Element of ( Group_of_Perm n) by Th8;

            take g;

            

             A3: (g * p) = (q * f) by Def6

            .= e by Th7;

            (p * g) = (f * q) by Def6

            .= e by Th7;

            hence thesis by A3;

          end;

          for p be Element of ( Group_of_Perm n) holds (p * e) = p & (e * p) = p

          proof

            let p be Element of ( Group_of_Perm n);

            reconsider p9 = p as Element of ( Permutations n) by Def6;

            

             A4: (e * p) = (p9 * e9) by Def6

            .= p by Th6;

            (p * e) = (e9 * p9) by Def6

            .= p by Th6;

            hence thesis by A4;

          end;

          hence thesis by A2;

        end;

        for p,q,r be Element of ( Group_of_Perm n) holds ((p * q) * r) = (p * (q * r))

        proof

          let p,q,r be Element of ( Group_of_Perm n);

          reconsider p9 = p, q9 = q, r9 = r as Element of ( Permutations n) by Def6;

          

           A5: (q9 * p9) is Permutation of ( Seg n) & (r9 * q9) is Permutation of ( Seg n)

          proof

            reconsider p9, q9, r9 as Permutation of ( Seg n) by Def5;

            (q9 * p9) is Permutation of ( Seg n) & (r9 * q9) is Permutation of ( Seg n);

            hence thesis;

          end;

          then

           A6: (q9 * p9) is Element of ( Permutations n) by Def5;

          

           A7: (r9 * q9) is Element of ( Permutations n) by A5, Def5;

          ((p * q) * r) = (the multF of ( Group_of_Perm n) . ((q9 * p9),r9)) by Def6

          .= (r9 * (q9 * p9)) by A6, Def6

          .= ((r9 * q9) * p9) by RELAT_1: 36

          .= (the multF of ( Group_of_Perm n) . (p9,(r9 * q9))) by A7, Def6

          .= (p * (q * r)) by Def6;

          hence thesis;

        end;

        hence thesis by A1, GROUP_1: 1;

      end;

    end

    theorem :: MATRIX_1:15

    

     Th9: ( idseq n) = ( 1_ ( Group_of_Perm n))

    proof

      reconsider e = ( idseq n) as Element of ( Group_of_Perm n) by Th5;

      reconsider e9 = ( idseq n) as Element of ( Permutations n) by Def5;

      for p be Element of ( Group_of_Perm n) holds (p * e) = p & (e * p) = p

      proof

        let p be Element of ( Group_of_Perm n);

        reconsider p9 = p as Element of ( Permutations n) by Def6;

        

         A1: (e * p) = (p9 * e9) by Def6

        .= p by Th6;

        (p * e) = (e9 * p9) by Def6

        .= p by Th6;

        hence thesis by A1;

      end;

      hence thesis by GROUP_1: 4;

    end;

    definition

      let n;

      let p be Permutation of ( Seg n);

      :: MATRIX_1:def14

      attr p is being_transposition means ex i, j st i in ( dom p) & j in ( dom p) & i <> j & (p . i) = j & (p . j) = i & for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k;

    end

    definition

      let n;

      let IT be Permutation of ( Seg n);

      :: MATRIX_1:def15

      attr IT is even means ex l be FinSequence of ( Group_of_Perm n) st (( len l) mod 2) = 0 & IT = ( Product l) & for i st i in ( dom l) holds ex q st (l . i) = q & q is being_transposition;

    end

    notation

      let n;

      let IT be Permutation of ( Seg n);

      antonym IT is odd for IT is even;

    end

    theorem :: MATRIX_1:16

    ( id ( Seg n)) is even

    proof

      set l = ( <*> the carrier of ( Group_of_Perm n));

       0 = ((2 * 0 ) + 0 );

      then

       A1: (( len l) mod 2) = 0 by NAT_D:def 2;

      ( Product ( <*> the carrier of ( Group_of_Perm n))) = ( 1_ ( Group_of_Perm n)) by GROUP_4: 8;

      then

       A2: ( idseq n) = ( Product l) by Th9;

      for i st i in ( dom l) holds ex q st (l . i) = q & q is being_transposition;

      hence thesis by A1, A2;

    end;

    definition

      let K be Ring;

      let n be Nat;

      let x be Element of K;

      let p be Element of ( Permutations n);

      :: MATRIX_1:def16

      func - (x,p) -> Element of K equals x if p is even

      otherwise ( - x);

      correctness ;

    end

    registration

      let n;

      cluster ( Permutations n) -> finite;

      coherence

      proof

        

         A1: ( Permutations n) c= ( Funcs (( Seg n),( Seg n)))

        proof

          let x be object;

          assume x in ( Permutations n);

          then x is Function of ( Seg n), ( Seg n) by Def5;

          hence thesis by FUNCT_2: 9;

        end;

        ( Funcs (( Seg n),( Seg n))) is finite by FRAENKEL: 6;

        hence thesis by A1, FINSET_1: 1;

      end;

    end