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):] & len (1. K,n) = n & width (1. K,n) = n ) by MATRIX_1:25;
A3: len (Line (1. K,n),1) = n by A2, 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) )
assume B1: [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 ( 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: j - i <= n - 1 by XREAL_1:15;
n - 1 < n by XREAL_1:46;
then B8: j - i < n by B5, XXREAL_0:2;
B9: 1 - n <= j - i by B4, XREAL_1:15;
- n <= (- n) + 1 by XREAL_1:31;
then B11: - n <= j - i by B9, XXREAL_0:2;
B12: (j - i) mod n >= 0 by A1, INT_3:9;
(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 B5, B8, INT_3:10; :: thesis: verum

end;

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

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

end;

end;

end;

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

then C2: (j - i) mod (len (Line (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 C3: [1,1] in Indices (1. K,n) by A2, ZFMISC_1:106;
(Line (1. K,n),1) . (((j - i) mod (len (Line (1. K,n),1))) + 1) = (1. K,n) * 1,1 by B23, A2, C2, MATRIX_1:def 8
.= 1_ K by C3, 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 C1, B1, MATRIX_1:def 12; :: thesis: verum

end;

suppose C2: 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 B8, INT_3:10;
hence (j - i) mod n <> 0 by C2; :: thesis: verum

end;

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

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

end;

end;

end;

then D3: ((j - i) mod (len (Line (1. K,n),1))) + 1 <> 1 by A2, MATRIX_1:def 8;
E1: 0 + 1 <= n by A1, NAT_1:13;
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 B, A2, MATRIX_1:def 8;
( 1 in Seg n & l in Seg n & l in Seg (width (1. K,n)) ) by A2, E1, B22, MATRIX_1:def 8;
then D6: [1,l] in Indices (1. K,n) by A2, ZFMISC_1:106;
(Line (1. K,n),1) . l = (1. K,n) * 1,l by A2, B23, MATRIX_1:def 8
.= 0. K by D3, D6, 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 C2, B1, 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 A9: 1. K,n is_line_circulant_about Line (1. K,n),1 by A2, A3, Def1;
consider p being FinSequence of K such that
A11: ( len p = width (1. K,n) & 1. K,n is_line_circulant_about p ) by A2, A3, A9;
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 A11; :: thesis: verum