let n be Element of NAT ; :: thesis: for K being Field st n > 0 holds
1. (K,n) is col_circulant
let K be Field; :: thesis: ( n > 0 implies 1. (K,n) is col_circulant )
assume A1: n > 0 ; :: thesis: 1. (K,n) is col_circulant
set M1 = 1. (K,n);
A2: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
set p = Col ((1. (K,n)),1);
A3: len (1. (K,n)) = n by MATRIX_0:24;
then A4: len (Col ((1. (K,n)),1)) = n by MATRIX_0:def 8;
A5: dom (1. (K,n)) = Seg n by A3, FINSEQ_1:def 3;
A6: width (1. (K,n)) = n by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) )
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 (1. (K,n)) ; :: thesis: (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
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 ( 0 <= i - j or 0 > i - j ) ;

suppose 0 <= i - j ; :: thesis: (i - j) mod n <= n - 1

hence (i - j) mod n <= n - 1 by A16, A17, NAT_D:63; :: thesis: verum

end;

suppose A18: 0 > i - j ; :: thesis: (i - j) mod n <= n - 1

then i - j <= - 1 by INT_1:8;
then n + (i - j) <= n + (- 1) by XREAL_1:6;
hence (i - j) mod n <= n - 1 by A15, A18, NAT_D:63; :: thesis: verum

end;

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 (Col ((1. (K,n)),1)))) + 1 in Seg n by A3, MATRIX_0:def 8;
(1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)

proof

per cases ( i = j or i <> j ) ;

suppose A22: i = j ; :: thesis: (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)

0 + 1 <= n by A1, NAT_1:13;
then 1 in Seg n ;
then A23: [1,1] in Indices (1. (K,n)) by A2, ZFMISC_1:87;
(i - j) mod (len (Col ((1. (K,n)),1))) = 0 by A1, A4, A22, NAT_D:63;
then (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) = (1. (K,n)) * (1,1) by A5, A21, MATRIX_0:def 8
.= 1_ K by A23, MATRIX_1:def 3 ;
hence (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) by A9, A22, MATRIX_1:def 3; :: thesis: verum

end;

suppose A24: i <> j ; :: thesis: (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)

then A25: i - j <> 0 ;
(i - j) mod n <> 0

proof

per cases ( 0 <= i - j or 0 > i - j ) ;

suppose 0 <= i - j ; :: thesis: (i - j) mod n <> 0

hence (i - j) mod n <> 0 by A17, A25, NAT_D:63; :: thesis: verum

end;

suppose A26: 0 > i - j ; :: thesis: (i - j) mod n <> 0

(1 - n) + n <= (i - j) + n by A14, XREAL_1:6;
hence (i - j) mod n <> 0 by A15, A26, NAT_D:63; :: thesis: verum

end;

end;

end;

then A27: ((i - j) mod (len (Col ((1. (K,n)),1)))) + 1 <> 1 by A3, MATRIX_0:def 8;
set l = ((i - j) mod (len (Col ((1. (K,n)),1)))) + 1;
reconsider l = ((i - j) mod (len (Col ((1. (K,n)),1)))) + 1 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 (1. (K,n)) by A3, A4, A20, FINSEQ_1:def 3;
then A29: [l,1] in Indices (1. (K,n)) by A6, A28, ZFMISC_1:87;
(Col ((1. (K,n)),1)) . l = (1. (K,n)) * (l,1) by A5, A21, MATRIX_0:def 8
.= 0. K by A27, A29, MATRIX_1:def 3 ;
hence (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) by A9, A24, MATRIX_1:def 3; :: thesis: verum

end;

end;

end;

hence (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) ; :: thesis: verum

end;

then 1. (K,n) is_col_circulant_about Col ((1. (K,n)),1) by A3, A4;
then consider p being FinSequence of K such that
A30: ( len p = len (1. (K,n)) & 1. (K,n) is_col_circulant_about p ) ;
take p ; :: according to MATRIX16:def 5 :: thesis: ( len p = len (1. (K,n)) & 1. (K,n) is_col_circulant_about p )
thus ( len p = len (1. (K,n)) & 1. (K,n) is_col_circulant_about p ) by A30; :: thesis: verum