let K be Field; for p being FinSequence of K st p is first-line-of-anti-circular holds
- p is first-line-of-anti-circular
let p be FinSequence of K; ( p is first-line-of-anti-circular implies - p is first-line-of-anti-circular )
set n = len p;
assume
p is first-line-of-anti-circular
; - p is first-line-of-anti-circular
then consider M1 being Matrix of len p,K such that
A1:
M1 is_anti-circular_about p
;
set M2 = - M1;
A2:
Indices M1 = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
A3:
Indices (- M1) = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
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;
then A5:
len (- p) = len p
by CARD_1:def 7;
then A6:
dom (- p) = Seg (len p)
by FINSEQ_1:def 3;
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)
A10:
((j - i) mod (len p)) + 1
in Seg (len p)
by A3, A8, Lm3;
(- M1) * (
i,
j) =
- (M1 * (i,j))
by A2, A3, 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 A1, A2, A3, A8, A9
.=
(- (- p)) . (((j - i) mod (len p)) + 1)
by A6, A10, FUNCT_1:13
;
hence
(- M1) * (
i,
j)
= (- (- p)) . (((j - i) mod (len (- p))) + 1)
by A4, CARD_1:def 7;
verum
end;
A11:
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 A12:
[i,j] in Indices (- M1)
and A13:
i <= j
;
(- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
((j - i) mod (len p)) + 1
in Seg (len p)
by A3, A12, Lm3;
then A14:
((j - i) mod (len p)) + 1
in dom p
by FINSEQ_1:def 3;
(- M1) * (
i,
j) =
- (M1 * (i,j))
by A2, A3, A12, MATRIX_3:def 2
.=
(comp K) . (M1 * (i,j))
by VECTSP_1:def 13
.=
(comp K) . (p . (((j - i) mod (len p)) + 1))
by A1, A2, A3, A12, A13
.=
(- p) . (((j - i) mod (len p)) + 1)
by A14, FUNCT_1:13
;
hence
(- M1) * (
i,
j)
= (- p) . (((j - i) mod (len (- p))) + 1)
by A4, CARD_1:def 7;
verum
end;
width (- M1) = len p
by MATRIX_0:24;
then
- M1 is_anti-circular_about - p
by A5, A11, A7;
then consider M2 being Matrix of len (- p),K such that
A15:
M2 is_anti-circular_about - p
by A5;
take
M2
; MATRIX16:def 11 M2 is_anti-circular_about - p
thus
M2 is_anti-circular_about - p
by A15; verum