let i, j, k, n, l be Element of NAT ; for D being non empty set
for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
let D be non empty set ; for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
let A be Matrix of n,D; ( A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies A * (i,j) = A * (k,l) )
assume that
A1:
A is col_circulant
and
A2:
[i,j] in [:(Seg n),(Seg n):]
and
A3:
k = i + 1
and
A4:
l = j + 1
and
A5:
i < n
and
A6:
j < n
; A * (i,j) = A * (k,l)
A7:
[i,j] in Indices A
by A2, MATRIX_0:24;
j in Seg n
by A2, ZFMISC_1:87;
then
1 <= j
by FINSEQ_1:1;
then
1 + 1 <= j + 1
by XREAL_1:6;
then A8:
1 <= l
by A4, XXREAL_0:2;
l <= n
by A4, A6, INT_1:7;
then A9:
l in Seg n
by A8;
i in Seg n
by A2, ZFMISC_1:87;
then
1 <= i
by FINSEQ_1:1;
then
1 + 1 <= i + 1
by XREAL_1:6;
then A10:
1 <= k
by A3, XXREAL_0:2;
consider p being FinSequence of D such that
len p = len A
and
A11:
A is_col_circulant_about p
by A1;
k <= n
by A3, A5, INT_1:7;
then
( Indices A = [:(Seg n),(Seg n):] & k in Seg n )
by A10, MATRIX_0:24;
then
[k,l] in Indices A
by A9, ZFMISC_1:87;
then A * (k,l) =
p . (((k - l) mod (len p)) + 1)
by A11
.=
p . (((i - j) mod (len p)) + 1)
by A3, A4
.=
A * (i,j)
by A11, A7
;
hence
A * (i,j) = A * (k,l)
; verum