let K be Field; for a being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (a * p) = a * (CCirc p)
let a be Element of K; for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (a * p) = a * (CCirc p)
let p be FinSequence of K; ( p is first-col-of-circulant implies CCirc (a * p) = a * (CCirc p) )
set n = len p;
A1:
len (a * p) = len p
by MATRIXR1:16;
assume A2:
p is first-col-of-circulant
; CCirc (a * p) = a * (CCirc p)
then
a * p is first-col-of-circulant
by Th46;
then A3:
CCirc (a * p) is_col_circulant_about a * p
by Def8;
A4:
Indices (CCirc p) = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
A5:
CCirc p is_col_circulant_about p
by A2, Def8;
A6:
for i, j being Nat st [i,j] in Indices (CCirc p) holds
(CCirc (a * p)) * (i,j) = a * ((CCirc p) * (i,j))
proof
let i,
j be
Nat;
( [i,j] in Indices (CCirc p) implies (CCirc (a * p)) * (i,j) = a * ((CCirc p) * (i,j)) )
A7:
dom (a * p) = Seg (len (a * p))
by FINSEQ_1:def 3;
assume A8:
[i,j] in Indices (CCirc p)
;
(CCirc (a * p)) * (i,j) = a * ((CCirc p) * (i,j))
then A9:
((i - j) mod (len p)) + 1
in Seg (len p)
by A4, Lm3;
A10:
dom p = Seg (len p)
by FINSEQ_1:def 3;
[i,j] in Indices (CCirc (a * p))
by A1, A8, MATRIX_0:26;
then (CCirc (a * p)) * (
i,
j) =
(a * p) . (((i - j) mod (len (a * p))) + 1)
by A3
.=
(a * p) /. (((i - j) mod (len p)) + 1)
by A1, A9, A7, PARTFUN1:def 6
.=
a * (p /. (((i - j) mod (len p)) + 1))
by A9, A10, POLYNOM1:def 1
.=
(a multfield) . (p /. (((i - j) mod (len p)) + 1))
by FVSUM_1:49
.=
(a multfield) . (p . (((i - j) mod (len p)) + 1))
by A9, A10, PARTFUN1:def 6
.=
(a multfield) . ((CCirc p) * (i,j))
by A5, A8
.=
a * ((CCirc p) * (i,j))
by FVSUM_1:49
;
hence
(CCirc (a * p)) * (
i,
j)
= a * ((CCirc p) * (i,j))
;
verum
end;
A11:
( len (CCirc p) = len p & width (CCirc p) = len p )
by MATRIX_0:24;
( len (CCirc (a * p)) = len p & width (CCirc (a * p)) = len p )
by A1, MATRIX_0:24;
hence
CCirc (a * p) = a * (CCirc p)
by A11, A6, MATRIX_3:def 5; verum