let i, j, k, n, l be Element of NAT ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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) ; :: thesis: verum