let K be Field; for p being FinSequence of K st p is first-symmetry-of-circulant holds
SCirc (- p) = - (SCirc p)
let p be FinSequence of K; ( p is first-symmetry-of-circulant implies SCirc (- p) = - (SCirc p) )
set n = len p;
A1:
( len (SCirc p) = len p & width (SCirc p) = len p )
by MATRIX_0:24;
A2:
Indices (SCirc 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-symmetry-of-circulant
; SCirc (- p) = - (SCirc p)
then
- p is first-symmetry-of-circulant
by Th8;
then A5:
SCirc (- p) is_symmetry_circulant_about - p
by Def7;
A6:
SCirc p is_symmetry_circulant_about p
by A4, Def7;
A7:
for i, j being Nat st [i,j] in Indices (SCirc p) holds
(SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j))
proof
let i,
j be
Nat;
( [i,j] in Indices (SCirc p) implies (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j)) )
assume A8:
[i,j] in Indices (SCirc p)
;
(SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j))
now (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j))per cases
( i + j <> (len p) + 1 or i + j = (len p) + 1 )
;
suppose A9:
i + j <> (len p) + 1
;
(SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j))
((i + j) - 1) mod (len p) in Seg (len p)
by A2, A8, A9, Lm4;
then A10:
((i + j) - 1) mod (len p) in dom p
by FINSEQ_1:def 3;
[i,j] in Indices (SCirc (- p))
by A3, A8, MATRIX_0:26;
then (SCirc (- p)) * (
i,
j) =
(- p) . (((i + j) - 1) mod (len (- p)))
by A5, A9, A3
.=
(comp K) . (p . (((i + j) - 1) mod (len p)))
by A3, A10, FUNCT_1:13
.=
(comp K) . ((SCirc p) * (i,j))
by A6, A8, A9
.=
- ((SCirc p) * (i,j))
by VECTSP_1:def 13
;
hence
(SCirc (- p)) * (
i,
j)
= - ((SCirc p) * (i,j))
;
verum end; suppose A11:
i + j = (len p) + 1
;
(SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j))
(
i in Seg (len p) &
j in Seg (len p) )
by A2, A8, ZFMISC_1:87;
then
( 1
<= i & 1
<= j )
by FINSEQ_1:1;
then
1
+ 1
<= i + j
by XREAL_1:7;
then
((len p) + 1) - 1
>= (1 + 1) - 1
by A11, XREAL_1:9;
then
len p in Seg (len p)
;
then A12:
len p in dom p
by FINSEQ_1:def 3;
[i,j] in Indices (SCirc (- p))
by A3, A8, MATRIX_0:26;
then (SCirc (- p)) * (
i,
j) =
(- p) . (len (- p))
by A5, A11, A3
.=
(comp K) . (p . (len p))
by A3, A12, FUNCT_1:13
.=
(comp K) . ((SCirc p) * (i,j))
by A6, A8, A11
.=
- ((SCirc p) * (i,j))
by VECTSP_1:def 13
;
hence
(SCirc (- p)) * (
i,
j)
= - ((SCirc p) * (i,j))
;
verum
hence
(SCirc (- p)) * (
i,
j)
= - ((SCirc p) * (i,j))
;
verum
end;
( len (SCirc (- p)) = len p & width (SCirc (- p)) = len p )
by A3, MATRIX_0:24;
hence
SCirc (- p) = - (SCirc p)
by A1, A7, MATRIX_3:def 2; verum