matrix17.miz



    begin

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

K for Field,

a,b,c for Element of K,

p,q for FinSequence of K,

M1,M2,M3 for Matrix of n, K;

    

     Lm1: for n,i be Nat st i in ( Seg n) holds ((n + 1) - i) in ( Seg n)

    proof

      let n,i be Nat;

      assume

       A1: i in ( Seg n);

      i <= n by A1, FINSEQ_1: 1;

      then (i + 1) <= (n + 1) by XREAL_1: 6;

      then

       A2: ((i + 1) - i) <= ((n + 1) - i) by XREAL_1: 9;

      1 <= i by A1, FINSEQ_1: 1;

      then (n + 1) <= (i + n) by XREAL_1: 6;

      then

       A3: ((n + 1) - i) <= ((i + n) - i) by XREAL_1: 9;

      ((n + 1) - i) in NAT by A2, INT_1: 3;

      hence thesis by A2, A3;

    end;

    

     Lm2: for n,i,j be Nat st [i, j] in [:( Seg n), ( Seg n):] holds ((n + 1) - j) in ( Seg n) & ((n + 1) - i) in ( Seg n)

    proof

      let n,i,j be Nat;

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

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

      hence thesis by Lm1;

    end;

    definition

      let K be Field, n be Nat, M be Matrix of n, K;

      :: MATRIX17:def1

      attr M is subsymmetric means

      : Def1: for i,j,k,l be Nat st [i, j] in ( Indices M) & k = ((n + 1) - j) & l = ((n + 1) - i) holds (M * (i,j)) = (M * (k,l));

    end

    registration

      let n, K, a;

      cluster ((n,n) --> a) -> subsymmetric;

      coherence

      proof

        let M be Matrix of n, K such that

         A1: M = ((n,n) --> a);

        let i,j,k,l be Nat;

        assume that

         A2: [i, j] in ( Indices M) and

         A3: k = ((n + 1) - j) & l = ((n + 1) - i);

        

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

        k in ( Seg n) & l in ( Seg n) by A3, A2, A4, Lm2;

        then [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        then (M * (k,l)) = a by A1, A4, MATRIX_0: 46;

        hence thesis by A1, A2, MATRIX_0: 46;

      end;

    end

    registration

      let n, K;

      cluster subsymmetric for Matrix of n, K;

      existence

      proof

        take ((n,n) --> ( 0. K));

        thus thesis;

      end;

    end

    registration

      let n, K;

      let M be subsymmetric Matrix of n, K;

      cluster ( - M) -> subsymmetric;

      coherence

      proof

        let N be Matrix of n, K such that

         A1: N = ( - M);

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices N) and

         A4: k = ((n + 1) - j) & l = ((n + 1) - i);

        

         A5: ( Indices ( - M)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then i in ( Seg n) & j in ( Seg n) by A1, A3, ZFMISC_1: 87;

        then k in ( Seg n) & l in ( Seg n) by A4, Lm1;

        then

         A6: [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        (( - M) * (i,j)) = ( - (M * (i,j))) by A1, A2, A3, A5, MATRIX_3:def 2

        .= ( - (M * (k,l))) by A1, A2, A3, A5, A4, Def1

        .= (( - M) * (k,l)) by A2, A6, MATRIX_3:def 2;

        hence thesis by A1;

      end;

    end

    registration

      let n, K;

      let M1,M2 be subsymmetric Matrix of n, K;

      cluster (M1 + M2) -> subsymmetric;

      coherence

      proof

        let M be Matrix of n, K such that

         A1: M = (M1 + M2);

        let i,j,k,l be Nat;

        assume that

         A2: [i, j] in ( Indices M) and

         A3: k = ((n + 1) - j) & l = ((n + 1) - i);

        

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

        ((n + 1) - j) in ( Seg n) & ((n + 1) - i) in ( Seg n) by A2, A4, Lm2;

        then

         A5: [k, l] in [:( Seg n), ( Seg n):] by A3, ZFMISC_1: 87;

        

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

        ((M1 + M2) * (i,j)) = ((M1 * (i,j)) + (M2 * (i,j))) by A2, A4, A6, MATRIX_3:def 3

        .= ((M1 * (k,l)) + (M2 * (i,j))) by A2, A4, A6, A3, Def1

        .= ((M1 * (k,l)) + (M2 * (k,l))) by A2, A4, A6, A3, Def1

        .= ((M1 + M2) * (k,l)) by A6, A5, MATRIX_3:def 3;

        hence thesis by A1;

      end;

    end

    registration

      let n, K, a;

      let M be subsymmetric Matrix of n, K;

      cluster (a * M) -> subsymmetric;

      coherence

      proof

        let M1 be Matrix of n, K such that

         A1: M1 = (a * M);

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices M1) and

         A4: k = ((n + 1) - j) & l = ((n + 1) - i);

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

        then k in ( Seg n) & l in ( Seg n) by A3, A4, Lm2;

        then

         A5: [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        

         A6: [i, j] in ( Indices M) by A2, A3, MATRIX_0: 24;

        

        then ((a * M) * (i,j)) = (a * (M * (i,j))) by MATRIX_3:def 5

        .= (a * (M * (k,l))) by A4, A6, Def1

        .= ((a * M) * (k,l)) by A2, A5, MATRIX_3:def 5;

        hence thesis by A1;

      end;

    end

    registration

      let n, K;

      let M1,M2 be subsymmetric Matrix of n, K;

      cluster (M1 - M2) -> subsymmetric;

      coherence ;

    end

    registration

      let n, K;

      let M be subsymmetric Matrix of n, K;

      cluster (M @ ) -> subsymmetric;

      coherence

      proof

        let M1 be Matrix of n, K such that

         A1: M1 = (M @ );

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices M1) and

         A4: k = ((n + 1) - j) & l = ((n + 1) - i);

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

        then

         A5: i in ( Seg n) & j in ( Seg n) by ZFMISC_1: 87;

        then

         A6: [j, i] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        ((n + 1) - j) in ( Seg n) & ((n + 1) - i) in ( Seg n) by A5, Lm1;

        then

         A7: [((n + 1) - i), ((n + 1) - j)] in [:( Seg n), ( Seg n):] & [((n + 1) - j), ((n + 1) - i)] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        

        thus (M1 * (i,j)) = (M * (j,i)) by A1, A2, A6, MATRIX_0:def 6

        .= (M * (l,k)) by A4, A6, A2, Def1

        .= (M1 * (k,l)) by A1, A7, A2, A4, MATRIX_0:def 6;

      end;

    end

    registration

      let n, K;

      cluster line_circulant -> subsymmetric for Matrix of n, K;

      coherence

      proof

        let M be Matrix of n, K;

        assume M is line_circulant;

        then

        consider p be FinSequence of K such that ( len p) = ( width M) and

         A1: M is_line_circulant_about p by MATRIX16:def 2;

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices M) and

         A4: k = ((n + 1) - j) & l = ((n + 1) - i);

        k in ( Seg n) & l in ( Seg n) by A3, A2, A4, Lm2;

        then

         A5: [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        (M * (k,l)) = (p . (((((n + 1) - i) - ((n + 1) - j)) mod ( len p)) + 1)) by A1, A2, A4, A5, MATRIX16:def 1

        .= (p . (((j - i) mod ( len p)) + 1));

        hence thesis by A3, A1, MATRIX16:def 1;

      end;

      cluster col_circulant -> subsymmetric for Matrix of n, K;

      coherence

      proof

        let M be Matrix of n, K;

        assume M is col_circulant;

        then

        consider p be FinSequence of K such that

         A6: ( len p) = ( len M) and

         A7: M is_col_circulant_about p by MATRIX16:def 5;

        

         A8: ( len M) = n by MATRIX_0: 24;

        

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

        let i,j,k,l be Nat;

        assume that

         A10: [i, j] in ( Indices M) and

         A11: k = ((n + 1) - j) & l = ((n + 1) - i);

        k in ( Seg n) & l in ( Seg n) by A10, A9, A11, Lm2;

        then

         A12: [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        (M * (k,l)) = (p . (((((n + 1) - j) - ((n + 1) - i)) mod n) + 1)) by A6, A7, A8, A9, A11, A12, MATRIX16:def 4

        .= (p . (((i - j) mod n) + 1));

        hence thesis by A6, A7, A8, A10, MATRIX16:def 4;

      end;

    end

    definition

      let K be Field, n be Nat, M be Matrix of n, K;

      :: MATRIX17:def2

      attr M is Anti-subsymmetric means

      : Def2: for i,j,k,l be Nat st [i, j] in ( Indices M) & k = ((n + 1) - j) & l = ((n + 1) - i) holds (M * (i,j)) = ( - (M * (k,l)));

    end

    registration

      let n, K;

      cluster Anti-subsymmetric for Matrix of n, K;

      existence

      proof

        take M = ((n,n) --> ( 0. K));

        let i,j,k,l be Nat;

        assume that

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

         A2: k = ((n + 1) - j) & l = ((n + 1) - i);

        

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

        k in ( Seg n) & l in ( Seg n) by A2, A1, A3, Lm2;

        then [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        then

         A4: (M * (k,l)) = ( 0. K) by A3, MATRIX_0: 46;

        ( 0. K) = ( - ( 0. K)) by RLVECT_1: 12;

        hence thesis by A4, A1, MATRIX_0: 46;

      end;

    end

    theorem :: MATRIX17:1

    for K be Fanoian Field, n,i,j,k,l be Nat, M1 be Matrix of n, K st [i, j] in ( Indices M1) & (i + j) = (n + 1) & k = ((n + 1) - j) & l = ((n + 1) - i) & M1 is Anti-subsymmetric holds (M1 * (i,j)) = ( 0. K)

    proof

      let K be Fanoian Field;

      let n,i,j,k,l be Nat;

      let M1 be Matrix of n, K;

      assume that

       A1: [i, j] in ( Indices M1) and

       A2: (i + j) = (n + 1) & k = ((n + 1) - j) & l = ((n + 1) - i) and

       A3: M1 is Anti-subsymmetric;

      (M1 * (i,j)) = ( - (M1 * (i,j))) by A1, A3, A2;

      then ((M1 * (i,j)) + (M1 * (i,j))) = ( 0. K) by RLVECT_1: 5;

      then ((( 1_ K) * (M1 * (i,j))) + (M1 * (i,j))) = ( 0. K);

      then ((( 1_ K) * (M1 * (i,j))) + (( 1_ K) * (M1 * (i,j)))) = ( 0. K);

      then (( 1_ K) + ( 1_ K)) <> ( 0. K) & ((( 1_ K) + ( 1_ K)) * (M1 * (i,j))) = ( 0. K) by VECTSP_1:def 7, VECTSP_1:def 19;

      hence thesis by VECTSP_1: 12;

    end;

    registration

      let n, K;

      let M be Anti-subsymmetric Matrix of n, K;

      cluster ( - M) -> Anti-subsymmetric;

      coherence

      proof

        let N be Matrix of n, K such that

         A1: N = ( - M);

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices N) and

         A4: k = ((n + 1) - j) & l = ((n + 1) - i);

        

         A5: ( Indices ( - M)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then i in ( Seg n) & j in ( Seg n) by A1, A3, ZFMISC_1: 87;

        then k in ( Seg n) & l in ( Seg n) by A4, Lm1;

        then

         A6: [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        (( - M) * (i,j)) = ( - (M * (i,j))) by A1, A2, A3, A5, MATRIX_3:def 2

        .= ( - ( - (M * (k,l)))) by A1, A2, A3, A5, A4, Def2

        .= ( - (( - M) * (k,l))) by A2, A6, MATRIX_3:def 2;

        hence thesis by A1;

      end;

    end

    registration

      let n, K;

      let M1,M2 be Anti-subsymmetric Matrix of n, K;

      cluster (M1 + M2) -> Anti-subsymmetric;

      coherence

      proof

        let M be Matrix of n, K such that

         A1: M = (M1 + M2);

        let i,j,k,l be Nat;

        assume that

         A2: [i, j] in ( Indices M) and

         A3: k = ((n + 1) - j) & l = ((n + 1) - i);

        

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

        ((n + 1) - j) in ( Seg n) & ((n + 1) - i) in ( Seg n) by A2, A4, Lm2;

        then

         A5: [k, l] in [:( Seg n), ( Seg n):] by A3, ZFMISC_1: 87;

        

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

        ((M1 + M2) * (i,j)) = ((M1 * (i,j)) + (M2 * (i,j))) by A2, A4, A6, MATRIX_3:def 3

        .= (( - (M1 * (k,l))) + (M2 * (i,j))) by A2, A4, A6, A3, Def2

        .= (( - (M1 * (k,l))) + ( - (M2 * (k,l)))) by A2, A4, A6, A3, Def2

        .= ( - ((M1 * (k,l)) + (M2 * (k,l)))) by RLVECT_1: 31

        .= ( - ((M1 + M2) * (k,l))) by A6, A5, MATRIX_3:def 3;

        hence thesis by A1;

      end;

    end

    registration

      let n, K, a;

      let M be Anti-subsymmetric Matrix of n, K;

      cluster (a * M) -> Anti-subsymmetric;

      coherence

      proof

        let M1 be Matrix of n, K such that

         A1: M1 = (a * M);

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices M1) and

         A4: k = ((n + 1) - j) & l = ((n + 1) - i);

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

        then k in ( Seg n) & l in ( Seg n) by A3, A4, Lm2;

        then

         A5: [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        

         A6: [i, j] in ( Indices M) by A2, A3, MATRIX_0: 24;

        

        then ((a * M) * (i,j)) = (a * (M * (i,j))) by MATRIX_3:def 5

        .= (a * ( - (M * (k,l)))) by A4, A6, Def2

        .= ( - (a * (M * (k,l)))) by VECTSP_1: 8

        .= ( - ((a * M) * (k,l))) by A2, A5, MATRIX_3:def 5;

        hence thesis by A1;

      end;

    end

    registration

      let n, K;

      let M1,M2 be Anti-subsymmetric Matrix of n, K;

      cluster (M1 - M2) -> Anti-subsymmetric;

      coherence ;

    end

    registration

      let n, K;

      let M be Anti-subsymmetric Matrix of n, K;

      cluster (M @ ) -> Anti-subsymmetric;

      coherence

      proof

        let M1 be Matrix of n, K such that

         A1: M1 = (M @ );

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices M1) and

         A4: k = ((n + 1) - j) & l = ((n + 1) - i);

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

        then

         A5: i in ( Seg n) & j in ( Seg n) by ZFMISC_1: 87;

        then

         A6: [j, i] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        ((n + 1) - j) in ( Seg n) & ((n + 1) - i) in ( Seg n) by A5, Lm1;

        then

         A7: [((n + 1) - i), ((n + 1) - j)] in [:( Seg n), ( Seg n):] & [((n + 1) - j), ((n + 1) - i)] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        

        thus (M1 * (i,j)) = (M * (j,i)) by A1, A2, A6, MATRIX_0:def 6

        .= ( - (M * (l,k))) by A4, A6, A2, Def2

        .= ( - (M1 * (k,l))) by A1, A7, A2, A4, MATRIX_0:def 6;

      end;

    end

    begin

    definition

      let K be Field;

      let n be Nat;

      let M be Matrix of n, K;

      :: MATRIX17:def3

      attr M is central_symmetric means

      : Def3: for i,j,k,l be Nat st [i, j] in ( Indices M) & k = ((n + 1) - i) & l = ((n + 1) - j) holds (M * (i,j)) = (M * (k,l));

    end

    registration

      let n, K, a;

      cluster ((n,n) --> a) -> central_symmetric;

      coherence

      proof

        let M be Matrix of n, K such that

         A1: M = ((n,n) --> a);

        let i,j,k,l be Nat;

        assume that

         A2: [i, j] in ( Indices M) and

         A3: k = ((n + 1) - i) & l = ((n + 1) - j);

        

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

        k in ( Seg n) & l in ( Seg n) by A3, A2, A4, Lm2;

        then [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        then (M * (k,l)) = a by A1, A4, MATRIX_0: 46;

        hence thesis by A1, A2, MATRIX_0: 46;

      end;

    end

    registration

      let n, K;

      cluster central_symmetric for Matrix of n, K;

      existence

      proof

        take ((n,n) --> ( 0. K));

        thus thesis;

      end;

    end

    registration

      let n, K;

      let M be central_symmetric Matrix of n, K;

      cluster ( - M) -> central_symmetric;

      coherence

      proof

        let N be Matrix of n, K such that

         A1: N = ( - M);

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices N) and

         A4: k = ((n + 1) - i) & l = ((n + 1) - j);

        

         A5: ( Indices ( - M)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then i in ( Seg n) & j in ( Seg n) by A1, A3, ZFMISC_1: 87;

        then k in ( Seg n) & l in ( Seg n) by A4, Lm1;

        then

         A6: [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        (( - M) * (i,j)) = ( - (M * (i,j))) by A1, A2, A3, A5, MATRIX_3:def 2

        .= ( - (M * (k,l))) by A1, A2, A3, A5, A4, Def3

        .= (( - M) * (k,l)) by A2, A6, MATRIX_3:def 2;

        hence thesis by A1;

      end;

    end

    registration

      let n, K;

      let M1,M2 be central_symmetric Matrix of n, K;

      cluster (M1 + M2) -> central_symmetric;

      coherence

      proof

        let M be Matrix of n, K such that

         A1: M = (M1 + M2);

        let i,j,k,l be Nat;

        assume that

         A2: [i, j] in ( Indices M) and

         A3: k = ((n + 1) - i) & l = ((n + 1) - j);

        

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

        ((n + 1) - j) in ( Seg n) & ((n + 1) - i) in ( Seg n) by A2, A4, Lm2;

        then

         A5: [k, l] in [:( Seg n), ( Seg n):] by A3, ZFMISC_1: 87;

        

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

        ((M1 + M2) * (i,j)) = ((M1 * (i,j)) + (M2 * (i,j))) by A2, A4, A6, MATRIX_3:def 3

        .= ((M1 * (k,l)) + (M2 * (i,j))) by A2, A4, A6, A3, Def3

        .= ((M1 * (k,l)) + (M2 * (k,l))) by A2, A4, A6, A3, Def3

        .= ((M1 + M2) * (k,l)) by A6, A5, MATRIX_3:def 3;

        hence thesis by A1;

      end;

    end

    registration

      let n, K, a;

      let M be central_symmetric Matrix of n, K;

      cluster (a * M) -> central_symmetric;

      coherence

      proof

        let M1 be Matrix of n, K such that

         A1: M1 = (a * M);

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices M1) and

         A4: k = ((n + 1) - i) & l = ((n + 1) - j);

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

        then k in ( Seg n) & l in ( Seg n) by A3, A4, Lm2;

        then

         A5: [k, l] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        

         A6: [i, j] in ( Indices M) by A2, A3, MATRIX_0: 24;

        

        then ((a * M) * (i,j)) = (a * (M * (i,j))) by MATRIX_3:def 5

        .= (a * (M * (k,l))) by A4, A6, Def3

        .= ((a * M) * (k,l)) by A2, A5, MATRIX_3:def 5;

        hence thesis by A1;

      end;

    end

    registration

      let n, K;

      let M1,M2 be central_symmetric Matrix of n, K;

      cluster (M1 - M2) -> central_symmetric;

      coherence ;

    end

    registration

      let n, K;

      let M be central_symmetric Matrix of n, K;

      cluster (M @ ) -> central_symmetric;

      coherence

      proof

        let M1 be Matrix of n, K such that

         A1: M1 = (M @ );

        

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

        let i,j,k,l be Nat;

        assume that

         A3: [i, j] in ( Indices M1) and

         A4: k = ((n + 1) - i) & l = ((n + 1) - j);

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

        then

         A5: i in ( Seg n) & j in ( Seg n) by ZFMISC_1: 87;

        then

         A6: [j, i] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        ((n + 1) - j) in ( Seg n) & ((n + 1) - i) in ( Seg n) by A5, Lm1;

        then

         A7: [((n + 1) - i), ((n + 1) - j)] in [:( Seg n), ( Seg n):] & [((n + 1) - j), ((n + 1) - i)] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        

        thus (M1 * (i,j)) = (M * (j,i)) by A1, A2, A6, MATRIX_0:def 6

        .= (M * (l,k)) by A4, A6, A2, Def3

        .= (M1 * (k,l)) by A1, A7, A2, A4, MATRIX_0:def 6;

      end;

    end

    registration

      let n, K;

      cluster symmetric subsymmetric -> central_symmetric for Matrix of n, K;

      coherence

      proof

        let M1 be Matrix of n, K;

        assume that

         A1: M1 is symmetric and

         A2: M1 is subsymmetric;

        

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

        let i,j,k,l be Nat;

        assume that

         A4: [i, j] in ( Indices M1) and

         A5: k = ((n + 1) - i) & l = ((n + 1) - j);

        k in ( Seg n) & l in ( Seg n) by A3, A4, A5, Lm2;

        then

         A6: [k, l] in [:( Seg n), ( Seg n):] & [l, k] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        

        thus (M1 * (i,j)) = (M1 * (l,k)) by A2, A4, A5

        .= ((M1 @ ) * (k,l)) by A6, A3, MATRIX_0:def 6

        .= (M1 * (k,l)) by A1;

      end;

    end

    begin

    

     Lm3: for n,i,j be Nat st i in ( Seg n) & j in ( Seg n) & (i + j) <> (n + 1) holds (((i + j) - 1) mod n) in ( Seg n)

    proof

      let n,i,j be Nat such that

       A1: i in ( Seg n) & j in ( Seg n);

      assume (i + j) <> (n + 1);

      per cases by XXREAL_0: 1;

        suppose

         A2: (i + j) < (n + 1);

        1 <= i & 1 <= j by A1, FINSEQ_1: 1;

        then (1 + 1) <= (i + j) by XREAL_1: 7;

        then

         A3: ((1 + 1) - 1) <= ((i + j) - 1) by XREAL_1: 9;

        

         A4: ((i + j) - 1) < ((n + 1) - 1) by A2, XREAL_1: 9;

        

         A5: (((i + j) - 1) mod n) = ((i + j) - 1) by A3, A4, NAT_D: 63;

        (((i + j) - 1) mod n) in NAT by A3, A5, INT_1: 3;

        hence thesis by A3, A5, A4;

      end;

        suppose

         A6: (i + j) > (n + 1);

        ((i + j) - n) > ((n + 1) - n) by A6, XREAL_1: 9;

        then

         A7: (((i + j) - n) - 1) > (1 - 1) by XREAL_1: 9;

        

         A8: (((i + j) - n) - 1) >= ( 0 + 1) by A7, INT_1: 7;

        i <= n & j <= n by A1, FINSEQ_1: 1;

        then (i + j) <= (n + n) by XREAL_1: 7;

        then ((i + j) - n) <= ((n + n) - n) by XREAL_1: 9;

        then

         A9: (((i + j) - n) - 1) <= (n - 1) by XREAL_1: 9;

        (n - 1) < n by XREAL_1: 44;

        then

         A10: (((i + j) - n) - 1) < n by A9, XXREAL_0: 2;

        

         A11: ((((i + j) - n) - 1) mod n) = (((i + j) - n) - 1) by A7, A10, NAT_D: 63;

        

         A12: ((((i + j) - n) - 1) mod n) in NAT by A7, A11, INT_1: 3;

        (((i + j) - 1) mod n) = (((((i + j) - 1) - n) + n) mod n)

        .= ((((((i + j) - 1) - n) mod n) + (n mod n)) mod n) by NAT_D: 66

        .= (((((i + j) - 1) - n) + 0 ) mod n) by A11, INT_1: 50;

        hence thesis by A10, A11, A8, A12;

      end;

    end;

    

     Lm4: for n,i,j be Nat st [i, j] in [:( Seg n), ( Seg n):] & (i + j) <> (n + 1) holds (((i + j) - 1) mod n) in ( Seg n)

    proof

      let n,i,j be Nat;

      assume that

       A1: [i, j] in [:( Seg n), ( Seg n):] and

       A2: (i + j) <> (n + 1);

      i in ( Seg n) & j in ( Seg n) by A1, ZFMISC_1: 87;

      hence thesis by A2, Lm3;

    end;

    definition

      let K be set, M be Matrix of K, p be FinSequence;

      :: MATRIX17:def4

      pred M is_symmetry_circulant_about p means ( len p) = ( width M) & (for i,j be Nat st [i, j] in ( Indices M) & (i + j) <> (( len p) + 1) holds (M * (i,j)) = (p . (((i + j) - 1) mod ( len p)))) & for i,j be Nat st [i, j] in ( Indices M) & (i + j) = (( len p) + 1) holds (M * (i,j)) = (p . ( len p));

    end

    theorem :: MATRIX17:2

    

     Th2: ((n,n) --> a) is_symmetry_circulant_about (n |-> a)

    proof

      set p = (n |-> a);

      set M = ((n,n) --> a);

      

       A1: ( width M) = n & ( len p) = n by CARD_1:def 7, MATRIX_0: 24;

      hence ( len p) = ( width M);

      

       A2: ( Indices ((n,n) --> a)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      thus for i,j be Nat st [i, j] in ( Indices M) & (i + j) <> (( len p) + 1) holds (M * (i,j)) = (p . (((i + j) - 1) mod ( len p)))

      proof

        let i,j be Nat;

        assume that

         A3: [i, j] in ( Indices M) and

         A4: (i + j) <> (( len p) + 1);

        ((( Seg n) --> a) . (((i + j) - 1) mod ( len p))) = a by A1, A2, A3, A4, Lm4, FUNCOP_1: 7;

        hence thesis by A3, MATRIX_0: 46;

      end;

      let i,j be Nat;

      assume that

       A5: [i, j] in ( Indices ((n,n) --> a)) and

       A6: (i + j) = (( len p) + 1);

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

      then 1 <= i & 1 <= j by FINSEQ_1: 1;

      then (1 + 1) <= (i + j) by XREAL_1: 7;

      then ((( len p) + 1) - 1) >= ((1 + 1) - 1) by A6, XREAL_1: 9;

      then

       A7: ( len p) in ( Seg ( len p));

      ((( Seg n) --> a) . ( len p)) = a by A1, A7, FUNCOP_1: 7;

      hence thesis by A5, MATRIX_0: 46;

    end;

    theorem :: MATRIX17:3

    

     Th3: M1 is_symmetry_circulant_about p implies (a * M1) is_symmetry_circulant_about (a * p)

    proof

      assume

       A1: M1 is_symmetry_circulant_about p;

      then

       A2: ( len p) = ( width M1);

      

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

      

       A4: ( width M1) = n by MATRIX_0: 24;

      then

       A5: ( dom p) = ( Seg n) by A2, FINSEQ_1:def 3;

      

       A6: ( dom (a * p)) = ( Seg ( len (a * p))) by FINSEQ_1:def 3;

      

       A7: ( len (a * p)) = ( len p) by MATRIXR1: 16;

      

       A8: for i,j be Nat st [i, j] in ( Indices (a * M1)) & (i + j) <> (( len (a * p)) + 1) holds ((a * M1) * (i,j)) = ((a * p) . (((i + j) - 1) mod ( len (a * p))))

      proof

        let i,j be Nat;

        assume that

         A9: [i, j] in ( Indices (a * M1)) and

         A10: (i + j) <> (( len (a * p)) + 1);

        

         A11: (((i + j) - 1) mod n) in ( Seg n) by A3, A2, A4, A9, A10, A7, Lm4;

        

         A12: [i, j] in ( Indices M1) by A3, A9, MATRIX_0: 24;

        

        then ((a * M1) * (i,j)) = (a * (M1 * (i,j))) by MATRIX_3:def 5

        .= ((a multfield ) . (M1 * (i,j))) by FVSUM_1: 49

        .= ((a multfield ) . (p . (((i + j) - 1) mod ( len p)))) by A1, A12, A10, A7

        .= ((a multfield ) . (p /. (((i + j) - 1) mod ( len p)))) by A2, A4, A5, A11, PARTFUN1:def 6

        .= (a * (p /. (((i + j) - 1) mod ( len p)))) by FVSUM_1: 49

        .= ((a * p) /. (((i + j) - 1) mod ( len p))) by A2, A4, A5, A11, POLYNOM1:def 1

        .= ((a * p) . (((i + j) - 1) mod ( len p))) by A2, A4, A6, A7, A11, PARTFUN1:def 6;

        hence thesis by MATRIXR1: 16;

      end;

      

       A13: for i,j be Nat st [i, j] in ( Indices (a * M1)) & (i + j) = (( len (a * p)) + 1) holds ((a * M1) * (i,j)) = ((a * p) . ( len (a * p)))

      proof

        let i,j be Nat;

        assume that

         A14: [i, j] in ( Indices (a * M1)) and

         A15: (i + j) = (( len (a * p)) + 1);

        i in ( Seg n) & j in ( Seg n) by A3, A14, ZFMISC_1: 87;

        then 1 <= i & 1 <= j by FINSEQ_1: 1;

        then (1 + 1) <= (i + j) by XREAL_1: 7;

        then

         A16: ((( len (a * p)) + 1) - 1) >= ((1 + 1) - 1) by A15, XREAL_1: 9;

        

         A17: ( len (a * p)) in ( Seg ( len (a * p))) by A16;

        then

         A18: ( len p) in ( dom (a * p)) by A7, FINSEQ_1:def 3;

        

         A19: ( len p) in ( dom p) by A7, A17, FINSEQ_1:def 3;

        

         A20: [i, j] in ( Indices M1) by A3, A14, MATRIX_0: 24;

        

        then ((a * M1) * (i,j)) = (a * (M1 * (i,j))) by MATRIX_3:def 5

        .= ((a multfield ) . (M1 * (i,j))) by FVSUM_1: 49

        .= ((a multfield ) . (p . ( len p))) by A1, A20, A15, A7

        .= ((a multfield ) . (p /. ( len p))) by A19, PARTFUN1:def 6

        .= (a * (p /. ( len p))) by FVSUM_1: 49

        .= ((a * p) /. ( len p)) by A19, POLYNOM1:def 1

        .= ((a * p) . ( len p)) by A18, PARTFUN1:def 6;

        hence thesis by MATRIXR1: 16;

      end;

      

       A21: ( width (a * M1)) = n & ( len (a * p)) = ( len p) by MATRIXR1: 16, MATRIX_0: 24;

      ( len p) = n by A2, MATRIX_0: 24;

      hence thesis by A21, A8, A13;

    end;

    theorem :: MATRIX17:4

    

     Th4: M1 is_symmetry_circulant_about p implies ( - M1) is_symmetry_circulant_about ( - p)

    proof

      assume

       A1: M1 is_symmetry_circulant_about p;

      then

       A2: ( len p) = ( width M1);

      

       A3: ( width M1) = n by MATRIX_0: 24;

      

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

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

      then

       A5: ( - p) is Element of (( len p) -tuples_on the carrier of K) by FINSEQ_2: 113;

      then

       A6: ( width ( - M1)) = n & ( len ( - p)) = ( len p) by CARD_1:def 7, MATRIX_0: 24;

      

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

      

       A8: for i,j be Nat st [i, j] in ( Indices ( - M1)) & (i + j) <> (( len p) + 1) holds (( - M1) * (i,j)) = (( - p) . (((i + j) - 1) mod ( len ( - p))))

      proof

        let i,j be Nat;

        assume that

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

         A10: (i + j) <> (( len p) + 1);

        (((i + j) - 1) mod n) in ( Seg n) by A3, A2, A4, A9, A10, Lm4;

        then

         A11: (((i + j) - 1) mod ( len p)) in ( dom p) by A2, A3, FINSEQ_1:def 3;

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A7, A4, A9, MATRIX_3:def 2

        .= (( comp K) . (M1 * (i,j))) by VECTSP_1:def 13

        .= (( comp K) . (p . (((i + j) - 1) mod ( len p)))) by A1, A7, A4, A9, A10

        .= (( - p) . (((i + j) - 1) mod ( len p))) by A11, FUNCT_1: 13;

        hence thesis by A5, CARD_1:def 7;

      end;

      for i,j be Nat st [i, j] in ( Indices ( - M1)) & (i + j) = (( len p) + 1) holds (( - M1) * (i,j)) = (( - p) . ( len ( - p)))

      proof

        let i,j be Nat;

        assume that

         A12: [i, j] in ( Indices ( - M1)) and

         A13: (i + j) = (( len p) + 1);

        i in ( Seg n) & j in ( Seg n) by A4, A12, ZFMISC_1: 87;

        then 1 <= i & 1 <= j by FINSEQ_1: 1;

        then (1 + 1) <= (i + j) by XREAL_1: 7;

        then ((( len p) + 1) - 1) >= ((1 + 1) - 1) by A13, XREAL_1: 9;

        then ( len p) in ( Seg ( len p));

        then

         A14: ( len p) in ( dom p) by FINSEQ_1:def 3;

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A7, A4, A12, MATRIX_3:def 2

        .= (( comp K) . (M1 * (i,j))) by VECTSP_1:def 13

        .= (( comp K) . (p . ( len p))) by A1, A7, A4, A12, A13

        .= (( - p) . ( len p)) by A14, FUNCT_1: 13;

        hence thesis by A5, CARD_1:def 7;

      end;

      hence thesis by A2, A3, A6, A8;

    end;

    theorem :: MATRIX17:5

    

     Th5: M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q implies (M1 + M2) is_symmetry_circulant_about (p + q)

    proof

      assume that

       A1: M1 is_symmetry_circulant_about p;

      

       A2: ( len p) = ( width M1) by A1;

      

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

      

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

      

       A5: ( width M1) = n by MATRIX_0: 24;

      then

       A6: ( dom p) = ( Seg n) by A2, FINSEQ_1:def 3;

      assume

       A7: M2 is_symmetry_circulant_about q;

      then

       A8: ( len q) = ( width M2);

      

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

      

       A10: n in NAT by ORDINAL1:def 12;

      

       A11: ( width M2) = n by MATRIX_0: 24;

      then ( dom q) = ( Seg n) by A8, FINSEQ_1:def 3;

      then

       A12: ( dom (p + q)) = ( dom p) by A6, POLYNOM1: 1;

      then

       A13: ( len (p + q)) = n by A6, A10, FINSEQ_1:def 3;

      

       A14: ( width (M1 + M2)) = n by MATRIX_0: 24;

      

       A15: ( dom (p + q)) = ( Seg ( len (p + q))) by FINSEQ_1:def 3;

      

       A16: for i,j be Nat st [i, j] in ( Indices (M1 + M2)) & (i + j) <> (( len (p + q)) + 1) holds ((M1 + M2) * (i,j)) = ((p + q) . (((i + j) - 1) mod ( len (p + q))))

      proof

        let i,j be Nat;

        assume that

         A17: [i, j] in ( Indices (M1 + M2)) and

         A18: (i + j) <> (( len (p + q)) + 1);

        

         A19: (((i + j) - 1) mod ( len (p + q))) in ( dom (p + q)) by A4, A15, A18, A17, A12, A6, Lm4;

        ((M1 + M2) * (i,j)) = ((M1 * (i,j)) + (M2 * (i,j))) by A9, A4, A17, MATRIX_3:def 3

        .= (the addF of K . ((M1 * (i,j)),(q . (((i + j) - 1) mod ( len (p + q)))))) by A7, A3, A4, A11, A17, A18, A13

        .= (the addF of K . ((p . (((i + j) - 1) mod ( len (p + q)))),(q . (((i + j) - 1) mod ( len (p + q)))))) by A1, A5, A9, A4, A13, A17, A18

        .= ((p + q) . (((i + j) - 1) mod ( len (p + q)))) by A19, FUNCOP_1: 22;

        hence thesis;

      end;

      for i,j be Nat st [i, j] in ( Indices (M1 + M2)) & (i + j) = (( len (p + q)) + 1) holds ((M1 + M2) * (i,j)) = ((p + q) . ( len (p + q)))

      proof

        let i,j be Nat;

        assume that

         A20: [i, j] in ( Indices (M1 + M2)) and

         A21: (i + j) = (( len (p + q)) + 1);

        i in ( Seg n) & j in ( Seg n) by A4, A20, ZFMISC_1: 87;

        then 1 <= i & 1 <= j by FINSEQ_1: 1;

        then (1 + 1) <= (i + j) by XREAL_1: 7;

        then ((( len (p + q)) + 1) - 1) >= ((1 + 1) - 1) by A21, XREAL_1: 9;

        then ( len (p + q)) in ( Seg ( len (p + q)));

        then

         A22: ( len (p + q)) in ( dom (p + q)) by FINSEQ_1:def 3;

        ((M1 + M2) * (i,j)) = ((M1 * (i,j)) + (M2 * (i,j))) by A9, A4, A20, MATRIX_3:def 3

        .= (the addF of K . ((M1 * (i,j)),(q . ( len (p + q))))) by A7, A11, A13, A3, A4, A20, A21

        .= (the addF of K . ((p . ( len (p + q))),(q . ( len (p + q))))) by A1, A9, A5, A4, A13, A20, A21

        .= ((p + q) . ( len (p + q))) by A22, FUNCOP_1: 22;

        hence thesis;

      end;

      hence thesis by A14, A13, A16;

    end;

    definition

      let K be set, M be Matrix of K;

      :: MATRIX17:def5

      attr M is symmetry_circulant means

      : Def5: ex p be FinSequence of K st ( len p) = ( width M) & M is_symmetry_circulant_about p;

    end

    definition

      let K be non empty set;

      let p be FinSequence of K;

      :: MATRIX17:def6

      attr p is first-symmetry-of-circulant means ex M be Matrix of ( len p), K st M is_symmetry_circulant_about p;

    end

    definition

      let K be non empty set, p be FinSequence of K;

      assume

       A1: p is first-symmetry-of-circulant;

      :: MATRIX17:def7

      func SCirc (p) -> Matrix of ( len p), K means

      : Def7: it is_symmetry_circulant_about p;

      existence by A1;

      uniqueness

      proof

        let M1,M2 be Matrix of ( len p), K;

        assume that

         A2: M1 is_symmetry_circulant_about p and

         A3: M2 is_symmetry_circulant_about p;

        

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

        for i,j be Nat st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j))

        proof

          let i,j be Nat;

          assume

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

          per cases ;

            suppose

             A6: (i + j) <> (( len p) + 1);

            then (M1 * (i,j)) = (p . (((i + j) - 1) mod ( len p))) by A5, A2;

            hence thesis by A3, A4, A5, A6;

          end;

            suppose

             A7: (i + j) = (( len p) + 1);

            then (M1 * (i,j)) = (p . ( len p)) by A2, A5;

            hence thesis by A3, A4, A5, A7;

          end;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    registration

      let n, K, a;

      cluster ((n,n) --> a) -> symmetry_circulant;

      coherence

      proof

        set p = (n |-> a);

        ((n,n) --> a) is_symmetry_circulant_about p by Th2;

        hence thesis;

      end;

    end

    registration

      let n, K;

      cluster symmetry_circulant for Matrix of n, K;

      existence

      proof

        take ((n,n) --> ( 0. K));

        thus thesis;

      end;

    end

    reserve D for non empty set,

t for FinSequence of D,

A for Matrix of n, D;

    theorem :: MATRIX17:6

    

     Th6: for p be FinSequence of D holds 0 < n & A is_symmetry_circulant_about p implies (A @ ) is_symmetry_circulant_about p

    proof

      let p be FinSequence of D;

      assume that

       A1: 0 < n and

       A2: A is_symmetry_circulant_about p;

      

       A3: ( len p) = ( width A) by A2;

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

      then

       A4: ( width (A @ )) = ( len p) by A1, A3, MATRIX_0: 54;

      

       A5: for i,j be Nat st [i, j] in ( Indices (A @ )) & (i + j) <> (( len p) + 1) holds ((A @ ) * (i,j)) = (p . (((i + j) - 1) mod ( len p)))

      proof

        let i,j be Nat;

        

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

        assume that

         A7: [i, j] in ( Indices (A @ )) and

         A8: (i + j) <> (( len p) + 1);

         [i, j] in ( Indices A) by A7, MATRIX_0: 26;

        then i in ( Seg n) & j in ( Seg n) by A6, ZFMISC_1: 87;

        then

         A9: [j, i] in ( Indices A) by A6, ZFMISC_1: 87;

        then ((A @ ) * (i,j)) = (A * (j,i)) by MATRIX_0:def 6;

        hence thesis by A2, A9, A8;

      end;

      for i,j be Nat st [i, j] in ( Indices (A @ )) & (i + j) = (( len p) + 1) holds ((A @ ) * (i,j)) = (p . ( len p))

      proof

        let i,j be Nat;

        

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

        assume that

         A11: [i, j] in ( Indices (A @ )) and

         A12: (i + j) = (( len p) + 1);

         [i, j] in ( Indices A) by A11, MATRIX_0: 26;

        then i in ( Seg n) & j in ( Seg n) by A10, ZFMISC_1: 87;

        then

         A13: [j, i] in ( Indices A) by A10, ZFMISC_1: 87;

        then ((A @ ) * (i,j)) = (A * (j,i)) by MATRIX_0:def 6;

        hence thesis by A2, A12, A13;

      end;

      hence thesis by A4, A5;

    end;

    registration

      let n, K, a;

      let M1 be symmetry_circulant Matrix of n, K;

      cluster (a * M1) -> symmetry_circulant;

      coherence

      proof

        consider p be FinSequence of K such that ( len p) = ( width M1) and

         A1: M1 is_symmetry_circulant_about p by Def5;

        (a * M1) is_symmetry_circulant_about (a * p) by A1, Th3;

        then ex q be FinSequence of K st ( len q) = ( width (a * M1)) & (a * M1) is_symmetry_circulant_about q;

        hence thesis;

      end;

    end

    registration

      let n, K;

      let M1,M2 be symmetry_circulant Matrix of n, K;

      cluster (M1 + M2) -> symmetry_circulant;

      coherence

      proof

        let M be Matrix of n, K such that

         A1: M = (M1 + M2);

        consider p be FinSequence of K such that

         A2: ( len p) = ( width M1) and

         A3: M1 is_symmetry_circulant_about p by Def5;

        ( width M1) = n by MATRIX_0: 24;

        then

         A4: ( dom p) = ( Seg n) by A2, FINSEQ_1:def 3;

        consider q be FinSequence of K such that

         A5: ( len q) = ( width M2) and

         A6: M2 is_symmetry_circulant_about q by Def5;

        

         A7: n in NAT by ORDINAL1:def 12;

        ( width M2) = n by MATRIX_0: 24;

        then ( dom q) = ( Seg n) by A5, FINSEQ_1:def 3;

        then ( dom (p + q)) = ( dom p) by A4, POLYNOM1: 1;

        then

         A8: ( len (p + q)) = n by A4, A7, FINSEQ_1:def 3;

        ( width (M1 + M2)) = n by MATRIX_0: 24;

        then ex r be FinSequence of K st ( len r) = ( width (M1 + M2)) & (M1 + M2) is_symmetry_circulant_about r by A8, A3, A6, Th5;

        hence thesis by A1;

      end;

    end

    registration

      let n, K;

      let M1 be symmetry_circulant Matrix of n, K;

      cluster ( - M1) -> symmetry_circulant;

      coherence

      proof

        let N be Matrix of n, K such that

         A1: N = ( - M1);

        consider p be FinSequence of K such that ( len p) = ( width M1) and

         A2: M1 is_symmetry_circulant_about p by Def5;

        ( - M1) is_symmetry_circulant_about ( - p) by A2, Th4;

        then ex r be FinSequence of K st ( len r) = ( width ( - M1)) & ( - M1) is_symmetry_circulant_about r;

        hence thesis by A1;

      end;

    end

    registration

      let n, K;

      let M1,M2 be symmetry_circulant Matrix of n, K;

      cluster (M1 - M2) -> symmetry_circulant;

      coherence ;

    end

    theorem :: MATRIX17:7

    A is symmetry_circulant & n > 0 implies (A @ ) is symmetry_circulant

    proof

      assume that

       A1: A is symmetry_circulant and

       A2: n > 0 ;

      consider p be FinSequence of D such that

       A3: ( len p) = ( width A) and

       A4: A is_symmetry_circulant_about p by A1;

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

      then ( width (A @ )) = ( len p) by A2, A3, MATRIX_0: 54;

      then

      consider p be FinSequence of D such that

       A5: ( len p) = ( width (A @ )) & (A @ ) is_symmetry_circulant_about p by A2, A4, Th6;

      take p;

      thus thesis by A5;

    end;

    theorem :: MATRIX17:8

    

     Th8: p is first-symmetry-of-circulant implies ( - p) is first-symmetry-of-circulant

    proof

      set n = ( len p);

      assume p is first-symmetry-of-circulant;

      then

      consider M1 be Matrix of ( len p), K such that

       A1: M1 is_symmetry_circulant_about p;

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

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

      then

       A2: ( len ( - p)) = ( len p) by CARD_1:def 7;

      ( - M1) is_symmetry_circulant_about ( - p) by A1, Th4;

      then

      consider M2 be Matrix of ( len ( - p)), K such that

       A3: M2 is_symmetry_circulant_about ( - p) by A2;

      take M2;

      thus thesis by A3;

    end;

    theorem :: MATRIX17:9

    p is first-symmetry-of-circulant implies ( SCirc ( - p)) = ( - ( SCirc p))

    proof

      set n = ( len p);

      

       A1: ( len ( SCirc p)) = ( len p) & ( width ( SCirc p)) = ( len p) by MATRIX_0: 24;

      

       A2: ( Indices ( SCirc p)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

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

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

      then

       A3: ( len ( - p)) = ( len p) by CARD_1:def 7;

      assume

       A4: p is first-symmetry-of-circulant;

      then ( - p) is first-symmetry-of-circulant by Th8;

      then

       A5: ( SCirc ( - p)) is_symmetry_circulant_about ( - p) by Def7;

      

       A6: ( SCirc p) is_symmetry_circulant_about p by A4, Def7;

      

       A7: for i,j be Nat st [i, j] in ( Indices ( SCirc p)) holds (( SCirc ( - p)) * (i,j)) = ( - (( SCirc p) * (i,j)))

      proof

        let i,j be Nat;

        assume

         A8: [i, j] in ( Indices ( SCirc p));

        now

          per cases ;

            suppose

             A9: (i + j) <> (( len p) + 1);

            (((i + j) - 1) mod n) in ( Seg n) by A2, A8, A9, Lm4;

            then

             A10: (((i + j) - 1) mod ( len p)) in ( dom p) by FINSEQ_1:def 3;

             [i, j] in ( Indices ( SCirc ( - p))) by A3, A8, MATRIX_0: 26;

            

            then (( SCirc ( - p)) * (i,j)) = (( - p) . (((i + j) - 1) mod ( len ( - p)))) by A5, A9, A3

            .= (( comp K) . (p . (((i + j) - 1) mod ( len p)))) by A3, A10, FUNCT_1: 13

            .= (( comp K) . (( SCirc p) * (i,j))) by A6, A8, A9

            .= ( - (( SCirc p) * (i,j))) by VECTSP_1:def 13;

            hence thesis;

          end;

            suppose

             A11: (i + j) = (( len p) + 1);

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

            then 1 <= i & 1 <= j by FINSEQ_1: 1;

            then (1 + 1) <= (i + j) by XREAL_1: 7;

            then ((( len p) + 1) - 1) >= ((1 + 1) - 1) by A11, XREAL_1: 9;

            then ( len p) in ( Seg ( len p));

            then

             A12: ( len p) in ( dom p) by FINSEQ_1:def 3;

             [i, j] in ( Indices ( SCirc ( - p))) by A3, A8, MATRIX_0: 26;

            

            then (( SCirc ( - p)) * (i,j)) = (( - p) . ( len ( - p))) by A5, A11, A3

            .= (( comp K) . (p . ( len p))) by A3, A12, FUNCT_1: 13

            .= (( comp K) . (( SCirc p) * (i,j))) by A6, A8, A11

            .= ( - (( SCirc p) * (i,j))) by VECTSP_1:def 13;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      ( len ( SCirc ( - p))) = ( len p) & ( width ( SCirc ( - p))) = ( len p) by A3, MATRIX_0: 24;

      hence thesis by A1, A7, MATRIX_3:def 2;

    end;

    theorem :: MATRIX17:10

    

     Th10: p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & ( len p) = ( len q) implies (p + q) is first-symmetry-of-circulant

    proof

      set n = ( len p);

      assume that

       A1: p is first-symmetry-of-circulant and

       A2: q is first-symmetry-of-circulant and

       A3: ( len p) = ( len q);

      consider M2 be Matrix of n, K such that

       A4: M2 is_symmetry_circulant_about q by A2, A3;

      

       A5: ( dom p) = ( Seg n) by FINSEQ_1:def 3;

      ( dom q) = ( Seg n) by A3, FINSEQ_1:def 3;

      then ( dom (p + q)) = ( dom p) by A5, POLYNOM1: 1;

      then

       A6: ( len (p + q)) = n by A5, FINSEQ_1:def 3;

      consider M1 be Matrix of n, K such that

       A7: M1 is_symmetry_circulant_about p by A1;

      ( width (M1 + M2)) = n by MATRIX_0: 24;

      then

      consider M3 be Matrix of ( len (p + q)), K such that ( len (p + q)) = ( width M3) and

       A8: M3 is_symmetry_circulant_about (p + q) by A6, A4, A7, Th5;

      take M3;

      thus thesis by A8;

    end;

    theorem :: MATRIX17:11

    

     Th11: ( len p) = ( len q) & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant implies ( SCirc (p + q)) = (( SCirc p) + ( SCirc q))

    proof

      set n = ( len p);

      assume that

       A1: ( len p) = ( len q) and

       A2: p is first-symmetry-of-circulant and

       A3: q is first-symmetry-of-circulant;

      

       A4: ( SCirc q) is_symmetry_circulant_about q & ( Indices ( SCirc p)) = ( Indices ( SCirc q)) by A1, A3, Def7, MATRIX_0: 26;

      (p + q) is first-symmetry-of-circulant by A1, A2, A3, Th10;

      then

       A5: ( SCirc (p + q)) is_symmetry_circulant_about (p + q) by Def7;

      

       A6: ( dom p) = ( Seg n) by FINSEQ_1:def 3;

      

       A7: ( SCirc p) is_symmetry_circulant_about p by A2, Def7;

      

       A8: ( dom (p + q)) = ( Seg ( len (p + q))) by FINSEQ_1:def 3;

      

       A9: ( Indices ( SCirc p)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      ( dom q) = ( Seg n) by A1, FINSEQ_1:def 3;

      then ( dom (p + q)) = ( dom p) by A6, POLYNOM1: 1;

      then

       A10: ( len (p + q)) = n by A6, FINSEQ_1:def 3;

      then

       A11: ( Indices ( SCirc p)) = ( Indices ( SCirc (p + q))) by MATRIX_0: 26;

      

       A12: for i,j be Nat holds [i, j] in ( Indices ( SCirc p)) implies (( SCirc (p + q)) * (i,j)) = ((( SCirc p) * (i,j)) + (( SCirc q) * (i,j)))

      proof

        let i,j be Nat;

        assume

         A13: [i, j] in ( Indices ( SCirc p));

        now

          per cases ;

            suppose

             A14: (i + j) <> (( len (p + q)) + 1);

            

             A15: (((i + j) - 1) mod n) in ( Seg n) by A9, A13, A14, A10, Lm4;

            (( SCirc (p + q)) * (i,j)) = ((p + q) . (((i + j) - 1) mod ( len (p + q)))) by A5, A11, A13, A14

            .= (the addF of K . ((p . (((i + j) - 1) mod ( len (p + q)))),(q . (((i + j) - 1) mod ( len (p + q)))))) by A8, A10, A15, FUNCOP_1: 22

            .= (the addF of K . ((( SCirc p) * (i,j)),(q . (((i + j) - 1) mod ( len q))))) by A1, A10, A7, A13, A14

            .= ((( SCirc p) * (i,j)) + (( SCirc q) * (i,j))) by A1, A4, A13, A14, A10;

            hence thesis;

          end;

            suppose

             A16: (i + j) = (( len (p + q)) + 1);

            i in ( Seg n) & j in ( Seg n) by A9, A13, ZFMISC_1: 87;

            then 1 <= i & 1 <= j by FINSEQ_1: 1;

            then (1 + 1) <= (i + j) by XREAL_1: 7;

            then ((( len (p + q)) + 1) - 1) >= ((1 + 1) - 1) by A16, XREAL_1: 9;

            then ( len (p + q)) in ( Seg ( len (p + q)));

            then

             A17: ( len (p + q)) in ( dom (p + q)) by FINSEQ_1:def 3;

            (( SCirc (p + q)) * (i,j)) = ((p + q) . ( len (p + q))) by A5, A11, A13, A16

            .= (the addF of K . ((p . ( len (p + q))),(q . ( len (p + q))))) by A17, FUNCOP_1: 22

            .= (the addF of K . ((( SCirc p) * (i,j)),(q . ( len q)))) by A1, A10, A7, A13, A16

            .= ((( SCirc p) * (i,j)) + (( SCirc q) * (i,j))) by A4, A13, A16, A1, A10;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A18: ( len ( SCirc p)) = ( len p) & ( width ( SCirc p)) = ( len p) by MATRIX_0: 24;

      ( len ( SCirc (p + q))) = ( len p) & ( width ( SCirc (p + q))) = ( len p) by A10, MATRIX_0: 24;

      hence thesis by A18, A12, MATRIX_3:def 3;

    end;

    theorem :: MATRIX17:12

    

     Th12: p is first-symmetry-of-circulant implies (a * p) is first-symmetry-of-circulant

    proof

      set n = ( len p);

      

       A1: ( len (a * p)) = ( len p) by MATRIXR1: 16;

      assume p is first-symmetry-of-circulant;

      then

      consider M1 be Matrix of n, K such that

       A2: M1 is_symmetry_circulant_about p;

      (a * M1) is_symmetry_circulant_about (a * p) by A2, Th3;

      then

      consider M2 be Matrix of ( len (a * p)), K such that

       A3: M2 is_symmetry_circulant_about (a * p) by A1;

      take M2;

      thus thesis by A3;

    end;

    theorem :: MATRIX17:13

    

     Th13: p is first-symmetry-of-circulant implies ( SCirc (a * p)) = (a * ( SCirc p))

    proof

      set n = ( len p);

      

       A1: ( len (a * p)) = ( len p) by MATRIXR1: 16;

      assume

       A2: p is first-symmetry-of-circulant;

      then (a * p) is first-symmetry-of-circulant by Th12;

      then

       A3: ( SCirc (a * p)) is_symmetry_circulant_about (a * p) by Def7;

      

       A4: ( Indices ( SCirc p)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( SCirc p) is_symmetry_circulant_about p by A2, Def7;

      

       A6: for i,j be Nat st [i, j] in ( Indices ( SCirc p)) holds (( SCirc (a * p)) * (i,j)) = (a * (( SCirc p) * (i,j)))

      proof

        let i,j be Nat;

        

         A7: ( dom (a * p)) = ( Seg ( len (a * p))) by FINSEQ_1:def 3;

        assume

         A8: [i, j] in ( Indices ( SCirc p));

        now

          per cases ;

            suppose

             A9: (i + j) <> (( len p) + 1);

            

             A10: (((i + j) - 1) mod n) in ( Seg n) by A4, A8, A9, Lm4;

            

             A11: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

             [i, j] in ( Indices ( SCirc (a * p))) by A1, A8, MATRIX_0: 26;

            

            then (( SCirc (a * p)) * (i,j)) = ((a * p) . (((i + j) - 1) mod ( len (a * p)))) by A1, A3, A9

            .= ((a * p) /. (((i + j) - 1) mod ( len p))) by A1, A10, A7, PARTFUN1:def 6

            .= (a * (p /. (((i + j) - 1) mod ( len p)))) by A10, A11, POLYNOM1:def 1

            .= ((a multfield ) . (p /. (((i + j) - 1) mod ( len p)))) by FVSUM_1: 49

            .= ((a multfield ) . (p . (((i + j) - 1) mod ( len p)))) by A10, A11, PARTFUN1:def 6

            .= ((a multfield ) . (( SCirc p) * (i,j))) by A5, A8, A9

            .= (a * (( SCirc p) * (i,j))) by FVSUM_1: 49;

            hence thesis;

          end;

            suppose

             A12: (i + j) = (( len p) + 1);

            

             A13: [i, j] in ( Indices ( SCirc (a * p))) by A1, A8, MATRIX_0: 26;

            i in ( Seg n) & j in ( Seg n) by A4, A8, ZFMISC_1: 87;

            then 1 <= i & 1 <= j by FINSEQ_1: 1;

            then (1 + 1) <= (i + j) by XREAL_1: 7;

            then ((( len p) + 1) - 1) >= ((1 + 1) - 1) by A12, XREAL_1: 9;

            then

             A14: ( len p) in ( Seg ( len p));

            then

             A15: ( len p) in ( dom (a * p)) by A1, FINSEQ_1:def 3;

            

             A16: ( len p) in ( dom p) by A14, FINSEQ_1:def 3;

            (( SCirc (a * p)) * (i,j)) = ((a * p) . ( len (a * p))) by A1, A3, A12, A13

            .= ((a * p) /. ( len p)) by A1, A15, PARTFUN1:def 6

            .= (a * (p /. ( len p))) by A16, POLYNOM1:def 1

            .= ((a multfield ) . (p /. ( len p))) by FVSUM_1: 49

            .= ((a multfield ) . (p . ( len p))) by A16, PARTFUN1:def 6

            .= ((a multfield ) . (( SCirc p) * (i,j))) by A5, A8, A12

            .= (a * (( SCirc p) * (i,j))) by FVSUM_1: 49;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A17: ( len ( SCirc p)) = ( len p) & ( width ( SCirc p)) = ( len p) by MATRIX_0: 24;

      ( len ( SCirc (a * p))) = ( len p) & ( width ( SCirc (a * p))) = ( len p) by A1, MATRIX_0: 24;

      hence thesis by A17, A6, MATRIX_3:def 5;

    end;

    theorem :: MATRIX17:14

    p is first-symmetry-of-circulant implies ((a * ( SCirc p)) + (b * ( SCirc p))) = ( SCirc ((a + b) * p))

    proof

      

       A1: ( len (b * p)) = ( len p) by MATRIXR1: 16;

      

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

      assume

       A3: p is first-symmetry-of-circulant;

      then

       A4: (a * p) is first-symmetry-of-circulant & (b * p) is first-symmetry-of-circulant by Th12;

      (a * ( SCirc p)) = ( SCirc (a * p)) & (b * ( SCirc p)) = ( SCirc (b * p)) by A3, Th13;

      then ((a * ( SCirc p)) + (b * ( SCirc p))) = ( SCirc ((a * p) + (b * p))) by A4, A1, Th11, MATRIXR1: 16;

      hence thesis by A2, FVSUM_1: 55;

    end;

    theorem :: MATRIX17:15

    p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & ( len p) = ( len q) implies ((a * ( SCirc p)) + (a * ( SCirc q))) = ( SCirc (a * (p + q)))

    proof

      assume that

       A1: p is first-symmetry-of-circulant & q is first-symmetry-of-circulant and

       A2: ( len p) = ( len q);

      

       A3: ( len ( SCirc p)) = ( len p) & ( width ( SCirc p)) = ( len p) by MATRIX_0: 24;

      ( len ( SCirc q)) = ( len p) & ( width ( SCirc q)) = ( len p) by A2, MATRIX_0: 24;

      

      then ((a * ( SCirc p)) + (a * ( SCirc q))) = (a * (( SCirc p) + ( SCirc q))) by A3, MATRIX_5: 20

      .= (a * ( SCirc (p + q))) by A1, A2, Th11

      .= ( SCirc (a * (p + q))) by A1, A2, Th10, Th13;

      hence thesis;

    end;

    theorem :: MATRIX17:16

    p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & ( len p) = ( len q) implies ((a * ( SCirc p)) + (b * ( SCirc q))) = ( SCirc ((a * p) + (b * q)))

    proof

      set n = ( len p);

      assume that

       A1: p is first-symmetry-of-circulant and

       A2: q is first-symmetry-of-circulant and

       A3: ( len p) = ( len q);

      

       A4: (a * p) is first-symmetry-of-circulant & (b * q) is first-symmetry-of-circulant by A1, A2, Th12;

      

       A5: ( len (b * q)) = n by A3, MATRIXR1: 16;

      ((a * ( SCirc p)) + (b * ( SCirc q))) = (( SCirc (a * p)) + (b * ( SCirc q))) by A1, Th13

      .= (( SCirc (a * p)) + ( SCirc (b * q))) by A2, Th13

      .= ( SCirc ((a * p) + (b * q))) by A4, A5, Th11, MATRIXR1: 16;

      hence thesis;

    end;

    theorem :: MATRIX17:17

    

     Th17: M1 is symmetry_circulant implies (M1 @ ) = M1

    proof

      assume M1 is symmetry_circulant;

      then

      consider p be FinSequence of K such that ( len p) = ( width M1) and

       A1: M1 is_symmetry_circulant_about p;

      

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

      

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

      

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

      for i,j be Nat st [i, j] in ( Indices M1) holds ((M1 @ ) * (i,j)) = (M1 * (i,j))

      proof

        let i,j be Nat;

        assume

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

        per cases ;

          suppose

           A6: (i + j) <> (( len p) + 1);

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

          then

           A7: [j, i] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

          

          then ((M1 @ ) * (i,j)) = (M1 * (j,i)) by A2, MATRIX_0:def 6

          .= (p . (((i + j) - 1) mod ( len p))) by A1, A7, A6, A2;

          hence thesis by A1, A5, A6;

        end;

          suppose

           A8: (i + j) = (( len p) + 1);

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

          then

           A9: [j, i] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

          ((M1 @ ) * (i,j)) = (M1 * (j,i)) by A2, A9, MATRIX_0:def 6

          .= (p . ( len p)) by A1, A9, A8, A2;

          hence thesis by A1, A8, A5;

        end;

      end;

      hence thesis by A3, A4, MATRIX_0: 21;

    end;

    registration

      let n, K;

      cluster symmetry_circulant -> symmetric for Matrix of n, K;

      coherence by Th17;

    end