let i, j, k, n, l be Element of NAT ; for K being Field
for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
M1 * (k,l) = M1 * (i,j)
let K be Field; for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
M1 * (k,l) = M1 * (i,j)
let M1 be Matrix of n,K; ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )
now ( ( i <= j & ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n & M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) ) ) or ( i >= j & ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n & M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) ) ) )per cases
( i <= j or i >= j )
;
case A1:
i <= j
;
( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n & M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )then A2:
i + 1
<= j + 1
by XREAL_1:6;
A3:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
assume that A4:
M1 is
anti-circular
and A5:
[i,j] in [:(Seg n),(Seg n):]
and A6:
k = i + 1
and A7:
l = j + 1
and A8:
i < n
and A9:
j < n
;
( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )
j in Seg n
by A5, ZFMISC_1:87;
then
1
<= j
by FINSEQ_1:1;
then
1
+ 1
<= j + 1
by XREAL_1:6;
then A10:
1
<= j + 1
by XXREAL_0:2;
j + 1
<= n
by A9, INT_1:7;
then A11:
l in Seg n
by A7, A10;
i in Seg n
by A5, ZFMISC_1:87;
then
1
<= i
by FINSEQ_1:1;
then
1
+ 1
<= i + 1
by XREAL_1:6;
then A12:
1
<= i + 1
by XXREAL_0:2;
consider p being
FinSequence of
K such that
len p = width M1
and A13:
M1 is_anti-circular_about p
by A4;
i + 1
<= n
by A8, INT_1:7;
then
k in Seg n
by A6, A12;
then
[k,l] in Indices M1
by A3, A11, ZFMISC_1:87;
then M1 * (
k,
l) =
p . (((l - k) mod (len p)) + 1)
by A6, A7, A13, A2
.=
p . (((j - i) mod (len p)) + 1)
by A6, A7
.=
M1 * (
i,
j)
by A1, A5, A13, A3
;
hence
(
M1 is
anti-circular &
[i,j] in [:(Seg n),(Seg n):] &
k = i + 1 &
l = j + 1 &
i < n &
j < n implies
M1 * (
k,
l)
= M1 * (
i,
j) )
;
verum end; case A14:
i >= j
;
( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n & M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )then A15:
i + 1
>= j + 1
by XREAL_1:6;
A16:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
assume that A17:
M1 is
anti-circular
and A18:
[i,j] in [:(Seg n),(Seg n):]
and A19:
k = i + 1
and A20:
l = j + 1
and A21:
i < n
and A22:
j < n
;
( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )
j in Seg n
by A18, ZFMISC_1:87;
then
1
<= j
by FINSEQ_1:1;
then
1
+ 1
<= j + 1
by XREAL_1:6;
then A23:
1
<= j + 1
by XXREAL_0:2;
j + 1
<= n
by A22, INT_1:7;
then A24:
l in Seg n
by A20, A23;
i in Seg n
by A18, ZFMISC_1:87;
then
1
<= i
by FINSEQ_1:1;
then
1
+ 1
<= i + 1
by XREAL_1:6;
then A25:
1
<= i + 1
by XXREAL_0:2;
consider p being
FinSequence of
K such that
len p = width M1
and A26:
M1 is_anti-circular_about p
by A17;
i + 1
<= n
by A21, INT_1:7;
then
k in Seg n
by A19, A25;
then
[k,l] in Indices M1
by A16, A24, ZFMISC_1:87;
then M1 * (
k,
l) =
(- p) . (((l - k) mod (len p)) + 1)
by A19, A20, A26, A15
.=
(- p) . (((j - i) mod (len p)) + 1)
by A19, A20
.=
M1 * (
i,
j)
by A14, A18, A26, A16
;
hence
(
M1 is
anti-circular &
[i,j] in [:(Seg n),(Seg n):] &
k = i + 1 &
l = j + 1 &
i < n &
j < n implies
M1 * (
k,
l)
= M1 * (
i,
j) )
;
verum end;
hence
( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )
; verum