let K be Field; for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (- p) = - (ACirc p)
let p be FinSequence of K; ( p is first-line-of-anti-circular implies ACirc (- p) = - (ACirc p) )
set n = len p;
A1:
( len (ACirc p) = len p & width (ACirc p) = len p )
by MATRIX_0:24;
A2:
Indices (ACirc p) = [:(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
- p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:113;
then A3:
len (- p) = len p
by CARD_1:def 7;
assume A4:
p is first-line-of-anti-circular
; ACirc (- p) = - (ACirc p)
then
- p is first-line-of-anti-circular
by Th58;
then A5:
ACirc (- p) is_anti-circular_about - p
by Def12;
A6:
ACirc p is_anti-circular_about p
by A4, Def12;
A7:
for i, j being Nat st [i,j] in Indices (ACirc p) holds
(ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j))
proof
let i,
j be
Nat;
( [i,j] in Indices (ACirc p) implies (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) )
assume A8:
[i,j] in Indices (ACirc p)
;
(ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j))
now ( ( i <= j & (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) ) or ( i >= j & (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) ) )per cases
( i <= j or i >= j )
;
case A9:
i <= j
;
(ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j))
((j - i) mod (len p)) + 1
in Seg (len p)
by A2, A8, Lm3;
then A10:
((j - i) mod (len p)) + 1
in dom p
by FINSEQ_1:def 3;
[i,j] in Indices (ACirc (- p))
by A3, A8, MATRIX_0:26;
then (ACirc (- p)) * (
i,
j) =
(- p) . (((j - i) mod (len (- p))) + 1)
by A5, A9
.=
(comp K) . (p . (((j - i) mod (len p)) + 1))
by A3, A10, FUNCT_1:13
.=
(comp K) . ((ACirc p) * (i,j))
by A6, A8, A9
.=
- ((ACirc p) * (i,j))
by VECTSP_1:def 13
;
hence
(ACirc (- p)) * (
i,
j)
= - ((ACirc p) * (i,j))
;
verum end; case A11:
i >= j
;
(ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j))
((j - i) mod (len p)) + 1
in Seg (len p)
by A2, A8, Lm3;
then A12:
((j - i) mod (len p)) + 1
in dom (- p)
by A3, FINSEQ_1:def 3;
[i,j] in Indices (ACirc (- p))
by A3, A8, MATRIX_0:26;
then (ACirc (- p)) * (
i,
j) =
(- (- p)) . (((j - i) mod (len (- p))) + 1)
by A5, A11
.=
(comp K) . ((- p) . (((j - i) mod (len p)) + 1))
by A3, A12, FUNCT_1:13
.=
(comp K) . ((ACirc p) * (i,j))
by A6, A8, A11
.=
- ((ACirc p) * (i,j))
by VECTSP_1:def 13
;
hence
(ACirc (- p)) * (
i,
j)
= - ((ACirc p) * (i,j))
;
verum end; end; end;
hence
(ACirc (- p)) * (
i,
j)
= - ((ACirc p) * (i,j))
;
verum
end;
( len (ACirc (- p)) = len p & width (ACirc (- p)) = len p )
by A3, MATRIX_0:24;
hence
ACirc (- p) = - (ACirc p)
by A1, A7, MATRIX_3:def 2; verum