let n be Element of NAT ; :: thesis: for K being Field st n > 0 holds
1. (K,n) is line_circulant
let K be Field; :: thesis: ( n > 0 implies 1. (K,n) is line_circulant )
set M1 = 1. (K,n);
set p = Line ((1. (K,n)),1);
assume A1: n > 0 ; :: thesis: 1. (K,n) is line_circulant
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 (Line ((1. (K,n)),1)) = n by MATRIX_0:def 7;
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((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) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1) )
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 (1. (K,n)) ; :: thesis: (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1)
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 ( 0 <= j - i or 0 > j - i ) ;

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

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

end;

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

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

end;

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

proof

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

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

0 + 1 <= n by A1, NAT_1:13;
then 1 in Seg n ;
then A21: [1,1] in Indices (1. (K,n)) by A2, ZFMISC_1:87;
(j - i) mod (len (Line ((1. (K,n)),1))) = 0 by A1, A4, A20, NAT_D:63;
then (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1) = (1. (K,n)) * (1,1) by A3, A19, MATRIX_0:def 7
.= 1_ K by A21, MATRIX_1:def 3 ;
hence (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1) by A7, A20, MATRIX_1:def 3; :: thesis: verum

end;

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

(j - i) mod n <> 0

proof

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

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

then (j - i) mod n = j - i by A13, NAT_D:63;
hence (j - i) mod n <> 0 by A22; :: thesis: verum

end;

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

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

end;

end;

end;

then A24: ((j - i) mod (len (Line ((1. (K,n)),1)))) + 1 <> 1 by A3, MATRIX_0:def 7;
set l = ((j - i) mod (len (Line ((1. (K,n)),1)))) + 1;
reconsider l = ((j - i) mod (len (Line ((1. (K,n)),1)))) + 1 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 (1. (K,n)) by A2, A25, ZFMISC_1:87;
(Line ((1. (K,n)),1)) . l = (1. (K,n)) * (1,l) by A3, A19, MATRIX_0:def 7
.= 0. K by A24, A26, MATRIX_1:def 3 ;
hence (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1) by A7, A22, MATRIX_1:def 3; :: thesis: verum

end;

end;

end;

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

end;

then 1. (K,n) is_line_circulant_about Line ((1. (K,n)),1) by A3, A4;
then consider p being FinSequence of K such that
A27: ( len p = width (1. (K,n)) & 1. (K,n) is_line_circulant_about p ) ;
take p ; :: according to MATRIX16:def 2 :: thesis: ( len p = width (1. (K,n)) & 1. (K,n) is_line_circulant_about p )
thus ( len p = width (1. (K,n)) & 1. (K,n) is_line_circulant_about p ) by A27; :: thesis: verum