let K be Field; :: thesis: for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (- p) = - (LCirc p)
let p be FinSequence of K; :: thesis: ( p is first-line-of-circulant implies LCirc (- p) = - (LCirc p) )
set n = len p;
assume A1:
p is first-line-of-circulant
; :: thesis: LCirc (- p) = - (LCirc p)
then A4:
- p is first-line-of-circulant
by Th31;
p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:110;
then
- p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:133;
then A6:
len (- p) = len p
by FINSEQ_1:def 18;
A10:
LCirc p is_line_circulant_about p
by A1, Def7;
A12:
LCirc (- p) is_line_circulant_about - p
by A4, Def7;
A13:
( len (LCirc (- p)) = len p & len (LCirc p) = len p & width (LCirc (- p)) = len p & width (LCirc p) = len p )
by A6, MATRIX_1:25;
A15:
( Indices (LCirc p) = Indices (LCirc (- p)) & Indices (LCirc p) = [:(Seg (len p)),(Seg (len p)):] )
by A6, MATRIX_1:25, MATRIX_1:27;
for i, j being Nat st [i,j] in Indices (LCirc p) holds
(LCirc (- p)) * i,j = - ((LCirc p) * i,j)
proof
let i,
j be
Nat;
:: thesis: ( [i,j] in Indices (LCirc p) implies (LCirc (- p)) * i,j = - ((LCirc p) * i,j) )
assume B1:
[i,j] in Indices (LCirc p)
;
:: thesis: (LCirc (- p)) * i,j = - ((LCirc p) * i,j)
then B2:
[i,j] in Indices (LCirc (- p))
by A6, MATRIX_1:27;
((j - i) mod (len p)) + 1
in Seg (len p)
by B1, A15, Lm2;
then B23:
((j - i) mod (len p)) + 1
in dom p
by FINSEQ_1:def 3;
(LCirc (- p)) * i,
j =
(- p) . (((j - i) mod (len (- p))) + 1)
by B2, A12, Def1
.=
(comp K) . (p . (((j - i) mod (len p)) + 1))
by A6, B23, FUNCT_1:23
.=
(comp K) . ((LCirc p) * i,j)
by B1, A10, Def1
.=
- ((LCirc p) * i,j)
by VECTSP_1:def 25
;
hence
(LCirc (- p)) * i,
j = - ((LCirc p) * i,j)
;
:: thesis: verum
end;
hence
LCirc (- p) = - (LCirc p)
by A13, MATRIX_3:def 2; :: thesis: verum