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
A2: ( Indices (1. K,n) = [:(Seg n),(Seg n):] & len (1. K,n) = n & width (1. K,n) = n ) by MATRIX_1:25;
set M1 = 1. K,n;
set p = Col (1. K,n),1;
A3: len (Col (1. K,n),1) = n by A2, MATRIX_1:def 9;
A6: ( dom (Col (1. K,n),1) = Seg n & dom (1. K,n) = Seg n ) by A2, A3, FINSEQ_1:def 3;
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) )
assume B1: [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 ( i in Seg n & j in Seg n ) by A2, ZFMISC_1:106;
then B4: ( 1 <= i & i <= n & 1 <= j & j <= n ) by FINSEQ_1:3;
then B5: i - j <= n - 1 by XREAL_1:15;
n - 1 < n by XREAL_1:46;
then B8: i - j < n by B5, XXREAL_0:2;
B9: 1 - n <= i - j by B4, XREAL_1:15;
- n <= (- n) + 1 by XREAL_1:31;
then B11: - n <= i - j by B9, XXREAL_0:2;
B12: (i - j) mod n >= 0 by A1, INT_3:9;
B13: (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 B5, B8, INT_3:10; :: thesis: verum

end;

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

i - j <= - 1 by C1, INT_1:21;
then n + (i - j) <= n + (- 1) by XREAL_1:8;
hence (i - j) mod n <= n - 1 by C1, B11, INT_3:10; :: thesis: verum

end;

end;

end;

B15: ( ((i - j) mod n) + 1 >= 0 + 1 & ((i - j) mod n) + 1 <= (n - 1) + 1 ) by B12, B13, XREAL_1:8;
B20: ((i - j) mod n) + 1 in NAT by B12, INT_1:16;
then B22: ((i - j) mod n) + 1 in Seg n by B15;
then B23: ((i - j) mod (len (Col (1. K,n),1))) + 1 in Seg n by A2, MATRIX_1:def 9;
(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 C1: i = j ; :: thesis: (1. K,n) * i,j = (Col (1. K,n),1) . (((i - j) mod (len (Col (1. K,n),1))) + 1)

then C2: (i - j) mod (len (Col (1. K,n),1)) = 0 by A1, A3, INT_3:10;
0 + 1 <= n by A1, NAT_1:13;
then ( 1 in Seg n & 1 in Seg n ) ;
then C: [1,1] in Indices (1. K,n) by A2, ZFMISC_1:106;
(Col (1. K,n),1) . (((i - j) mod (len (Col (1. K,n),1))) + 1) = (1. K,n) * 1,1 by B23, A6, C2, MATRIX_1:def 9
.= 1_ K by C, MATRIX_1:def 12 ;
hence (1. K,n) * i,j = (Col (1. K,n),1) . (((i - j) mod (len (Col (1. K,n),1))) + 1) by C1, B1, MATRIX_1:def 12; :: thesis: verum

end;

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

then D1: 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 D1, B8, INT_3:10; :: thesis: verum

end;

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

(1 - n) + n <= (i - j) + n by B9, XREAL_1:8;
hence (i - j) mod n <> 0 by E1, B11, INT_3:10; :: thesis: verum

end;

end;

end;

then D3: ((i - j) mod (len (Col (1. K,n),1))) + 1 <> 1 by A2, MATRIX_1:def 9;
E1: 0 + 1 <= n by A1, NAT_1:13;
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 A2, B20, MATRIX_1:def 9;
( 1 in Seg n & l in dom (1. K,n) ) by A3, E1, B22, A2, FINSEQ_1:def 3;
then D6: [l,1] in Indices (1. K,n) by A2, ZFMISC_1:106;
(Col (1. K,n),1) . l = (1. K,n) * l,1 by A6, B23, MATRIX_1:def 9
.= 0. K by D6, D3, MATRIX_1:def 12 ;
hence (1. K,n) * i,j = (Col (1. K,n),1) . (((i - j) mod (len (Col (1. K,n),1))) + 1) by C2, B1, MATRIX_1:def 12; :: 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 A9: 1. K,n is_col_circulant_about Col (1. K,n),1 by A2, A3, Def4;
consider p being FinSequence of K such that
A11: ( len p = len (1. K,n) & 1. K,n is_col_circulant_about p ) by A2, A3, A9;
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 A11; :: thesis: verum