let K be Field; for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (- p) = - (CCirc p)
let p be FinSequence of K; ( p is first-col-of-circulant implies CCirc (- p) = - (CCirc p) )
set n = len p;
A1:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A2:
Indices (CCirc p) = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
assume A3:
p is first-col-of-circulant
; CCirc (- p) = - (CCirc p)
then A4:
CCirc p is_col_circulant_about p
by Def8;
- p is first-col-of-circulant
by A3, Th35;
then A5:
CCirc (- p) is_col_circulant_about - p
by Def8;
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 A6:
len (- p) = len p
by CARD_1:def 7;
then A7:
Indices (CCirc p) = Indices (CCirc (- p))
by MATRIX_0:26;
A8:
for i, j being Nat st [i,j] in Indices (CCirc p) holds
(CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j))
proof
let i,
j be
Nat;
( [i,j] in Indices (CCirc p) implies (CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j)) )
assume A9:
[i,j] in Indices (CCirc p)
;
(CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j))
then A10:
((i - j) mod (len p)) + 1
in Seg (len p)
by A2, Lm3;
(CCirc (- p)) * (
i,
j) =
(- p) . (((i - j) mod (len (- p))) + 1)
by A5, A7, A9
.=
(comp K) . (p . (((i - j) mod (len p)) + 1))
by A6, A1, A10, FUNCT_1:13
.=
(comp K) . ((CCirc p) * (i,j))
by A4, A9
.=
- ((CCirc p) * (i,j))
by VECTSP_1:def 13
;
hence
(CCirc (- p)) * (
i,
j)
= - ((CCirc p) * (i,j))
;
verum
end;
A11:
( len (CCirc p) = len p & width (CCirc p) = len p )
by MATRIX_0:24;
( len (CCirc (- p)) = len p & width (CCirc (- p)) = len p )
by A6, MATRIX_0:24;
hence
CCirc (- p) = - (CCirc p)
by A11, A8, MATRIX_3:def 2; verum