let n be Element of NAT ; for K being Field
for M1 being Matrix of n,K st M1 is anti-circular holds
- M1 is anti-circular
let K be Field; for M1 being Matrix of n,K st M1 is anti-circular holds
- M1 is anti-circular
let M1 be Matrix of n,K; ( M1 is anti-circular implies - M1 is anti-circular )
A1:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
assume
M1 is anti-circular
; - M1 is anti-circular
then consider p being FinSequence of K such that
A2:
len p = width M1
and
A3:
M1 is_anti-circular_about p
;
set r = - p;
p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:92;
then A4:
- p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:113;
A5:
Indices (- M1) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A6:
width M1 = n
by MATRIX_0:24;
A7:
for i, j being Nat st [i,j] in Indices (- M1) & i <= j holds
(- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (- M1) & i <= j implies (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) )
assume that A8:
[i,j] in Indices (- M1)
and A9:
i <= j
;
(- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
((j - i) mod n) + 1
in Seg n
by A5, A8, Lm3;
then A10:
((j - i) mod (len p)) + 1
in dom p
by A2, A6, FINSEQ_1:def 3;
(- M1) * (
i,
j) =
- (M1 * (i,j))
by A1, A5, A8, MATRIX_3:def 2
.=
(comp K) . (M1 * (i,j))
by VECTSP_1:def 13
.=
(comp K) . (p . (((j - i) mod (len p)) + 1))
by A3, A1, A5, A8, A9
.=
(- p) . (((j - i) mod (len p)) + 1)
by A10, FUNCT_1:13
;
hence
(- M1) * (
i,
j)
= (- p) . (((j - i) mod (len (- p))) + 1)
by A4, CARD_1:def 7;
verum
end;
A11:
width (- M1) = n
by MATRIX_0:24;
A12:
len (- p) = len p
by A4, CARD_1:def 7;
then A13:
dom (- p) = Seg (len p)
by FINSEQ_1:def 3;
for i, j being Nat st [i,j] in Indices (- M1) & i >= j holds
(- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (- M1) & i >= j implies (- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1) )
assume that A14:
[i,j] in Indices (- M1)
and A15:
i >= j
;
(- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1)
A16:
((j - i) mod n) + 1
in Seg n
by A5, A14, Lm3;
(- M1) * (
i,
j) =
- (M1 * (i,j))
by A1, A5, A14, MATRIX_3:def 2
.=
(comp K) . (M1 * (i,j))
by VECTSP_1:def 13
.=
(comp K) . ((- p) . (((j - i) mod (len p)) + 1))
by A3, A1, A5, A14, A15
.=
(- (- p)) . (((j - i) mod (len p)) + 1)
by A2, A6, A13, A16, FUNCT_1:13
;
hence
(- M1) * (
i,
j)
= (- (- p)) . (((j - i) mod (len (- p))) + 1)
by A4, CARD_1:def 7;
verum
end;
then
- M1 is_anti-circular_about - p
by A2, A6, A11, A12, A7;
then consider r being FinSequence of K such that
A17:
( len r = width (- M1) & - M1 is_anti-circular_about r )
;
take
r
; MATRIX16:def 10 ( len r = width (- M1) & - M1 is_anti-circular_about r )
thus
( len r = width (- M1) & - M1 is_anti-circular_about r )
by A17; verum