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_1:25;
A3: width (1. K,n) = n by MATRIX_1:25;
then A4: len (Line (1. K,n),1) = n by MATRIX_1:def 8;
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, INT_3:9;
then A6: ((j - i) mod n) + 1 in NAT by INT_1:16;
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:106;
then A9: 1 <= j by FINSEQ_1:3;
A10: j <= n by A8, FINSEQ_1:3;
A11: i in Seg n by A2, A7, ZFMISC_1:106;
then 1 <= i by FINSEQ_1:3;
then A12: j - i <= n - 1 by A10, XREAL_1:15;
n - 1 < n by XREAL_1:46;
then A13: j - i < n by A12, XXREAL_0:2;
i <= n by A11, FINSEQ_1:3;
then A14: 1 - n <= j - i by A9, XREAL_1:15;
- n <= (- n) + 1 by XREAL_1:31;
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, INT_3:10; :: thesis: verum

end;

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

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

end;

end;

end;

then A17: ((j - i) mod n) + 1 <= (n - 1) + 1 by XREAL_1:8;
((j - i) mod n) + 1 >= 0 + 1 by A5, XREAL_1:8;
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_1:def 8;
(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:106;
(j - i) mod (len (Line (1. K,n),1)) = 0 by A1, A4, A20, INT_3:10;
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_1:def 8
.= 1_ K by A21, MATRIX_1:def 12 ;
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 12; :: 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, INT_3:10;
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:8;
hence (j - i) mod n <> 0 by A15, A23, INT_3:10; :: thesis: verum

end;

end;

end;

then A24: ((j - i) mod (len (Line (1. K,n),1))) + 1 <> 1 by A3, MATRIX_1:def 8;
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_1:def 8;
0 + 1 <= n by A1, NAT_1:13;
then A25: 1 in Seg n ;
l in Seg n by A3, A18, MATRIX_1:def 8;
then A26: [1,l] in Indices (1. K,n) by A2, A25, ZFMISC_1:106;
(Line (1. K,n),1) . l = (1. K,n) * 1,l by A3, A19, MATRIX_1:def 8
.= 0. K by A24, A26, MATRIX_1:def 12 ;
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 12; :: 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, Def1;
then consider p being FinSequence of K such that
A27: ( len p = width (1. K,n) & 1. K,n is_line_circulant_about p ) by A3, A4;
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