let K be Field; for a being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
a * p is first-line-of-anti-circular
let a be Element of K; for p being FinSequence of K st p is first-line-of-anti-circular holds
a * p is first-line-of-anti-circular
let p be FinSequence of K; ( p is first-line-of-anti-circular implies a * p is first-line-of-anti-circular )
set n = len p;
A1:
dom p = Seg (len p)
by FINSEQ_1:def 3;
assume
p is first-line-of-anti-circular
; a * p is first-line-of-anti-circular
then consider M1 being Matrix of len p,K such that
A2:
M1 is_anti-circular_about p
;
A3:
Indices (a * M1) = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
A4:
len (a * p) = len p
by MATRIXR1:16;
A5:
for i, j being Nat st [i,j] in Indices (a * M1) & i >= j holds
(a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1)
proof
len (a * (- p)) = len (- p)
by MATRIXR1:16;
then A6:
dom (a * (- p)) =
Seg (len (- p))
by FINSEQ_1:def 3
.=
dom (- p)
by FINSEQ_1:def 3
;
A7:
a * p is
Element of
(len p) -tuples_on the
carrier of
K
by A4, FINSEQ_2:92;
let i,
j be
Nat;
( [i,j] in Indices (a * M1) & i >= j implies (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) )
assume that A8:
[i,j] in Indices (a * M1)
and A9:
i >= j
;
(a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1)
A10:
((j - i) mod (len p)) + 1
in Seg (len p)
by A3, A8, Lm3;
A11:
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
len (- p) = len p
by CARD_1:def 7;
then A12:
dom (- p) = Seg (len p)
by FINSEQ_1:def 3;
A13:
[i,j] in Indices M1
by A3, A8, MATRIX_0:24;
then (a * M1) * (
i,
j) =
a * (M1 * (i,j))
by MATRIX_3:def 5
.=
(a multfield) . (M1 * (i,j))
by FVSUM_1:49
.=
(a multfield) . ((- p) . (((j - i) mod (len p)) + 1))
by A2, A9, A13
.=
(a multfield) . ((- p) /. (((j - i) mod (len p)) + 1))
by A10, A12, PARTFUN1:def 6
.=
a * ((- p) /. (((j - i) mod (len p)) + 1))
by FVSUM_1:49
.=
(a * (- p)) /. (((j - i) mod (len p)) + 1)
by A10, A12, POLYNOM1:def 1
.=
(a * (- p)) . (((j - i) mod (len p)) + 1)
by A10, A12, A6, PARTFUN1:def 6
.=
(a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1)
by A11, FVSUM_1:59
.=
((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1)
by A11, FVSUM_1:54
.=
((- (a * (1_ K))) * p) . (((j - i) mod (len p)) + 1)
by VECTSP_1:8
.=
((- a) * p) . (((j - i) mod (len p)) + 1)
.=
((- ((1_ K) * a)) * p) . (((j - i) mod (len p)) + 1)
.=
(((- (1_ K)) * a) * p) . (((j - i) mod (len p)) + 1)
by VECTSP_1:9
.=
((- (1_ K)) * (a * p)) . (((j - i) mod (len p)) + 1)
by A11, FVSUM_1:54
.=
(- (a * p)) . (((j - i) mod (len p)) + 1)
by A7, FVSUM_1:59
;
hence
(a * M1) * (
i,
j)
= (- (a * p)) . (((j - i) mod (len (a * p))) + 1)
by MATRIXR1:16;
verum
end;
A14:
dom (a * p) = Seg (len (a * p))
by FINSEQ_1:def 3;
A15:
for i, j being Nat st [i,j] in Indices (a * M1) & i <= j holds
(a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (a * M1) & i <= j implies (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) )
assume that A16:
[i,j] in Indices (a * M1)
and A17:
i <= j
;
(a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
A18:
((j - i) mod (len p)) + 1
in Seg (len p)
by A3, A16, Lm3;
then A19:
((j - i) mod (len p)) + 1
in dom (a * p)
by A14, MATRIXR1:16;
A20:
[i,j] in Indices M1
by A3, A16, MATRIX_0:24;
then (a * M1) * (
i,
j) =
a * (M1 * (i,j))
by MATRIX_3:def 5
.=
(a multfield) . (M1 * (i,j))
by FVSUM_1:49
.=
(a multfield) . (p . (((j - i) mod (len p)) + 1))
by A2, A17, A20
.=
(a multfield) . (p /. (((j - i) mod (len p)) + 1))
by A1, A18, PARTFUN1:def 6
.=
a * (p /. (((j - i) mod (len p)) + 1))
by FVSUM_1:49
.=
(a * p) /. (((j - i) mod (len p)) + 1)
by A1, A18, POLYNOM1:def 1
.=
(a * p) . (((j - i) mod (len p)) + 1)
by A19, PARTFUN1:def 6
;
hence
(a * M1) * (
i,
j)
= (a * p) . (((j - i) mod (len (a * p))) + 1)
by MATRIXR1:16;
verum
end;
width (a * M1) = len p
by MATRIX_0:24;
then
a * M1 is_anti-circular_about a * p
by A4, A15, A5;
then consider M2 being Matrix of len (a * p),K such that
A21:
M2 is_anti-circular_about a * p
by A4;
take
M2
; MATRIX16:def 11 M2 is_anti-circular_about a * p
thus
M2 is_anti-circular_about a * p
by A21; verum