let K be Field; for a being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
a * p is first-line-of-circulant
let a be Element of K; for p being FinSequence of K st p is first-line-of-circulant holds
a * p is first-line-of-circulant
let p be FinSequence of K; ( p is first-line-of-circulant implies a * p is first-line-of-circulant )
set n = len p;
A1:
len (a * p) = len p
by MATRIXR1:16;
assume
p is first-line-of-circulant
; a * p is first-line-of-circulant
then consider M1 being Matrix of len p,K such that
A2:
M1 is_line_circulant_about p
;
A3:
Indices (a * M1) = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
A4:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A5:
dom (a * p) = Seg (len (a * p))
by FINSEQ_1:def 3;
A6:
for i, j being Nat st [i,j] in Indices (a * M1) 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) implies (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) )
assume A7:
[i,j] in Indices (a * M1)
;
(a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
then A8:
((j - i) mod (len p)) + 1
in Seg (len p)
by A3, Lm3;
then A9:
((j - i) mod (len p)) + 1
in dom (a * p)
by A5, MATRIXR1:16;
A10:
[i,j] in Indices M1
by A3, A7, 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, A10
.=
(a multfield) . (p /. (((j - i) mod (len p)) + 1))
by A4, A8, PARTFUN1:def 6
.=
a * (p /. (((j - i) mod (len p)) + 1))
by FVSUM_1:49
.=
(a * p) /. (((j - i) mod (len p)) + 1)
by A4, A8, POLYNOM1:def 1
.=
(a * p) . (((j - i) mod (len p)) + 1)
by A9, 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_line_circulant_about a * p
by A1, A6;
then consider M2 being Matrix of len (a * p),K such that
A11:
M2 is_line_circulant_about a * p
by A1;
take
M2
; MATRIX16:def 3 M2 is_line_circulant_about a * p
thus
M2 is_line_circulant_about a * p
by A11; verum