let n be Element of NAT ; for K being Field st n > 0 holds
1. (K,n) is line_circulant
let K be Field; ( 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
; 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;
( [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))
;
(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
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
;
(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;
verum end; suppose A22:
i <> j
;
(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
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;
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)
;
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
; MATRIX16:def 2 ( 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; verum