matrix16.miz



    begin

    reserve i,j,k,n,l for Element of 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 k be Nat st k <= n & k >= 1 holds ((k - 1) mod n) = (k - 1)

    proof

      let k be Nat;

      assume that

       A1: k <= n and

       A2: k >= 1;

      

       A3: (k - 1) >= (1 - 1) by A2, XREAL_1: 9;

      

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

      (k - 1) <= (n - 1) by A1, XREAL_1: 9;

      then (k - 1) < n by A4, XXREAL_0: 2;

      hence thesis by A3, NAT_D: 63;

    end;

    

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

    proof

      let n,i,j be Nat;

      assume that

       A1: i in ( Seg n) and

       A2: j in ( Seg n);

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

      then

       A3: (1 - n) <= (j - i) by XREAL_1: 13;

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

      then

       A4: (j - i) <= (n - 1) by XREAL_1: 13;

      ( - n) <= (( - n) + 1) by XREAL_1: 29;

      then

       A5: ( - n) <= (j - i) by A3, XXREAL_0: 2;

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

      then

       A6: (j - i) < n by A4, XXREAL_0: 2;

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

      proof

        per cases ;

          suppose 0 <= (j - i);

          hence thesis by A4, A6, NAT_D: 63;

        end;

          suppose

           A7: 0 > (j - i);

          then (j - i) <= ( - 1) by INT_1: 8;

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

          hence thesis by A5, A7, NAT_D: 63;

        end;

      end;

      then

       A8: (((j - i) mod n) + 1) <= ((n - 1) + 1) by XREAL_1: 6;

      n > 0 by A1, FINTOPO5: 2;

      then ((j - i) mod n) >= 0 by NAT_D: 62;

      then (((j - i) mod n) + 1) >= ( 0 + 1) & (((j - i) mod n) + 1) in NAT by INT_1: 3, XREAL_1: 6;

      hence thesis by A8;

    end;

    

     Lm3: for n,i,j be Nat holds ( [i, j] in [:( Seg n), ( Seg n):] or [j, i] in [:( Seg n), ( Seg n):]) implies (((j - i) mod n) + 1) in ( Seg n)

    proof

      let n,i,j be Nat;

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

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

      hence thesis by Lm2;

    end;

    theorem :: MATRIX16:1

    (( 1_ K) * p) = p

    proof

      

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

      

       A2: ( Seg ( len (( 1_ K) * p))) = ( Seg ( len p)) & ( dom (( 1_ K) * p)) = ( Seg ( len (( 1_ K) * p))) by FINSEQ_1:def 3, MATRIXR1: 16;

      for i be Nat st i in ( dom p) holds ((( 1_ K) * p) . i) = (p . i)

      proof

        let i be Nat;

        

         A3: ( rng p) c= the carrier of K by FINSEQ_1:def 4;

        assume

         A4: i in ( dom p);

        then

         A5: (p . i) in ( dom (the multF of K [;] (( 1_ K),( id the carrier of K)))) by A2, A1, FUNCT_1: 11;

        (p . i) in ( rng p) by A4, FUNCT_1: 3;

        then

        reconsider b = (p . i) as Element of K by A3;

        ((( 1_ K) * p) . i) = ((( 1_ K) multfield ) . (p . i)) by A4, FUNCT_1: 13

        .= (the multF of K . (( 1_ K),(( id the carrier of K) . (p . i)))) by A5, FUNCOP_1: 32

        .= (( 1_ K) * b)

        .= (p . i);

        hence thesis;

      end;

      hence thesis by A2, A1, FINSEQ_1: 13;

    end;

    theorem :: MATRIX16:2

    (( - ( 1_ K)) * p) = ( - p)

    proof

      

       A1: ( Seg ( len (( - ( 1_ K)) * p))) = ( Seg ( len p)) & ( dom (( - ( 1_ K)) * p)) = ( Seg ( len (( - ( 1_ K)) * p))) by FINSEQ_1:def 3, MATRIXR1: 16;

      

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

      

       A3: for i be Nat st i in ( dom p) holds ((( - ( 1_ K)) * p) . i) = (( - p) . i)

      proof

        let i be Nat;

        

         A4: ( rng p) c= the carrier of K by FINSEQ_1:def 4;

        assume

         A5: i in ( dom p);

        then

         A6: (p . i) in ( dom (the multF of K [;] (( - ( 1_ K)),( id the carrier of K)))) by A1, A2, FUNCT_1: 11;

        (p . i) in ( rng p) by A5, FUNCT_1: 3;

        then

        reconsider b = (p . i) as Element of K by A4;

        ((( - ( 1_ K)) * b) + b) = ((( - ( 1_ K)) * b) + (( 1_ K) * b))

        .= ((( - ( 1_ K)) + ( 1_ K)) * b) by VECTSP_1:def 7

        .= (( 0. K) * b) by RLVECT_1: 5

        .= ( 0. K);

        then ((( - ( 1_ K)) * b) + (b + ( - b))) = (( 0. K) + ( - b)) by RLVECT_1:def 3;

        

        then (( 0. K) + ( - b)) = ((( - ( 1_ K)) * b) + ( 0. K)) by RLVECT_1: 5

        .= (( - ( 1_ K)) * b) by RLVECT_1: 4;

        then

         A7: (( - ( 1_ K)) * b) = ( - b) by RLVECT_1: 4;

        ((( - ( 1_ K)) * p) . i) = ((( - ( 1_ K)) multfield ) . (p . i)) by A5, FUNCT_1: 13

        .= (the multF of K . (( - ( 1_ K)),(( id the carrier of K) . (p . i)))) by A6, FUNCOP_1: 32

        .= (the multF of K . (( - ( 1_ K)),b))

        .= (( comp K) . b) by A7, VECTSP_1:def 13

        .= (( - p) . i) by A5, FUNCT_1: 13;

        hence thesis;

      end;

      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

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

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

      hence thesis by A1, A3, A8, FINSEQ_1: 13;

    end;

    definition

      let K be set;

      let M be Matrix of K;

      let p be FinSequence;

      :: MATRIX16:def1

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

    end

    definition

      let K be set;

      let M be Matrix of K;

      :: MATRIX16:def2

      attr M is line_circulant means ex p be FinSequence of K st ( len p) = ( width M) & M is_line_circulant_about p;

    end

    definition

      let K be non empty set;

      let p be FinSequence of K;

      :: MATRIX16:def3

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

    end

    definition

      let K be set;

      let M be Matrix of K;

      let p be FinSequence;

      :: MATRIX16:def4

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

    end

    definition

      let K be set;

      let M be Matrix of K;

      :: MATRIX16:def5

      attr M is col_circulant means ex p be FinSequence of K st ( len p) = ( len M) & M is_col_circulant_about p;

    end

    definition

      let K be non empty set;

      let p be FinSequence of K;

      :: MATRIX16:def6

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

    end

    definition

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

      assume

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

      :: MATRIX16:def7

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

      : Def7: it is_line_circulant_about p;

      existence by A1;

      uniqueness

      proof

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

        assume that

         A2: M1 is_line_circulant_about p and

         A3: M2 is_line_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);

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

          hence thesis by A3, A4, A5;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    definition

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

      assume

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

      :: MATRIX16:def8

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

      : Def8: it is_col_circulant_about p;

      existence by A1;

      uniqueness

      proof

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

        assume that

         A2: M1 is_col_circulant_about p and

         A3: M2 is_col_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);

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

          hence thesis by A3, A4, A5;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    registration

      let K be Field;

      cluster first-line-of-circulant first-col-of-circulant for FinSequence of K;

      existence

      proof

        

         A1: ( 0. (K,1,1)) = (1 |-> (1 |-> ( 0. K)));

        set M1 = ( 0. (K,1));

        take p = (1 |-> ( 0. K));

        

         A2: ( len (1 |-> ( 0. K))) = 1 by CARD_1:def 7;

        

         A3: ( Indices ( 0. (K,1))) = [:( Seg 1), ( Seg 1):] by MATRIX_0: 24;

        

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

        proof

          let i,j be Nat;

          assume

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

          then (((i - j) mod 1) + 1) in ( Seg 1) by A3, Lm3;

          then ((( Seg 1) --> ( 0. K)) . (((i - j) mod 1) + 1)) = ( 0. K) by FUNCOP_1: 7;

          hence thesis by A2, A1, A5, MATRIX_3: 1;

        end;

        

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

        proof

          let i,j be Nat;

          assume

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

          then (((j - i) mod 1) + 1) in ( Seg 1) by A3, Lm3;

          then ((( Seg 1) --> ( 0. K)) . (((j - i) mod 1) + 1)) = ( 0. K) by FUNCOP_1: 7;

          hence thesis by A2, A1, A7, MATRIX_3: 1;

        end;

        ( width ( 0. (K,1))) = 1 by MATRIX_0: 24;

        then M1 is_line_circulant_about p by A2, A6;

        hence p is first-line-of-circulant by A2;

        ( len ( 0. (K,1))) = 1 by MATRIX_0: 24;

        then M1 is_col_circulant_about p by A2, A4;

        hence thesis by A2;

      end;

    end

    registration

      let K, n;

      cluster ( 0. (K,n)) -> line_circulant col_circulant;

      coherence

      proof

        set p = (n |-> ( 0. K));

        

         A1: ( len ( 0. (K,n))) = n by MATRIX_0: 24;

        

         A2: ( 0. (K,n,n)) = (n |-> (n |-> ( 0. K)));

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

        

         A3: ( len (n |-> ( 0. K))) = n by CARD_1:def 7;

        

         A4: ( Indices ( 0. (K,n))) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

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

        proof

          let i,j be Nat;

          assume

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

          then (((i - j) mod n) + 1) in ( Seg n) by A4, Lm3;

          then (((i - j) mod ( len p)) + 1) in ( Seg n) by CARD_1:def 7;

          then ((( Seg n) --> ( 0. K)) . (((i - j) mod ( len p)) + 1)) = ( 0. K) by FUNCOP_1: 7;

          hence thesis by A2, A5, MATRIX_3: 1;

        end;

        then

         A6: M1 is_col_circulant_about p by A1, A3;

        

         A7: ( width ( 0. (K,n))) = n by MATRIX_0: 24;

        thus M1 is line_circulant

        proof

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

          proof

            let i,j be Nat;

            assume

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

            then (((j - i) mod n) + 1) in ( Seg n) by A4, Lm3;

            then ((( Seg n) --> ( 0. K)) . (((j - i) mod n) + 1)) = ( 0. K) by FUNCOP_1: 7;

            hence thesis by A3, A2, A8, MATRIX_3: 1;

          end;

          then M1 is_line_circulant_about p by A7, A3;

          then

          consider p be FinSequence of K such that

           A9: ( len p) = ( width M1) & M1 is_line_circulant_about p;

          take p;

          thus thesis by A9;

        end;

        consider p be FinSequence of K such that

         A10: ( len p) = ( len M1) & M1 is_col_circulant_about p by A6;

        take p;

        thus thesis by A10;

      end;

    end

    registration

      let K;

      let n;

      let a be Element of K;

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

      coherence

      proof

        set p = (n |-> a);

        

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

        

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

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

        proof

          let i,j be Nat;

          assume

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

          then (((j - i) mod n) + 1) in ( Seg n) by A2, Lm3;

          then (((j - i) mod ( len p)) + 1) in ( Seg n) by CARD_1:def 7;

          then ((( Seg n) --> a) . (((j - i) mod ( len p)) + 1)) = a by FUNCOP_1: 7;

          hence thesis by A3, MATRIX_0: 46;

        end;

        then ((n,n) --> a) is_line_circulant_about p by A1;

        hence thesis;

      end;

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

      coherence

      proof

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

        set p = (n |-> a);

        

         A4: ( len ((n,n) --> a)) = n & ( len p) = n by CARD_1:def 7;

        

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

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

        proof

          let i,j be Nat;

          assume

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

          then (((i - j) mod n) + 1) in ( Seg n) by A5, Lm3;

          then (((i - j) mod ( len p)) + 1) in ( Seg n) by CARD_1:def 7;

          then ((( Seg n) --> a) . (((i - j) mod ( len p)) + 1)) = a by FUNCOP_1: 7;

          hence thesis by A6, MATRIX_0: 46;

        end;

        then M1 is_col_circulant_about p by A4;

        hence thesis;

      end;

    end

    registration

      let K;

      cluster line_circulant col_circulant for Matrix of K;

      existence

      proof

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

        thus thesis;

      end;

    end

    reserve D for non empty set,

t for FinSequence of D,

A for Matrix of n, D;

    theorem :: MATRIX16:3

    A is line_circulant & n > 0 implies (A @ ) is col_circulant

    proof

      assume that

       A1: A is line_circulant and

       A2: n > 0 ;

      consider p be FinSequence of D such that

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

       A4: A is_line_circulant_about p by A1;

      ( width A) = n by MATRIX_0: 24;

      then

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

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

      proof

        let i,j be Nat;

        

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

        assume [i, j] in ( Indices (A @ ));

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

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

        then

         A7: [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 A4, A7;

      end;

      then (A @ ) is_col_circulant_about p by A5;

      then

      consider p be FinSequence of D such that

       A8: ( len p) = ( len (A @ )) & (A @ ) is_col_circulant_about p;

      take p;

      thus thesis by A8;

    end;

    theorem :: MATRIX16:4

    A is_line_circulant_about t & n > 0 implies t = ( Line (A,1))

    proof

      assume that

       A1: A is_line_circulant_about t and

       A2: n > 0 ;

      

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

      then

       A4: ( dom t) = ( Seg ( len t)) & ( len t) = n by A1, FINSEQ_1:def 3;

      

       A5: for k be Nat st k in ( dom t) holds (t . k) = (( Line (A,1)) . k)

      proof

        let k be Nat;

        assume

         A6: k in ( dom t);

        then

         A7: 1 <= k & k <= n by A4, FINSEQ_1: 1;

        n >= ( 0 + 1) by A2, INT_1: 7;

        then 1 in ( Seg n);

        then [1, k] in [:( Seg n), ( Seg n):] by A4, A6, ZFMISC_1:def 2;

        then

         A8: [1, k] in ( Indices A) by MATRIX_0: 24;

        (( Line (A,1)) . k) = (A * (1,k)) by A3, A4, A6, MATRIX_0:def 7

        .= (t . (((k - 1) mod ( len t)) + 1)) by A1, A8

        .= (t . (((k - 1) mod n) + 1)) by A1, A3

        .= (t . ((k - 1) + 1)) by A7, Lm1;

        hence thesis;

      end;

      ( len ( Line (A,1))) = n by A3, MATRIX_0:def 7;

      then ( dom ( Line (A,1))) = ( dom t) by A4, FINSEQ_1:def 3;

      hence thesis by A5, FINSEQ_1: 13;

    end;

    theorem :: MATRIX16:5

    A is line_circulant & [i, j] in [:( Seg n), ( Seg n):] & k = (i + 1) & l = (j + 1) & i < n & j < n implies (A * (i,j)) = (A * (k,l))

    proof

      assume that

       A1: A is line_circulant and

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

       A3: k = (i + 1) and

       A4: l = (j + 1) and

       A5: i < n and

       A6: j < n;

      consider p be FinSequence of D such that ( len p) = ( width A) and

       A7: A is_line_circulant_about p by A1;

      

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

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

      then 1 <= j by FINSEQ_1: 1;

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

      then

       A9: 1 <= (j + 1) by XXREAL_0: 2;

      (j + 1) <= n by A6, INT_1: 7;

      then

       A10: l in ( Seg n) by A4, A9;

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

      then 1 <= i by FINSEQ_1: 1;

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

      then

       A11: 1 <= (i + 1) by XXREAL_0: 2;

      (i + 1) <= n by A5, INT_1: 7;

      then k in ( Seg n) by A3, A11;

      then [k, l] in ( Indices A) by A8, A10, ZFMISC_1: 87;

      

      then (A * (k,l)) = (p . (((l - k) mod ( len p)) + 1)) by A7

      .= (p . (((j - i) mod ( len p)) + 1)) by A3, A4

      .= (A * (i,j)) by A2, A7, A8;

      hence thesis;

    end;

    theorem :: MATRIX16:6

    

     Th6: M1 is line_circulant implies (a * M1) is line_circulant

    proof

      

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

      assume M1 is line_circulant;

      then

      consider p be FinSequence of K such that

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

       A3: M1 is_line_circulant_about p;

      

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

      proof

        let i,j be Nat;

        assume

         A8: [i, j] in ( Indices (a * M1));

        then

         A9: (((j - i) mod n) + 1) in ( Seg n) by A1, Lm3;

        then

         A10: (((j - i) mod ( len p)) + 1) in ( dom (a * p)) by A2, A4, A6, MATRIXR1: 16;

        

         A11: [i, j] in ( Indices M1) by A1, A8, 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 . (((j - i) mod ( len p)) + 1))) by A3, A11

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

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

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

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

        hence thesis by MATRIXR1: 16;

      end;

      

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

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

      then (a * M1) is_line_circulant_about (a * p) by A12, A7;

      then

      consider q be FinSequence of K such that

       A13: ( len q) = ( width (a * M1)) & (a * M1) is_line_circulant_about q;

      take q;

      thus thesis by A13;

    end;

    theorem :: MATRIX16:7

    

     Th7: M1 is line_circulant & M2 is line_circulant implies (M1 + M2) is line_circulant

    proof

      assume that

       A1: M1 is line_circulant and

       A2: M2 is line_circulant;

      consider p be FinSequence of K such that

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

       A4: M1 is_line_circulant_about p by A1;

      

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

      

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

      

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

      then

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

      consider q be FinSequence of K such that

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

       A10: M2 is_line_circulant_about q by A2;

      

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

      

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

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

      then

       A13: ( dom (p + q)) = ( dom p) by A8, POLYNOM1: 1;

      then

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

      

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

      

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

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

      proof

        let i,j be Nat;

        assume

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

        then

         A18: (((j - i) mod ( len (p + q))) + 1) in ( dom (p + q)) by A6, A8, A16, A13, Lm3;

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

        .= (the addF of K . ((M1 * (i,j)),(q . (((j - i) mod ( len q)) + 1)))) by A10, A5, A6, A17

        .= (the addF of K . ((p . (((j - i) mod ( len (p + q))) + 1)),(q . (((j - i) mod ( len (p + q))) + 1)))) by A4, A9, A11, A7, A12, A6, A14, A17

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

        hence thesis;

      end;

      then (M1 + M2) is_line_circulant_about (p + q) by A15, A14;

      then

      consider r be FinSequence of K such that

       A19: ( len r) = ( width (M1 + M2)) & (M1 + M2) is_line_circulant_about r;

      take r;

      thus thesis by A19;

    end;

    theorem :: MATRIX16:8

    

     Th8: M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies ((M1 + M2) + M3) is line_circulant

    proof

      assume that

       A1: M1 is line_circulant & M2 is line_circulant and

       A2: M3 is line_circulant;

      (M1 + M2) is line_circulant by A1, Th7;

      hence thesis by A2, Th7;

    end;

    theorem :: MATRIX16:9

    M1 is line_circulant & M2 is line_circulant implies ((a * M1) + (b * M2)) is line_circulant

    proof

      assume M1 is line_circulant & M2 is line_circulant;

      then (a * M1) is line_circulant & (b * M2) is line_circulant by Th6;

      hence thesis by Th7;

    end;

    theorem :: MATRIX16:10

    M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies (((a * M1) + (b * M2)) + (c * M3)) is line_circulant

    proof

      assume that

       A1: M1 is line_circulant & M2 is line_circulant and

       A2: M3 is line_circulant;

      

       A3: (c * M3) is line_circulant by A2, Th6;

      (a * M1) is line_circulant & (b * M2) is line_circulant by A1, Th6;

      hence thesis by A3, Th8;

    end;

    theorem :: MATRIX16:11

    

     Th11: M1 is line_circulant implies ( - M1) is line_circulant

    proof

      

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

      

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

      assume M1 is line_circulant;

      then

      consider p be FinSequence of K such that

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

       A4: M1 is_line_circulant_about p;

      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;

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

      proof

        let i,j be Nat;

        assume

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

        then (((j - i) mod n) + 1) in ( Seg n) by A2, Lm3;

        then

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

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A7, A2, A8, MATRIX_3:def 2

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

        .= (( comp K) . (p . (((j - i) mod ( len p)) + 1))) by A4, A7, A2, A8

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

        hence thesis by A5, CARD_1:def 7;

      end;

      then ( - M1) is_line_circulant_about ( - p) by A3, A1, A6;

      then

      consider r be FinSequence of K such that

       A10: ( len r) = ( width ( - M1)) & ( - M1) is_line_circulant_about r;

      take r;

      thus thesis by A10;

    end;

    theorem :: MATRIX16:12

    M1 is line_circulant & M2 is line_circulant implies (M1 - M2) is line_circulant

    proof

      assume that

       A1: M1 is line_circulant and

       A2: M2 is line_circulant;

      ( - M2) is line_circulant by A2, Th11;

      hence thesis by A1, Th7;

    end;

    theorem :: MATRIX16:13

    

     Th13: M1 is line_circulant & M2 is line_circulant implies ((a * M1) - (b * M2)) is line_circulant

    proof

      assume that

       A1: M1 is line_circulant and

       A2: M2 is line_circulant;

      (b * M2) is line_circulant by A2, Th6;

      then

       A3: ( - (b * M2)) is line_circulant by Th11;

      (a * M1) is line_circulant by A1, Th6;

      hence thesis by A3, Th7;

    end;

    theorem :: MATRIX16:14

    M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies (((a * M1) + (b * M2)) - (c * M3)) is line_circulant

    proof

      assume that

       A1: M1 is line_circulant & M2 is line_circulant and

       A2: M3 is line_circulant;

      (c * M3) is line_circulant by A2, Th6;

      then

       A3: ( - (c * M3)) is line_circulant by Th11;

      (a * M1) is line_circulant & (b * M2) is line_circulant by A1, Th6;

      then ((a * M1) + (b * M2)) is line_circulant by Th7;

      hence thesis by A3, Th7;

    end;

    theorem :: MATRIX16:15

    M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies (((a * M1) - (b * M2)) - (c * M3)) is line_circulant

    proof

      assume that

       A1: M1 is line_circulant & M2 is line_circulant and

       A2: M3 is line_circulant;

      (c * M3) is line_circulant by A2, Th6;

      then

       A3: ( - (c * M3)) is line_circulant by Th11;

      ((a * M1) - (b * M2)) is line_circulant by A1, Th13;

      hence thesis by A3, Th7;

    end;

    theorem :: MATRIX16:16

    M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies (((a * M1) - (b * M2)) + (c * M3)) is line_circulant

    proof

      assume M1 is line_circulant & M2 is line_circulant & M3 is line_circulant;

      then (c * M3) is line_circulant & ((a * M1) - (b * M2)) is line_circulant by Th6, Th13;

      hence thesis by Th7;

    end;

    theorem :: MATRIX16:17

    A is col_circulant & n > 0 implies (A @ ) is line_circulant

    proof

      assume that

       A1: A is col_circulant and

       A2: n > 0 ;

      consider p be FinSequence of D such that

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

       A4: A is_col_circulant_about p by A1;

      ( width A) = n by MATRIX_0: 24;

      then

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

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

      proof

        let i,j be Nat;

        

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

        assume [i, j] in ( Indices (A @ ));

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

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

        then

         A7: [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 A4, A7;

      end;

      then (A @ ) is_line_circulant_about p by A5;

      then

      consider p be FinSequence of D such that

       A8: ( len p) = ( width (A @ )) & (A @ ) is_line_circulant_about p;

      take p;

      thus thesis by A8;

    end;

    theorem :: MATRIX16:18

    A is_col_circulant_about t & n > 0 implies t = ( Col (A,1))

    proof

      assume that

       A1: A is_col_circulant_about t and

       A2: n > 0 ;

      

       A3: ( len A) = n by MATRIX_0: 24;

      then

       A4: ( len t) = n by A1;

      

       A5: ( dom t) = ( Seg ( len t)) by FINSEQ_1:def 3;

      ( len ( Col (A,1))) = n by A3, MATRIX_0:def 8;

      then

       A6: ( dom ( Col (A,1))) = ( dom t) by A5, A4, FINSEQ_1:def 3;

      for k be Nat st k in ( dom t) holds (t . k) = (( Col (A,1)) . k)

      proof

        let k be Nat;

        assume

         A7: k in ( dom t);

        then

         A8: 1 <= k & k <= n by A5, A4, FINSEQ_1: 1;

        n >= ( 0 + 1) by A2, INT_1: 7;

        then 1 in ( Seg n);

        then [k, 1] in [:( Seg n), ( Seg n):] by A5, A4, A7, ZFMISC_1:def 2;

        then

         A9: [k, 1] in ( Indices A) by MATRIX_0: 24;

        ( len ( Col (A,1))) = ( len A) by MATRIX_0:def 8;

        then ( dom ( Col (A,1))) = ( Seg ( len A)) by FINSEQ_1:def 3;

        then k in ( dom A) by A6, A7, FINSEQ_1:def 3;

        

        then (( Col (A,1)) . k) = (A * (k,1)) by MATRIX_0:def 8

        .= (t . (((k - 1) mod ( len t)) + 1)) by A1, A9

        .= (t . ((k - 1) + 1)) by A4, A8, Lm1;

        hence thesis;

      end;

      hence thesis by A6, FINSEQ_1: 13;

    end;

    theorem :: MATRIX16:19

    A is col_circulant & [i, j] in [:( Seg n), ( Seg n):] & k = (i + 1) & l = (j + 1) & i < n & j < n implies (A * (i,j)) = (A * (k,l))

    proof

      assume that

       A1: A is col_circulant and

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

       A3: k = (i + 1) and

       A4: l = (j + 1) and

       A5: i < n and

       A6: j < n;

      

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

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

      then 1 <= j by FINSEQ_1: 1;

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

      then

       A8: 1 <= l by A4, XXREAL_0: 2;

      l <= n by A4, A6, INT_1: 7;

      then

       A9: l in ( Seg n) by A8;

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

      then 1 <= i by FINSEQ_1: 1;

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

      then

       A10: 1 <= k by A3, XXREAL_0: 2;

      consider p be FinSequence of D such that ( len p) = ( len A) and

       A11: A is_col_circulant_about p by A1;

      k <= n by A3, A5, INT_1: 7;

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

      then [k, l] in ( Indices A) by A9, ZFMISC_1: 87;

      

      then (A * (k,l)) = (p . (((k - l) mod ( len p)) + 1)) by A11

      .= (p . (((i - j) mod ( len p)) + 1)) by A3, A4

      .= (A * (i,j)) by A11, A7;

      hence thesis;

    end;

    theorem :: MATRIX16:20

    

     Th20: M1 is col_circulant implies (a * M1) is col_circulant

    proof

      

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

      assume M1 is col_circulant;

      then

      consider p be FinSequence of K such that

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

       A3: M1 is_col_circulant_about p;

      

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

      then

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

      

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

      

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

      

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

      proof

        let i,j be Nat;

        assume [i, j] in ( Indices (a * M1));

        then

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

        then

         A10: (((i - j) mod ( len p)) + 1) in ( Seg n) by A2, A1, A4, Lm3;

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

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

        .= ((a multfield ) . (p . (((i - j) mod ( len p)) + 1))) by A3, A9

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

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

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

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

        hence thesis;

      end;

      

       A11: ( len (a * M1)) = n by MATRIX_0: 24;

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

      then (a * M1) is_col_circulant_about (a * p) by A11, A6, A8;

      then

      consider q be FinSequence of K such that

       A12: ( len q) = ( len (a * M1)) & (a * M1) is_col_circulant_about q;

      take q;

      thus thesis by A12;

    end;

    theorem :: MATRIX16:21

    

     Th21: M1 is col_circulant & M2 is col_circulant implies (M1 + M2) is col_circulant

    proof

      assume that

       A1: M1 is col_circulant and

       A2: M2 is col_circulant;

      consider p be FinSequence of K such that

       A3: ( len p) = ( len M1) and

       A4: M1 is_col_circulant_about p by A1;

      

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

      

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

      consider q be FinSequence of K such that

       A7: ( len q) = ( len M2) and

       A8: M2 is_col_circulant_about q by A2;

      

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

      

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

      

       A11: ( len M1) = n by MATRIX_0: 24;

      then

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

      

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

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

      then

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

      then

       A15: ( len (p + q)) = n by A12, FINSEQ_1:def 3;

      

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

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

      proof

        let i,j be Nat;

        assume

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

        then

         A18: (((i - j) mod ( len (p + q))) + 1) in ( Seg n) by A6, A12, A16, A14, Lm3;

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

        .= (the addF of K . ((M1 * (i,j)),(q . (((i - j) mod ( len q)) + 1)))) by A8, A5, A6, A17

        .= (the addF of K . ((p . (((i - j) mod ( len (p + q))) + 1)),(q . (((i - j) mod ( len (p + q))) + 1)))) by A4, A7, A9, A11, A13, A6, A15, A17

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

        hence thesis;

      end;

      then (M1 + M2) is_col_circulant_about (p + q) by A10, A15;

      then

      consider r be FinSequence of K such that

       A19: ( len r) = ( len (M1 + M2)) & (M1 + M2) is_col_circulant_about r;

      take r;

      thus thesis by A19;

    end;

    theorem :: MATRIX16:22

    

     Th22: M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies ((M1 + M2) + M3) is col_circulant

    proof

      assume that

       A1: M1 is col_circulant & M2 is col_circulant and

       A2: M3 is col_circulant;

      (M1 + M2) is col_circulant by A1, Th21;

      hence thesis by A2, Th21;

    end;

    theorem :: MATRIX16:23

    M1 is col_circulant & M2 is col_circulant implies ((a * M1) + (b * M2)) is col_circulant

    proof

      assume M1 is col_circulant & M2 is col_circulant;

      then (a * M1) is col_circulant & (b * M2) is col_circulant by Th20;

      hence thesis by Th21;

    end;

    theorem :: MATRIX16:24

    M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies (((a * M1) + (b * M2)) + (c * M3)) is col_circulant

    proof

      assume that

       A1: M1 is col_circulant & M2 is col_circulant and

       A2: M3 is col_circulant;

      

       A3: (c * M3) is col_circulant by A2, Th20;

      (a * M1) is col_circulant & (b * M2) is col_circulant by A1, Th20;

      hence thesis by A3, Th22;

    end;

    theorem :: MATRIX16:25

    

     Th25: M1 is col_circulant implies ( - M1) is col_circulant

    proof

      

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

      

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

      assume M1 is col_circulant;

      then

      consider p be FinSequence of K such that

       A3: ( len p) = ( len M1) and

       A4: M1 is_col_circulant_about p;

      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: ( len ( - M1)) = n & ( len ( - p)) = ( len p) by CARD_1:def 7, MATRIX_0: 24;

      

       A7: ( len M1) = n by MATRIX_0: 24;

      then

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

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

      proof

        let i,j be Nat;

        assume

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

        then

         A10: (((i - j) mod n) + 1) in ( Seg n) by A2, Lm3;

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A1, A2, A9, MATRIX_3:def 2

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

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

        .= (( - p) . (((i - j) mod ( len p)) + 1)) by A3, A7, A8, A10, FUNCT_1: 13;

        hence thesis by A5, CARD_1:def 7;

      end;

      then ( - M1) is_col_circulant_about ( - p) by A3, A7, A6;

      then

      consider r be FinSequence of K such that

       A11: ( len r) = ( len ( - M1)) & ( - M1) is_col_circulant_about r;

      take r;

      thus thesis by A11;

    end;

    theorem :: MATRIX16:26

    M1 is col_circulant & M2 is col_circulant implies (M1 - M2) is col_circulant

    proof

      assume that

       A1: M1 is col_circulant and

       A2: M2 is col_circulant;

      ( - M2) is col_circulant by A2, Th25;

      hence thesis by A1, Th21;

    end;

    theorem :: MATRIX16:27

    

     Th27: M1 is col_circulant & M2 is col_circulant implies ((a * M1) - (b * M2)) is col_circulant

    proof

      assume that

       A1: M1 is col_circulant and

       A2: M2 is col_circulant;

      (b * M2) is col_circulant by A2, Th20;

      then

       A3: ( - (b * M2)) is col_circulant by Th25;

      (a * M1) is col_circulant by A1, Th20;

      hence thesis by A3, Th21;

    end;

    theorem :: MATRIX16:28

    M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies (((a * M1) + (b * M2)) - (c * M3)) is col_circulant

    proof

      assume that

       A1: M1 is col_circulant & M2 is col_circulant and

       A2: M3 is col_circulant;

      (c * M3) is col_circulant by A2, Th20;

      then

       A3: ( - (c * M3)) is col_circulant by Th25;

      (a * M1) is col_circulant & (b * M2) is col_circulant by A1, Th20;

      then ((a * M1) + (b * M2)) is col_circulant by Th21;

      hence thesis by A3, Th21;

    end;

    theorem :: MATRIX16:29

    M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies (((a * M1) - (b * M2)) - (c * M3)) is col_circulant

    proof

      assume that

       A1: M1 is col_circulant & M2 is col_circulant and

       A2: M3 is col_circulant;

      (c * M3) is col_circulant by A2, Th20;

      then

       A3: ( - (c * M3)) is col_circulant by Th25;

      ((a * M1) - (b * M2)) is col_circulant by A1, Th27;

      hence thesis by A3, Th21;

    end;

    theorem :: MATRIX16:30

    M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies (((a * M1) - (b * M2)) + (c * M3)) is col_circulant

    proof

      assume M1 is col_circulant & M2 is col_circulant & M3 is col_circulant;

      then (c * M3) is col_circulant & ((a * M1) - (b * M2)) is col_circulant by Th20, Th27;

      hence thesis by Th21;

    end;

    theorem :: MATRIX16:31

    

     Th31: p is first-line-of-circulant implies ( - p) is first-line-of-circulant

    proof

      set n = ( len p);

      assume p is first-line-of-circulant;

      then

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

       A1: M1 is_line_circulant_about p;

      set M2 = ( - M1);

      

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

      

       A3: ( 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

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

      then

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

      

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

      

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

      proof

        let i,j be Nat;

        assume

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

        then

         A9: (((j - i) mod n) + 1) in ( Seg n) by A3, Lm3;

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A2, A3, A8, MATRIX_3:def 2

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

        .= (( comp K) . (p . (((j - i) mod ( len p)) + 1))) by A1, A2, A3, A8

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

        hence thesis by A4, CARD_1:def 7;

      end;

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

      then M2 is_line_circulant_about ( - p) by A5, A7;

      then

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

       A10: M2 is_line_circulant_about ( - p) by A5;

      take M2;

      thus thesis by A10;

    end;

    theorem :: MATRIX16:32

    p is first-line-of-circulant implies ( LCirc ( - p)) = ( - ( LCirc p))

    proof

      set n = ( len p);

      

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

      

       A2: ( Indices ( LCirc 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-line-of-circulant;

      then ( - p) is first-line-of-circulant by Th31;

      then

       A5: ( LCirc ( - p)) is_line_circulant_about ( - p) by Def7;

      

       A6: ( LCirc p) is_line_circulant_about p by A4, Def7;

      

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

      proof

        let i,j be Nat;

        assume

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

        then (((j - i) mod n) + 1) in ( Seg n) by A2, Lm3;

        then

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

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

        

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

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

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

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

        hence thesis;

      end;

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

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

    end;

    theorem :: MATRIX16:33

    

     Th33: p is first-line-of-circulant & q is first-line-of-circulant & ( len p) = ( len q) implies (p + q) is first-line-of-circulant

    proof

      set n = ( len p);

      assume that

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

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

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

      consider M2 be Matrix of n, K such that

       A4: M2 is_line_circulant_about q by A2, A3;

      

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

      

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

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

      then

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

      then

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

      consider M1 be Matrix of n, K such that

       A9: M1 is_line_circulant_about p by A1;

      

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

      set M3 = (M1 + M2);

      

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

      

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

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

      proof

        let i,j be Nat;

        assume

         A13: [i, j] in ( Indices (M1 + M2));

        then

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

        then

         A15: (((j - i) mod ( len (p + q))) + 1) in ( dom (p + q)) by A10, A6, A5, A7, Lm3;

        

         A16: [i, j] in ( Indices M2) by A12, A13, MATRIX_0: 24;

        (M3 * (i,j)) = ((M1 * (i,j)) + (M2 * (i,j))) by A14, MATRIX_3:def 3

        .= (the addF of K . ((M1 * (i,j)),(q . (((j - i) mod ( len q)) + 1)))) by A4, A16

        .= (the addF of K . ((p . (((j - i) mod ( len (p + q))) + 1)),(q . (((j - i) mod ( len (p + q))) + 1)))) by A3, A9, A8, A14

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

        hence thesis;

      end;

      then (M1 + M2) is_line_circulant_about (p + q) by A11, A8;

      then

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

       A17: M3 is_line_circulant_about (p + q) by A11;

      take M3;

      thus thesis by A17;

    end;

    theorem :: MATRIX16:34

    

     Th34: ( len p) = ( len q) & p is first-line-of-circulant & q is first-line-of-circulant implies ( LCirc (p + q)) = (( LCirc p) + ( LCirc q))

    proof

      set n = ( len p);

      assume that

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

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

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

      

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

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

      then

       A5: ( LCirc (p + q)) is_line_circulant_about (p + q) by Def7;

      

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

      

       A7: ( LCirc p) is_line_circulant_about p by A2, Def7;

      

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

      

       A9: ( Indices ( LCirc 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 ( LCirc p)) = ( Indices ( LCirc (p + q))) by MATRIX_0: 26;

      

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

      proof

        let i,j be Nat;

        assume

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

        then

         A14: (((j - i) mod n) + 1) in ( Seg n) by A9, Lm3;

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

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

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

        .= ((( LCirc p) * (i,j)) + (( LCirc q) * (i,j))) by A4, A13;

        hence thesis;

      end;

      

       A15: ( len ( LCirc p)) = ( len p) & ( width ( LCirc p)) = ( len p) by MATRIX_0: 24;

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

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

    end;

    theorem :: MATRIX16:35

    

     Th35: p is first-col-of-circulant implies ( - p) is first-col-of-circulant

    proof

      set n = ( len p);

      assume p is first-col-of-circulant;

      then

      consider M1 be Matrix of n, K such that

       A1: M1 is_col_circulant_about p;

      set M2 = ( - M1);

      

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

      

       A3: ( 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

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

      then

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

      

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

      

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

      proof

        let i,j be Nat;

        assume

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

        then

         A9: (((i - j) mod n) + 1) in ( Seg n) by A3, Lm3;

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A2, A3, A8, MATRIX_3:def 2

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

        .= (( comp K) . (p . (((i - j) mod ( len p)) + 1))) by A1, A2, A3, A8

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

        hence thesis by A4, CARD_1:def 7;

      end;

      ( len ( - M1)) = n by MATRIX_0: 24;

      then M2 is_col_circulant_about ( - p) by A5, A7;

      then

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

       A10: M2 is_col_circulant_about ( - p) by A5;

      take M2;

      thus thesis by A10;

    end;

    theorem :: MATRIX16:36

    for p be FinSequence of K st p is first-col-of-circulant holds ( CCirc ( - p)) = ( - ( CCirc p))

    proof

      let p;

      set n = ( len p);

      

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

      

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

      assume

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

      then

       A4: ( CCirc p) is_col_circulant_about p by Def8;

      ( - p) is first-col-of-circulant by A3, Th35;

      then

       A5: ( CCirc ( - p)) is_col_circulant_about ( - p) by Def8;

      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

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

      then

       A7: ( Indices ( CCirc p)) = ( Indices ( CCirc ( - p))) by MATRIX_0: 26;

      

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

      proof

        let i,j be Nat;

        assume

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

        then

         A10: (((i - j) mod n) + 1) in ( Seg n) by A2, Lm3;

        (( CCirc ( - p)) * (i,j)) = (( - p) . (((i - j) mod ( len ( - p))) + 1)) by A5, A7, A9

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

        .= (( comp K) . (( CCirc p) * (i,j))) by A4, A9

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

        hence thesis;

      end;

      

       A11: ( len ( CCirc p)) = ( len p) & ( width ( CCirc p)) = ( len p) by MATRIX_0: 24;

      ( len ( CCirc ( - p))) = ( len p) & ( width ( CCirc ( - p))) = ( len p) by A6, MATRIX_0: 24;

      hence thesis by A11, A8, MATRIX_3:def 2;

    end;

    theorem :: MATRIX16:37

    

     Th37: p is first-col-of-circulant & q is first-col-of-circulant & ( len p) = ( len q) implies (p + q) is first-col-of-circulant

    proof

      set n = ( len p);

      assume that

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

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

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

      consider M2 be Matrix of n, K such that

       A4: M2 is_col_circulant_about q by A2, A3;

      

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

      

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

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

      then

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

      then

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

      consider M1 be Matrix of n, K such that

       A9: M1 is_col_circulant_about p by A1;

      

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

      set M3 = (M1 + M2);

      

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

      

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

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

      proof

        let i,j be Nat;

        assume

         A13: [i, j] in ( Indices (M1 + M2));

        then

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

        then

         A15: (((i - j) mod ( len (p + q))) + 1) in ( dom (p + q)) by A10, A6, A5, A7, Lm3;

        

         A16: [i, j] in ( Indices M2) by A12, A13, MATRIX_0: 24;

        (M3 * (i,j)) = ((M1 * (i,j)) + (M2 * (i,j))) by A14, MATRIX_3:def 3

        .= (the addF of K . ((M1 * (i,j)),(q . (((i - j) mod ( len q)) + 1)))) by A4, A16

        .= (the addF of K . ((p . (((i - j) mod ( len (p + q))) + 1)),(q . (((i - j) mod ( len (p + q))) + 1)))) by A3, A9, A8, A14

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

        hence thesis;

      end;

      then (M1 + M2) is_col_circulant_about (p + q) by A11, A8;

      then

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

       A17: M3 is_col_circulant_about (p + q) by A11;

      take M3;

      thus thesis by A17;

    end;

    theorem :: MATRIX16:38

    

     Th38: ( len p) = ( len q) & p is first-col-of-circulant & q is first-col-of-circulant implies ( CCirc (p + q)) = (( CCirc p) + ( CCirc q))

    proof

      set n = ( len p);

      assume that

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

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

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

      

       A4: ( CCirc q) is_col_circulant_about q & ( Indices ( CCirc p)) = ( Indices ( CCirc q)) by A1, A3, Def8, MATRIX_0: 26;

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

      then

       A5: ( CCirc (p + q)) is_col_circulant_about (p + q) by Def8;

      

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

      

       A7: ( CCirc p) is_col_circulant_about p by A2, Def8;

      

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

      

       A9: ( Indices ( CCirc 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 ( CCirc p)) = ( Indices ( CCirc (p + q))) by MATRIX_0: 26;

      

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

      proof

        let i,j be Nat;

        assume

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

        then

         A14: (((i - j) mod n) + 1) in ( Seg n) by A9, Lm3;

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

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

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

        .= ((( CCirc p) * (i,j)) + (( CCirc q) * (i,j))) by A4, A13;

        hence thesis;

      end;

      

       A15: ( len ( CCirc p)) = ( len p) & ( width ( CCirc p)) = ( len p) by MATRIX_0: 24;

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

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

    end;

    theorem :: MATRIX16:39

    n > 0 implies ( 1. (K,n)) is col_circulant

    proof

      assume

       A1: n > 0 ;

      set M1 = ( 1. (K,n));

      

       A2: ( Indices ( 1. (K,n))) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      set p = ( Col (M1,1));

      

       A3: ( len ( 1. (K,n))) = n by MATRIX_0: 24;

      then

       A4: ( len p) = n by MATRIX_0:def 8;

      

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

      

       A6: ( width ( 1. (K,n))) = n by MATRIX_0: 24;

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

      proof

        let i,j be Nat;

        

         A7: ((i - j) mod n) >= 0 by A1, NAT_D: 62;

        then

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

        assume

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

        then

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

        then

         A11: 1 <= j by FINSEQ_1: 1;

        

         A12: j <= n by A10, FINSEQ_1: 1;

        

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

        then 1 <= i by FINSEQ_1: 1;

        then

         A14: (1 - n) <= (i - j) by A12, XREAL_1: 13;

        ( - n) <= (( - n) + 1) by XREAL_1: 29;

        then

         A15: ( - n) <= (i - j) by A14, XXREAL_0: 2;

        i <= n by A13, FINSEQ_1: 1;

        then

         A16: (i - j) <= (n - 1) by A11, XREAL_1: 13;

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

        then

         A17: (i - j) < n by A16, XXREAL_0: 2;

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

        proof

          per cases ;

            suppose 0 <= (i - j);

            hence thesis by A16, A17, NAT_D: 63;

          end;

            suppose

             A18: 0 > (i - j);

            then (i - j) <= ( - 1) by INT_1: 8;

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

            hence thesis by A15, A18, NAT_D: 63;

          end;

        end;

        then

         A19: (((i - j) mod n) + 1) <= ((n - 1) + 1) by XREAL_1: 6;

        (((i - j) mod n) + 1) >= ( 0 + 1) by A7, XREAL_1: 6;

        then

         A20: (((i - j) mod n) + 1) in ( Seg n) by A19, A8;

        then

         A21: (((i - j) mod ( len p)) + 1) in ( Seg n) by A3, MATRIX_0:def 8;

        (M1 * (i,j)) = (p . (((i - j) mod ( len p)) + 1))

        proof

          per cases ;

            suppose

             A22: i = j;

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

            then 1 in ( Seg n);

            then

             A23: [1, 1] in ( Indices M1) by A2, ZFMISC_1: 87;

            ((i - j) mod ( len p)) = 0 by A1, A4, A22, NAT_D: 63;

            

            then (p . (((i - j) mod ( len p)) + 1)) = (M1 * (1,1)) by A5, A21, MATRIX_0:def 8

            .= ( 1_ K) by A23, MATRIX_1:def 3;

            hence thesis by A9, A22, MATRIX_1:def 3;

          end;

            suppose

             A24: i <> j;

            then

             A25: (i - j) <> 0 ;

            ((i - j) mod n) <> 0

            proof

              per cases ;

                suppose 0 <= (i - j);

                hence thesis by A17, A25, NAT_D: 63;

              end;

                suppose

                 A26: 0 > (i - j);

                ((1 - n) + n) <= ((i - j) + n) by A14, XREAL_1: 6;

                hence thesis by A15, A26, NAT_D: 63;

              end;

            end;

            then

             A27: (((i - j) mod ( len p)) + 1) <> 1 by A3, MATRIX_0:def 8;

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

            reconsider l as Nat by A3, A8, MATRIX_0:def 8;

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

            then

             A28: 1 in ( Seg n);

            l in ( dom M1) by A3, A4, A20, FINSEQ_1:def 3;

            then

             A29: [l, 1] in ( Indices M1) by A6, A28, ZFMISC_1: 87;

            (p . l) = (M1 * (l,1)) by A5, A21, MATRIX_0:def 8

            .= ( 0. K) by A27, A29, MATRIX_1:def 3;

            hence thesis by A9, A24, MATRIX_1:def 3;

          end;

        end;

        hence thesis;

      end;

      then M1 is_col_circulant_about p by A3, A4;

      then

      consider p be FinSequence of K such that

       A30: ( len p) = ( len M1) & M1 is_col_circulant_about p;

      take p;

      thus thesis by A30;

    end;

    theorem :: MATRIX16:40

    n > 0 implies ( 1. (K,n)) is line_circulant

    proof

      set M1 = ( 1. (K,n));

      set p = ( Line (M1,1));

      assume

       A1: n > 0 ;

      

       A2: ( Indices ( 1. (K,n))) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width ( 1. (K,n))) = n by MATRIX_0: 24;

      then

       A4: ( len p) = n by MATRIX_0:def 7;

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

      proof

        let i,j be Nat;

        

         A5: ((j - i) mod n) >= 0 by A1, NAT_D: 62;

        then

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

        assume

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

        then

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

        then

         A9: 1 <= j by FINSEQ_1: 1;

        

         A10: j <= n by A8, FINSEQ_1: 1;

        

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

        then 1 <= i by FINSEQ_1: 1;

        then

         A12: (j - i) <= (n - 1) by A10, XREAL_1: 13;

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

        then

         A13: (j - i) < n by A12, XXREAL_0: 2;

        i <= n by A11, FINSEQ_1: 1;

        then

         A14: (1 - n) <= (j - i) by A9, XREAL_1: 13;

        ( - n) <= (( - n) + 1) by XREAL_1: 29;

        then

         A15: ( - n) <= (j - i) by A14, XXREAL_0: 2;

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

        proof

          per cases ;

            suppose 0 <= (j - i);

            hence thesis by A12, A13, NAT_D: 63;

          end;

            suppose

             A16: 0 > (j - i);

            then (j - i) <= ( - 1) by INT_1: 8;

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

            hence thesis by A15, A16, NAT_D: 63;

          end;

        end;

        then

         A17: (((j - i) mod n) + 1) <= ((n - 1) + 1) by XREAL_1: 6;

        (((j - i) mod n) + 1) >= ( 0 + 1) by A5, XREAL_1: 6;

        then

         A18: (((j - i) mod n) + 1) in ( Seg n) by A17, A6;

        then

         A19: (((j - i) mod ( len p)) + 1) in ( Seg n) by A3, MATRIX_0:def 7;

        (M1 * (i,j)) = (p . (((j - i) mod ( len p)) + 1))

        proof

          per cases ;

            suppose

             A20: i = j;

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

            then 1 in ( Seg n);

            then

             A21: [1, 1] in ( Indices M1) by A2, ZFMISC_1: 87;

            ((j - i) mod ( len p)) = 0 by A1, A4, A20, NAT_D: 63;

            

            then (p . (((j - i) mod ( len p)) + 1)) = (M1 * (1,1)) by A3, A19, MATRIX_0:def 7

            .= ( 1_ K) by A21, MATRIX_1:def 3;

            hence thesis by A7, A20, MATRIX_1:def 3;

          end;

            suppose

             A22: i <> j;

            ((j - i) mod n) <> 0

            proof

              per cases ;

                suppose 0 <= (j - i);

                then ((j - i) mod n) = (j - i) by A13, NAT_D: 63;

                hence thesis by A22;

              end;

                suppose

                 A23: 0 > (j - i);

                ((1 - n) + n) <= ((j - i) + n) by A14, XREAL_1: 6;

                hence thesis by A15, A23, NAT_D: 63;

              end;

            end;

            then

             A24: (((j - i) mod ( len p)) + 1) <> 1 by A3, MATRIX_0:def 7;

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

            reconsider l as Nat by A3, A6, MATRIX_0:def 7;

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

            then

             A25: 1 in ( Seg n);

            l in ( Seg n) by A3, A18, MATRIX_0:def 7;

            then

             A26: [1, l] in ( Indices M1) by A2, A25, ZFMISC_1: 87;

            (p . l) = (M1 * (1,l)) by A3, A19, MATRIX_0:def 7

            .= ( 0. K) by A24, A26, MATRIX_1:def 3;

            hence thesis by A7, A22, MATRIX_1:def 3;

          end;

        end;

        hence thesis;

      end;

      then M1 is_line_circulant_about p by A3, A4;

      then

      consider p be FinSequence of K such that

       A27: ( len p) = ( width M1) & M1 is_line_circulant_about p;

      take p;

      thus thesis by A27;

    end;

    theorem :: MATRIX16:41

    

     Th41: p is first-line-of-circulant implies (a * p) is first-line-of-circulant

    proof

      set n = ( len p);

      

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

      assume p is first-line-of-circulant;

      then

      consider M1 be Matrix of n, K such that

       A2: M1 is_line_circulant_about p;

      

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

      

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

      

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

      

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

      proof

        let i,j be Nat;

        assume

         A7: [i, j] in ( Indices (a * M1));

        then

         A8: (((j - i) mod n) + 1) in ( Seg n) by A3, Lm3;

        then

         A9: (((j - i) mod ( len p)) + 1) in ( dom (a * p)) by A5, MATRIXR1: 16;

        

         A10: [i, j] in ( Indices M1) by A3, A7, 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 . (((j - i) mod ( len p)) + 1))) by A2, A10

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

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

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

        .= ((a * p) . (((j - i) mod ( len p)) + 1)) by A9, PARTFUN1:def 6;

        hence thesis by MATRIXR1: 16;

      end;

      ( width (a * M1)) = n by MATRIX_0: 24;

      then (a * M1) is_line_circulant_about (a * p) by A1, A6;

      then

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

       A11: M2 is_line_circulant_about (a * p) by A1;

      take M2;

      thus thesis by A11;

    end;

    theorem :: MATRIX16:42

    

     Th42: p is first-line-of-circulant implies ( LCirc (a * p)) = (a * ( LCirc p))

    proof

      set n = ( len p);

      

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

      assume

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

      then (a * p) is first-line-of-circulant by Th41;

      then

       A3: ( LCirc (a * p)) is_line_circulant_about (a * p) by Def7;

      

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

      

       A5: ( LCirc p) is_line_circulant_about p by A2, Def7;

      

       A6: for i,j be Nat st [i, j] in ( Indices ( LCirc p)) holds (( LCirc (a * p)) * (i,j)) = (a * (( LCirc 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 ( LCirc p));

        then

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

        

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

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

        

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

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

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

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

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

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

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

        hence thesis;

      end;

      

       A11: ( len ( LCirc p)) = ( len p) & ( width ( LCirc p)) = ( len p) by MATRIX_0: 24;

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

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

    end;

    theorem :: MATRIX16:43

    p is first-line-of-circulant implies ((a * ( LCirc p)) + (b * ( LCirc p))) = ( LCirc ((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-line-of-circulant;

      then

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

      (a * ( LCirc p)) = ( LCirc (a * p)) & (b * ( LCirc p)) = ( LCirc (b * p)) by A3, Th42;

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

      hence thesis by A2, FVSUM_1: 55;

    end;

    theorem :: MATRIX16:44

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

    proof

      assume that

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

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

      

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

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

      

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

      .= (a * ( LCirc (p + q))) by A1, A2, Th34

      .= ( LCirc (a * (p + q))) by A1, A2, Th33, Th42;

      hence thesis;

    end;

    theorem :: MATRIX16:45

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

    proof

      set n = ( len p);

      assume that

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

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

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

      

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

      

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

      ((a * ( LCirc p)) + (b * ( LCirc q))) = (( LCirc (a * p)) + (b * ( LCirc q))) by A1, Th42

      .= (( LCirc (a * p)) + ( LCirc (b * q))) by A2, Th42

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

      hence thesis;

    end;

    theorem :: MATRIX16:46

    

     Th46: p is first-col-of-circulant implies (a * p) is first-col-of-circulant

    proof

      set n = ( len p);

      

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

      assume p is first-col-of-circulant;

      then

      consider M1 be Matrix of n, K such that

       A2: M1 is_col_circulant_about p;

      

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

      

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

      

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

      

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

      proof

        let i,j be Nat;

        assume

         A7: [i, j] in ( Indices (a * M1));

        then

         A8: (((i - j) mod n) + 1) in ( Seg n) by A3, Lm3;

        then

         A9: (((i - j) mod ( len p)) + 1) in ( dom (a * p)) by A5, MATRIXR1: 16;

        

         A10: [i, j] in ( Indices M1) by A3, A7, 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) mod ( len p)) + 1))) by A2, A10

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

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

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

        .= ((a * p) . (((i - j) mod ( len p)) + 1)) by A9, PARTFUN1:def 6;

        hence thesis by MATRIXR1: 16;

      end;

      ( len (a * M1)) = n by MATRIX_0: 24;

      then (a * M1) is_col_circulant_about (a * p) by A1, A6;

      then

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

       A11: M2 is_col_circulant_about (a * p) by A1;

      take M2;

      thus thesis by A11;

    end;

    theorem :: MATRIX16:47

    

     Th47: p is first-col-of-circulant implies ( CCirc (a * p)) = (a * ( CCirc p))

    proof

      set n = ( len p);

      

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

      assume

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

      then (a * p) is first-col-of-circulant by Th46;

      then

       A3: ( CCirc (a * p)) is_col_circulant_about (a * p) by Def8;

      

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

      

       A5: ( CCirc p) is_col_circulant_about p by A2, Def8;

      

       A6: for i,j be Nat st [i, j] in ( Indices ( CCirc p)) holds (( CCirc (a * p)) * (i,j)) = (a * (( CCirc 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 ( CCirc p));

        then

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

        

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

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

        

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

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

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

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

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

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

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

        hence thesis;

      end;

      

       A11: ( len ( CCirc p)) = ( len p) & ( width ( CCirc p)) = ( len p) by MATRIX_0: 24;

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

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

    end;

    theorem :: MATRIX16:48

    p is first-col-of-circulant implies ((a * ( CCirc p)) + (b * ( CCirc p))) = ( CCirc ((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-col-of-circulant;

      then

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

      (a * ( CCirc p)) = ( CCirc (a * p)) & (b * ( CCirc p)) = ( CCirc (b * p)) by A3, Th47;

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

      hence thesis by A2, FVSUM_1: 55;

    end;

    theorem :: MATRIX16:49

    p is first-col-of-circulant & q is first-col-of-circulant & ( len p) = ( len q) & ( len p) > 0 implies ((a * ( CCirc p)) + (a * ( CCirc q))) = ( CCirc (a * (p + q)))

    proof

      assume that

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

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

      

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

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

      

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

      .= (a * ( CCirc (p + q))) by A1, A2, Th38

      .= ( CCirc (a * (p + q))) by A1, A2, Th37, Th47;

      hence thesis;

    end;

    theorem :: MATRIX16:50

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

    proof

      set n = ( len p);

      assume that

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

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

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

      

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

      

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

      ((a * ( CCirc p)) + (b * ( CCirc q))) = (( CCirc (a * p)) + (b * ( CCirc q))) by A1, Th47

      .= (( CCirc (a * p)) + ( CCirc (b * q))) by A2, Th47

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

      hence thesis;

    end;

    notation

      let K be set;

      let M be Matrix of K;

      synonym M is circulant for M is line_circulant;

    end

    begin

    definition

      let K be Field;

      let M1 be Matrix of K;

      let p be FinSequence of K;

      :: MATRIX16:def9

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

    end

    definition

      let K be Field;

      let M be Matrix of K;

      :: MATRIX16:def10

      attr M is anti-circular means ex p be FinSequence of K st ( len p) = ( width M) & M is_anti-circular_about p;

    end

    definition

      let K be Field;

      let p be FinSequence of K;

      :: MATRIX16:def11

      attr p is first-line-of-anti-circular means ex M be Matrix of ( len p), K st M is_anti-circular_about p;

    end

    definition

      let K be Field, p be FinSequence of K;

      assume

       A1: p is first-line-of-anti-circular;

      :: MATRIX16:def12

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

      : Def12: it is_anti-circular_about p;

      existence by A1;

      uniqueness

      proof

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

        assume that

         A2: M1 is_anti-circular_about p and

         A3: M2 is_anti-circular_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;

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

            hence thesis by A3, A4, A5, A6;

          end;

            suppose

             A7: i > j;

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

            hence thesis by A3, A4, A5, A7;

          end;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    theorem :: MATRIX16:51

    M1 is anti-circular implies (a * M1) is anti-circular

    proof

      

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

      assume M1 is anti-circular;

      then

      consider p be FinSequence of K such that

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

       A3: M1 is_anti-circular_about p;

      

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

      proof

        let i,j be Nat;

        assume that

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

         A9: i <= j;

        

         A10: (((j - i) mod n) + 1) in ( Seg n) by A1, A8, Lm3;

        then

         A11: (((j - i) mod ( len p)) + 1) in ( dom (a * p)) by A2, A4, A6, MATRIXR1: 16;

        

         A12: [i, j] in ( Indices M1) by A1, A8, 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 . (((j - i) mod ( len p)) + 1))) by A3, A9, A12

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

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

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

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

        hence thesis by MATRIXR1: 16;

      end;

      

       A13: ( width (a * M1)) = n by MATRIX_0: 24;

      

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

      

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

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

      proof

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

        

        then

         A16: ( dom (a * ( - p))) = ( Seg ( len ( - p))) by FINSEQ_1:def 3

        .= ( dom ( - p)) by FINSEQ_1:def 3;

        

         A17: (a * p) is Element of (n -tuples_on the carrier of K) by A15, A14, FINSEQ_2: 92;

        let i,j be Nat;

        assume that

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

         A19: i >= j;

        

         A20: (((j - i) mod n) + 1) in ( Seg n) by A1, A18, Lm3;

        

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

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

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

        then

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

        

         A23: [i, j] in ( Indices M1) by A1, A18, 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) . (((j - i) mod ( len p)) + 1))) by A3, A19, A23

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

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

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

        .= ((a * ( - p)) . (((j - i) mod ( len p)) + 1)) by A2, A4, A20, A22, A16, PARTFUN1:def 6

        .= ((a * (( - ( 1_ K)) * p)) . (((j - i) mod ( len p)) + 1)) by A21, FVSUM_1: 59

        .= (((a * ( - ( 1_ K))) * p) . (((j - i) mod ( len p)) + 1)) by A21, FVSUM_1: 54

        .= ((( - (a * ( 1_ K))) * p) . (((j - i) mod ( len p)) + 1)) by VECTSP_1: 8

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

        .= ((( - (( 1_ K) * a)) * p) . (((j - i) mod ( len p)) + 1))

        .= (((( - ( 1_ K)) * a) * p) . (((j - i) mod ( len p)) + 1)) by VECTSP_1: 9

        .= ((( - ( 1_ K)) * (a * p)) . (((j - i) mod ( len p)) + 1)) by A21, FVSUM_1: 54

        .= (( - (a * p)) . (((j - i) mod ( len p)) + 1)) by A17, FVSUM_1: 59;

        hence thesis by MATRIXR1: 16;

      end;

      then (a * M1) is_anti-circular_about (a * p) by A13, A15, A14, A7;

      then

      consider q be FinSequence of K such that

       A24: ( len q) = ( width (a * M1)) & (a * M1) is_anti-circular_about q;

      take q;

      thus thesis by A24;

    end;

    theorem :: MATRIX16:52

    

     Th52: M1 is anti-circular & M2 is anti-circular implies (M1 + M2) is anti-circular

    proof

      assume that

       A1: M1 is anti-circular and

       A2: M2 is anti-circular;

      consider p be FinSequence of K such that

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

       A4: M1 is_anti-circular_about p by A1;

      

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

      then

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

      consider q be FinSequence of K such that

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

       A8: M2 is_anti-circular_about q by A2;

      

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

      

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

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

      then

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

      then

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

      

       A13: 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 ( len ( - p)) = ( len p) by CARD_1:def 7;

      then

       A14: ( dom ( - p)) = ( Seg n) by A3, A5, FINSEQ_1:def 3;

      

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

      

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

      

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

      

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

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

      then ( len ( - q)) = ( len q) by CARD_1:def 7;

      then

       A19: ( dom ( - q)) = ( Seg n) by A7, A10, FINSEQ_1:def 3;

      

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

      proof

        let i,j be Nat;

        assume that

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

         A22: i >= j;

        ( dom (( - p) + ( - q))) = ( dom ( - p)) by A14, A19, POLYNOM1: 1;

        then

         A23: (((j - i) mod ( len (p + q))) + 1) in ( dom (( - p) + ( - q))) by A16, A6, A9, A14, A11, A21, Lm3;

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

        .= (the addF of K . ((M1 * (i,j)),(( - q) . (((j - i) mod ( len q)) + 1)))) by A8, A15, A16, A21, A22

        .= (the addF of K . ((( - p) . (((j - i) mod ( len (p + q))) + 1)),(( - q) . (((j - i) mod ( len (p + q))) + 1)))) by A4, A7, A17, A5, A10, A16, A12, A21, A22

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

        .= (( - (p + q)) . (((j - i) mod ( len (p + q))) + 1)) by A3, A7, A13, A18, A5, A10, FVSUM_1: 31;

        hence thesis;

      end;

      

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

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

      proof

        let i,j be Nat;

        assume that

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

         A26: i <= j;

        

         A27: (((j - i) mod ( len (p + q))) + 1) in ( dom (p + q)) by A16, A6, A9, A11, A25, Lm3;

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

        .= (the addF of K . ((M1 * (i,j)),(q . (((j - i) mod ( len q)) + 1)))) by A8, A15, A16, A25, A26

        .= (the addF of K . ((p . (((j - i) mod ( len (p + q))) + 1)),(q . (((j - i) mod ( len (p + q))) + 1)))) by A4, A7, A17, A5, A10, A16, A12, A25, A26

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

        hence thesis;

      end;

      then (M1 + M2) is_anti-circular_about (p + q) by A24, A12, A20;

      then

      consider r be FinSequence of K such that

       A28: ( len r) = ( width (M1 + M2)) & (M1 + M2) is_anti-circular_about r;

      take r;

      thus thesis by A28;

    end;

    theorem :: MATRIX16:53

    for K be Fanoian Field, n,i,j be Nat, M1 be Matrix of n, K st [i, j] in ( Indices M1) & i = j & M1 is anti-circular holds (M1 * (i,j)) = ( 0. K)

    proof

      let K be Fanoian Field;

      let n,i,j be Nat;

      let M1 be Matrix of n, K;

      assume that

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

       A2: i = j and

       A3: M1 is anti-circular;

      consider p be FinSequence of K such that

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

       A5: M1 is_anti-circular_about p by A3;

      

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

      

       A7: ( width M1) = 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 ( len ( - p)) = ( len p) by CARD_1:def 7;

      then ( Indices M1) = [:( Seg n), ( Seg n):] & ( dom ( - p)) = ( Seg n) by A4, A7, FINSEQ_1:def 3, MATRIX_0: 24;

      then

       A8: (((j - i) mod ( len p)) + 1) in ( dom ( - p)) by A1, A4, A7, Lm3;

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

      .= (( comp K) . (p . (((j - i) mod ( len p)) + 1))) by A8, FUNCT_1: 12

      .= ( - (M1 * (i,j))) by A6, VECTSP_1:def 13;

      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;

    theorem :: MATRIX16:54

    M1 is anti-circular & [i, j] in [:( Seg n), ( Seg n):] & k = (i + 1) & l = (j + 1) & i < n & j < n implies (M1 * (k,l)) = (M1 * (i,j))

    proof

      now

        per cases ;

          case

           A1: i <= j;

          then

           A2: (i + 1) <= (j + 1) by XREAL_1: 6;

          

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

          assume that

           A4: M1 is anti-circular and

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

           A6: k = (i + 1) and

           A7: l = (j + 1) and

           A8: i < n and

           A9: j < n;

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

          then 1 <= j by FINSEQ_1: 1;

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

          then

           A10: 1 <= (j + 1) by XXREAL_0: 2;

          (j + 1) <= n by A9, INT_1: 7;

          then

           A11: l in ( Seg n) by A7, A10;

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

          then 1 <= i by FINSEQ_1: 1;

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

          then

           A12: 1 <= (i + 1) by XXREAL_0: 2;

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

           A13: M1 is_anti-circular_about p by A4;

          (i + 1) <= n by A8, INT_1: 7;

          then k in ( Seg n) by A6, A12;

          then [k, l] in ( Indices M1) by A3, A11, ZFMISC_1: 87;

          

          then (M1 * (k,l)) = (p . (((l - k) mod ( len p)) + 1)) by A6, A7, A13, A2

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

          .= (M1 * (i,j)) by A1, A5, A13, A3;

          hence thesis;

        end;

          case

           A14: i >= j;

          then

           A15: (i + 1) >= (j + 1) by XREAL_1: 6;

          

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

          assume that

           A17: M1 is anti-circular and

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

           A19: k = (i + 1) and

           A20: l = (j + 1) and

           A21: i < n and

           A22: j < n;

          j in ( Seg n) by A18, ZFMISC_1: 87;

          then 1 <= j by FINSEQ_1: 1;

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

          then

           A23: 1 <= (j + 1) by XXREAL_0: 2;

          (j + 1) <= n by A22, INT_1: 7;

          then

           A24: l in ( Seg n) by A20, A23;

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

          then 1 <= i by FINSEQ_1: 1;

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

          then

           A25: 1 <= (i + 1) by XXREAL_0: 2;

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

           A26: M1 is_anti-circular_about p by A17;

          (i + 1) <= n by A21, INT_1: 7;

          then k in ( Seg n) by A19, A25;

          then [k, l] in ( Indices M1) by A16, A24, ZFMISC_1: 87;

          

          then (M1 * (k,l)) = (( - p) . (((l - k) mod ( len p)) + 1)) by A19, A20, A26, A15

          .= (( - p) . (((j - i) mod ( len p)) + 1)) by A19, A20

          .= (M1 * (i,j)) by A14, A18, A26, A16;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX16:55

    

     Th55: M1 is anti-circular implies ( - M1) is anti-circular

    proof

      

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

      assume M1 is anti-circular;

      then

      consider p be FinSequence of K such that

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

       A3: M1 is_anti-circular_about p;

      set r = ( - p);

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

      then

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

      

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

      

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

      

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

      proof

        let i,j be Nat;

        assume that

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

         A9: i <= j;

        (((j - i) mod n) + 1) in ( Seg n) by A5, A8, Lm3;

        then

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

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A1, A5, A8, MATRIX_3:def 2

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

        .= (( comp K) . (p . (((j - i) mod ( len p)) + 1))) by A3, A1, A5, A8, A9

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

        hence thesis by A4, CARD_1:def 7;

      end;

      

       A11: ( width ( - M1)) = n by MATRIX_0: 24;

      

       A12: ( len ( - p)) = ( len p) by A4, CARD_1:def 7;

      then

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

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

      proof

        let i,j be Nat;

        assume that

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

         A15: i >= j;

        

         A16: (((j - i) mod n) + 1) in ( Seg n) by A5, A14, Lm3;

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A1, A5, A14, MATRIX_3:def 2

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

        .= (( comp K) . (( - p) . (((j - i) mod ( len p)) + 1))) by A3, A1, A5, A14, A15

        .= (( - ( - p)) . (((j - i) mod ( len p)) + 1)) by A2, A6, A13, A16, FUNCT_1: 13;

        hence thesis by A4, CARD_1:def 7;

      end;

      then ( - M1) is_anti-circular_about r by A2, A6, A11, A12, A7;

      then

      consider r be FinSequence of K such that

       A17: ( len r) = ( width ( - M1)) & ( - M1) is_anti-circular_about r;

      take r;

      thus thesis by A17;

    end;

    theorem :: MATRIX16:56

    M1 is anti-circular & M2 is anti-circular implies (M1 - M2) is anti-circular

    proof

      assume that

       A1: M1 is anti-circular and

       A2: M2 is anti-circular;

      ( - M2) is anti-circular by A2, Th55;

      hence thesis by A1, Th52;

    end;

    theorem :: MATRIX16:57

    M1 is_anti-circular_about p & n > 0 implies p = ( Line (M1,1))

    proof

      assume that

       A1: M1 is_anti-circular_about p and

       A2: n > 0 ;

      

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

      

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

      then

       A5: ( len p) = n by A1;

      

       A6: for k be Nat st k in ( dom p) holds (p . k) = (( Line (M1,1)) . k)

      proof

        let k be Nat;

        assume

         A7: k in ( dom p);

        then

         A8: 1 <= k by A3, FINSEQ_1: 1;

        n >= ( 0 + 1) by A2, INT_1: 7;

        then 1 in ( Seg n);

        then [1, k] in [:( Seg n), ( Seg n):] by A3, A5, A7, ZFMISC_1:def 2;

        then

         A9: [1, k] in ( Indices M1) by MATRIX_0: 24;

        

         A10: k <= n by A3, A5, A7, FINSEQ_1: 1;

        (( Line (M1,1)) . k) = (M1 * (1,k)) by A4, A3, A5, A7, MATRIX_0:def 7

        .= (p . (((k - 1) mod ( len p)) + 1)) by A1, A8, A9

        .= (p . (((k - 1) mod n) + 1)) by A1, A4

        .= (p . ((k - 1) + 1)) by A8, A10, Lm1;

        hence thesis;

      end;

      ( len ( Line (M1,1))) = n by A4, MATRIX_0:def 7;

      then ( dom ( Line (M1,1))) = ( dom p) by A3, A5, FINSEQ_1:def 3;

      hence thesis by A6, FINSEQ_1: 13;

    end;

    theorem :: MATRIX16:58

    

     Th58: p is first-line-of-anti-circular implies ( - p) is first-line-of-anti-circular

    proof

      set n = ( len p);

      assume p is first-line-of-anti-circular;

      then

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

       A1: M1 is_anti-circular_about p;

      set M2 = ( - M1);

      

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

      

       A3: ( 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

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

      then

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

      then

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

      

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

      proof

        let i,j be Nat;

        assume that

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

         A9: i >= j;

        

         A10: (((j - i) mod n) + 1) in ( Seg n) by A3, A8, Lm3;

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A2, A3, A8, MATRIX_3:def 2

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

        .= (( comp K) . (( - p) . (((j - i) mod ( len p)) + 1))) by A1, A2, A3, A8, A9

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

        hence thesis by A4, CARD_1:def 7;

      end;

      

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

      proof

        let i,j be Nat;

        assume that

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

         A13: i <= j;

        (((j - i) mod n) + 1) in ( Seg n) by A3, A12, Lm3;

        then

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

        (( - M1) * (i,j)) = ( - (M1 * (i,j))) by A2, A3, A12, MATRIX_3:def 2

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

        .= (( comp K) . (p . (((j - i) mod ( len p)) + 1))) by A1, A2, A3, A12, A13

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

        hence thesis by A4, CARD_1:def 7;

      end;

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

      then M2 is_anti-circular_about ( - p) by A5, A11, A7;

      then

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

       A15: M2 is_anti-circular_about ( - p) by A5;

      take M2;

      thus thesis by A15;

    end;

    theorem :: MATRIX16:59

    p is first-line-of-anti-circular implies ( ACirc ( - p)) = ( - ( ACirc p))

    proof

      set n = ( len p);

      

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

      

       A2: ( Indices ( ACirc 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-line-of-anti-circular;

      then ( - p) is first-line-of-anti-circular by Th58;

      then

       A5: ( ACirc ( - p)) is_anti-circular_about ( - p) by Def12;

      

       A6: ( ACirc p) is_anti-circular_about p by A4, Def12;

      

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

      proof

        let i,j be Nat;

        assume

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

        now

          per cases ;

            case

             A9: i <= j;

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

            then

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

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

            

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

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

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

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

            hence thesis;

          end;

            case

             A11: i >= j;

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

            then

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

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

            

            then (( ACirc ( - p)) * (i,j)) = (( - ( - p)) . (((j - i) mod ( len ( - p))) + 1)) by A5, A11

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

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

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

            hence thesis;

          end;

        end;

        hence thesis;

      end;

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

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

    end;

    theorem :: MATRIX16:60

    

     Th60: p is first-line-of-anti-circular & q is first-line-of-anti-circular & ( len p) = ( len q) implies (p + q) is first-line-of-anti-circular

    proof

      set n = ( len p);

      assume that

       A1: p is first-line-of-anti-circular and

       A2: q is first-line-of-anti-circular and

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

      consider M2 be Matrix of n, K such that

       A4: M2 is_anti-circular_about q by A2, A3;

      

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

      

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

      ( len q) = ( width M2) by A4;

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

      then

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

      then

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

      consider M1 be Matrix of n, K such that

       A9: M1 is_anti-circular_about p by A1;

      

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

      set M3 = (M1 + M2);

      

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

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

      then

       A12: ( len ( - q)) = ( len q) by CARD_1:def 7;

      

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

      

       A14: ( Indices (M1 + M2)) = [:( Seg n), ( Seg 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 holds ((M1 + M2) * (i,j)) = ((p + q) . (((j - i) mod ( len (p + q))) + 1))

      proof

        let i,j be Nat;

        assume that

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

         A18: i <= j;

        

         A19: (((j - i) mod ( len (p + q))) + 1) in ( dom (p + q)) by A14, A6, A15, A7, A17, Lm3;

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

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

        .= (the addF of K . ((p . (((j - i) mod ( len (p + q))) + 1)),(q . (((j - i) mod ( len (p + q))) + 1)))) by A3, A9, A10, A14, A8, A17, A18

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

        hence thesis;

      end;

      

       A20: 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

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

      then

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

      

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

      proof

        let i,j be Nat;

        assume that

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

         A25: i >= j;

        ( dom ( - p)) = ( Seg ( len p)) & ( dom ( - q)) = ( Seg ( len q)) by A21, A12, FINSEQ_1:def 3;

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

        then

         A26: (((j - i) mod ( len (p + q))) + 1) in ( dom (( - p) + ( - q))) by A14, A6, A15, A22, A7, A24, Lm3;

        ((M1 + M2) * (i,j)) = ((M1 * (i,j)) + (M2 * (i,j))) by A10, A14, A24, MATRIX_3:def 3

        .= (the addF of K . ((M1 * (i,j)),(( - q) . (((j - i) mod ( len q)) + 1)))) by A4, A13, A14, A24, A25

        .= (the addF of K . ((( - p) . (((j - i) mod ( len p)) + 1)),(( - q) . (((j - i) mod ( len q)) + 1)))) by A9, A10, A14, A24, A25

        .= ((( - p) + ( - q)) . (((j - i) mod ( len (p + q))) + 1)) by A3, A8, A26, FUNCOP_1: 22

        .= (( - (p + q)) . (((j - i) mod ( len (p + q))) + 1)) by A3, A20, A11, FVSUM_1: 31;

        hence thesis;

      end;

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

      then ( len (p + q)) = ( width (M1 + M2)) by A6, A7, FINSEQ_1:def 3;

      then ( len (M1 + M2)) = n & M3 is_anti-circular_about (p + q) by A16, A23, MATRIX_0: 24;

      then

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

       A27: M3 is_anti-circular_about (p + q) by A8;

      take M3;

      thus thesis by A27;

    end;

    theorem :: MATRIX16:61

    

     Th61: p is first-line-of-anti-circular & q is first-line-of-anti-circular & ( len p) = ( len q) implies ( ACirc (p + q)) = (( ACirc p) + ( ACirc q))

    proof

      set n = ( len p);

      assume that

       A1: p is first-line-of-anti-circular and

       A2: q is first-line-of-anti-circular and

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

      

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

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

      then

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

      then

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

      then

       A7: ( Indices ( ACirc p)) = ( Indices ( ACirc (p + q))) by MATRIX_0: 26;

      

       A8: ( Indices ( ACirc p)) = ( Indices ( ACirc q)) by A3, MATRIX_0: 26;

      

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

      

       A10: 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

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

      

       A12: ( Indices ( ACirc p)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      (p + q) is first-line-of-anti-circular by A1, A2, A3, Th60;

      then

       A13: ( ACirc (p + q)) is_anti-circular_about (p + q) by Def12;

      

       A14: ( ACirc q) is_anti-circular_about q by A2, Def12;

      

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

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

      then

       A16: ( len ( - q)) = ( len q) by CARD_1:def 7;

      

       A17: ( ACirc p) is_anti-circular_about p by A1, Def12;

      

       A18: ( Indices ( ACirc q)) = [:( Seg n), ( Seg n):] by A3, MATRIX_0: 24;

      

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

      proof

        let i,j be Nat;

        assume

         A20: [i, j] in ( Indices ( ACirc p));

        then

         A21: (((j - i) mod n) + 1) in ( Seg n) by A12, Lm3;

        now

          per cases ;

            case

             A22: i <= j;

            

            then (( ACirc (p + q)) * (i,j)) = ((p + q) . (((j - i) mod ( len (p + q))) + 1)) by A13, A7, A20

            .= (the addF of K . ((p . (((j - i) mod ( len (p + q))) + 1)),(q . (((j - i) mod ( len (p + q))) + 1)))) by A9, A6, A21, FUNCOP_1: 22

            .= (the addF of K . ((( ACirc p) * (i,j)),(q . (((j - i) mod ( len q)) + 1)))) by A3, A6, A17, A20, A22

            .= ((( ACirc p) * (i,j)) + (( ACirc q) * (i,j))) by A14, A8, A20, A22;

            hence thesis;

          end;

            case

             A23: i >= j;

            

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

            ( dom ( - q)) = ( Seg ( len q)) by A16, FINSEQ_1:def 3;

            then ( dom p) = ( Seg n) & ( dom (( - p) + ( - q))) = ( dom ( - p)) by A3, A24, FINSEQ_1:def 3, POLYNOM1: 1;

            then

             A25: (((j - i) mod ( len (p + q))) + 1) in ( dom (( - p) + ( - q))) by A9, A5, A12, A20, A24, Lm3;

            (( ACirc (p + q)) * (i,j)) = (( - (p + q)) . (((j - i) mod ( len (p + q))) + 1)) by A13, A7, A20, A23

            .= ((( - p) + ( - q)) . (((j - i) mod ( len (p + q))) + 1)) by A3, A10, A15, FVSUM_1: 31

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

            .= (the addF of K . ((( ACirc p) * (i,j)),(( - q) . (((j - i) mod ( len q)) + 1)))) by A3, A6, A17, A20, A23

            .= ((( ACirc p) * (i,j)) + (( ACirc q) * (i,j))) by A14, A12, A18, A20, A23;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A26: ( len ( ACirc p)) = ( len p) & ( width ( ACirc p)) = ( len p) by MATRIX_0: 24;

      ( len ( ACirc (p + q))) = ( len p) & ( width ( ACirc (p + q))) = ( len p) by A6, MATRIX_0: 24;

      hence thesis by A26, A19, MATRIX_3:def 3;

    end;

    theorem :: MATRIX16:62

    

     Th62: p is first-line-of-anti-circular implies (a * p) is first-line-of-anti-circular

    proof

      set n = ( len p);

      

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

      assume p is first-line-of-anti-circular;

      then

      consider M1 be Matrix of n, K such that

       A2: M1 is_anti-circular_about p;

      

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

      

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

      

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

      proof

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

        

        then

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

        .= ( dom ( - p)) by FINSEQ_1:def 3;

        

         A7: (a * p) is Element of (n -tuples_on the carrier of K) by A4, FINSEQ_2: 92;

        let i,j be Nat;

        assume that

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

         A9: i >= j;

        

         A10: (((j - i) mod n) + 1) in ( Seg n) by A3, A8, Lm3;

        

         A11: p is Element of (n -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 ( len ( - p)) = ( len p) by CARD_1:def 7;

        then

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

        

         A13: [i, j] in ( Indices M1) by A3, A8, 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) . (((j - i) mod ( len p)) + 1))) by A2, A9, A13

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

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

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

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

        .= ((a * (( - ( 1_ K)) * p)) . (((j - i) mod ( len p)) + 1)) by A11, FVSUM_1: 59

        .= (((a * ( - ( 1_ K))) * p) . (((j - i) mod ( len p)) + 1)) by A11, FVSUM_1: 54

        .= ((( - (a * ( 1_ K))) * p) . (((j - i) mod ( len p)) + 1)) by VECTSP_1: 8

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

        .= ((( - (( 1_ K) * a)) * p) . (((j - i) mod ( len p)) + 1))

        .= (((( - ( 1_ K)) * a) * p) . (((j - i) mod ( len p)) + 1)) by VECTSP_1: 9

        .= ((( - ( 1_ K)) * (a * p)) . (((j - i) mod ( len p)) + 1)) by A11, FVSUM_1: 54

        .= (( - (a * p)) . (((j - i) mod ( len p)) + 1)) by A7, FVSUM_1: 59;

        hence thesis by MATRIXR1: 16;

      end;

      

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

      

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

      proof

        let i,j be Nat;

        assume that

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

         A17: i <= j;

        

         A18: (((j - i) mod n) + 1) in ( Seg n) by A3, A16, Lm3;

        then

         A19: (((j - i) mod ( len p)) + 1) in ( dom (a * p)) by A14, MATRIXR1: 16;

        

         A20: [i, j] in ( Indices M1) by A3, A16, 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 . (((j - i) mod ( len p)) + 1))) by A2, A17, A20

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

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

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

        .= ((a * p) . (((j - i) mod ( len p)) + 1)) by A19, PARTFUN1:def 6;

        hence thesis by MATRIXR1: 16;

      end;

      ( width (a * M1)) = n by MATRIX_0: 24;

      then (a * M1) is_anti-circular_about (a * p) by A4, A15, A5;

      then

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

       A21: M2 is_anti-circular_about (a * p) by A4;

      take M2;

      thus thesis by A21;

    end;

    theorem :: MATRIX16:63

    

     Th63: p is first-line-of-anti-circular implies ( ACirc (a * p)) = (a * ( ACirc p))

    proof

      set n = ( len p);

      

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

      assume

       A2: p is first-line-of-anti-circular;

      then

       A3: ( ACirc p) is_anti-circular_about p by Def12;

      (a * p) is first-line-of-anti-circular by A2, Th62;

      then

       A4: ( ACirc (a * p)) is_anti-circular_about (a * p) by Def12;

      

       A5: ( Indices ( ACirc p)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

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

      proof

        let i,j be Nat;

        assume

         A7: [i, j] in ( Indices ( ACirc p));

        then

         A8: (((j - i) mod n) + 1) in ( Seg n) by A5, Lm3;

        

         A9: [i, j] in ( Indices ( ACirc (a * p))) by A1, A7, MATRIX_0: 26;

        now

          per cases ;

            case

             A10: i <= j;

            

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

            

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

            (( ACirc (a * p)) * (i,j)) = ((a * p) . (((j - i) mod ( len (a * p))) + 1)) by A4, A9, A10

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

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

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

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

            .= ((a multfield ) . (( ACirc p) * (i,j))) by A3, A7, A10

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

            hence thesis;

          end;

            case

             A13: i >= j;

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

            

            then

             A14: ( dom (a * ( - p))) = ( Seg ( len ( - p))) by FINSEQ_1:def 3

            .= ( dom ( - p)) by FINSEQ_1:def 3;

            

             A15: (a * p) is Element of (n -tuples_on the carrier of K) by A1, FINSEQ_2: 92;

            

             A16: p is Element of (n -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 ( len ( - p)) = ( len p) by CARD_1:def 7;

            then

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

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

            .= ((a multfield ) . (( - p) . (((j - i) mod ( len p)) + 1))) by A3, A7, A13

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

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

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

            .= ((a * ( - p)) . (((j - i) mod ( len p)) + 1)) by A8, A17, A14, PARTFUN1:def 6

            .= ((a * (( - ( 1_ K)) * p)) . (((j - i) mod ( len p)) + 1)) by A16, FVSUM_1: 59

            .= (((a * ( - ( 1_ K))) * p) . (((j - i) mod ( len p)) + 1)) by A16, FVSUM_1: 54

            .= ((( - (a * ( 1_ K))) * p) . (((j - i) mod ( len p)) + 1)) by VECTSP_1: 8

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

            .= ((( - (( 1_ K) * a)) * p) . (((j - i) mod ( len p)) + 1))

            .= (((( - ( 1_ K)) * a) * p) . (((j - i) mod ( len p)) + 1)) by VECTSP_1: 9

            .= ((( - ( 1_ K)) * (a * p)) . (((j - i) mod ( len p)) + 1)) by A16, FVSUM_1: 54

            .= (( - (a * p)) . (((j - i) mod ( len p)) + 1)) by A15, FVSUM_1: 59

            .= (( ACirc (a * p)) * (i,j)) by A1, A4, A9, A13;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

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

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

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

    end;

    theorem :: MATRIX16:64

    p is first-line-of-anti-circular implies ((a * ( ACirc p)) + (b * ( ACirc p))) = ( ACirc ((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-line-of-anti-circular;

      then

       A4: (a * p) is first-line-of-anti-circular & (b * p) is first-line-of-anti-circular by Th62;

      ((a * ( ACirc p)) + (b * ( ACirc p))) = (( ACirc (a * p)) + (b * ( ACirc p))) by A3, Th63

      .= (( ACirc (a * p)) + ( ACirc (b * p))) by A3, Th63

      .= ( ACirc ((a * p) + (b * p))) by A4, A1, Th61, MATRIXR1: 16;

      hence thesis by A2, FVSUM_1: 55;

    end;

    theorem :: MATRIX16:65

    p is first-line-of-anti-circular & q is first-line-of-anti-circular & ( len p) = ( len q) implies ((a * ( ACirc p)) + (a * ( ACirc q))) = ( ACirc (a * (p + q)))

    proof

      assume that

       A1: p is first-line-of-anti-circular & q is first-line-of-anti-circular and

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

      

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

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

      

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

      .= (a * ( ACirc (p + q))) by A1, A2, Th61

      .= ( ACirc (a * (p + q))) by A1, A2, Th60, Th63;

      hence thesis;

    end;

    theorem :: MATRIX16:66

    p is first-line-of-anti-circular & q is first-line-of-anti-circular & ( len p) = ( len q) implies ((a * ( ACirc p)) + (b * ( ACirc q))) = ( ACirc ((a * p) + (b * q)))

    proof

      set n = ( len p);

      assume that

       A1: p is first-line-of-anti-circular and

       A2: q is first-line-of-anti-circular and

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

      

       A4: (a * p) is first-line-of-anti-circular & (b * q) is first-line-of-anti-circular by A1, A2, Th62;

      

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

      ((a * ( ACirc p)) + (b * ( ACirc q))) = (( ACirc (a * p)) + (b * ( ACirc q))) by A1, Th63

      .= (( ACirc (a * p)) + ( ACirc (b * q))) by A2, Th63

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

      hence thesis;

    end;

    registration

      let K, n;

      cluster ( 0. (K,n)) -> anti-circular;

      coherence

      proof

        set p = (n |-> ( 0. K));

        

         A1: ( width ( 0. (K,n))) = n by MATRIX_0: 24;

        

         A2: ( 0. (K,n,n)) = (n |-> (n |-> ( 0. K)));

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

        

         A3: ( len (n |-> ( 0. K))) = n by CARD_1:def 7;

        

         A4: ( Indices ( 0. (K,n))) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        

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

        proof

          let i,j be Nat;

          assume that

           A6: [i, j] in ( Indices M1) and i >= j;

          

           A7: (((j - i) mod n) + 1) in ( Seg n) by A4, A6, Lm3;

          (( - p) . (((j - i) mod ( len p)) + 1)) = ((n |-> ( - ( 0. K))) . (((j - i) mod n) + 1)) by A3, FVSUM_1: 25

          .= ( - ( 0. K)) by A7, FUNCOP_1: 7

          .= ( 0. K) by VECTSP_2: 3;

          hence thesis by A2, A6, MATRIX_3: 1;

        end;

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

        proof

          let i,j be Nat;

          assume that

           A8: [i, j] in ( Indices M1) and i <= j;

          (((j - i) mod n) + 1) in ( Seg n) by A4, A8, Lm3;

          then ((( Seg n) --> ( 0. K)) . (((j - i) mod n) + 1)) = ( 0. K) by FUNCOP_1: 7;

          hence thesis by A3, A2, A8, MATRIX_3: 1;

        end;

        then M1 is_anti-circular_about p by A1, A3, A5;

        then

        consider p be FinSequence of K such that

         A9: ( len p) = ( width M1) & M1 is_anti-circular_about p;

        take p;

        thus thesis by A9;

      end;

    end