let n be Element of NAT ; for K being Field
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 + M2 is line_circulant
let K be Field; for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 + M2 is line_circulant
let M1, M2 be Matrix of n,K; ( M1 is line_circulant & M2 is line_circulant implies M1 + M2 is line_circulant )
assume that
A1:
M1 is line_circulant
and
A2:
M2 is line_circulant
; M1 + M2 is line_circulant
consider p being FinSequence of K such that
A3:
len p = width M1
and
A4:
M1 is_line_circulant_about p
by A1;
A5:
Indices M2 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A6:
Indices (M1 + M2) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A7:
width M1 = n
by MATRIX_0:24;
then A8:
dom p = Seg n
by A3, FINSEQ_1:def 3;
consider q being FinSequence of K such that
A9:
len q = width M2
and
A10:
M2 is_line_circulant_about q
by A2;
A11:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A12:
width M2 = n
by MATRIX_0:24;
then
dom q = Seg n
by A9, FINSEQ_1:def 3;
then A13:
dom (p + q) = dom p
by A8, POLYNOM1:1;
then A14:
len (p + q) = n
by A8, FINSEQ_1:def 3;
A15:
width (M1 + M2) = n
by MATRIX_0:24;
A16:
dom (p + q) = Seg (len (p + q))
by FINSEQ_1:def 3;
for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) )
assume A17:
[i,j] in Indices (M1 + M2)
;
(M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
then A18:
((j - i) mod (len (p + q))) + 1
in dom (p + q)
by A6, A8, A16, A13, Lm3;
(M1 + M2) * (
i,
j) =
(M1 * (i,j)) + (M2 * (i,j))
by A11, A6, A17, MATRIX_3:def 3
.=
the
addF of
K . (
(M1 * (i,j)),
(q . (((j - i) mod (len q)) + 1)))
by A10, A5, A6, A17
.=
the
addF of
K . (
(p . (((j - i) mod (len (p + q))) + 1)),
(q . (((j - i) mod (len (p + q))) + 1)))
by A4, A9, A11, A7, A12, A6, A14, A17
.=
(p + q) . (((j - i) mod (len (p + q))) + 1)
by A18, FUNCOP_1:22
;
hence
(M1 + M2) * (
i,
j)
= (p + q) . (((j - i) mod (len (p + q))) + 1)
;
verum
end;
then
M1 + M2 is_line_circulant_about p + q
by A15, A14;
then consider r being FinSequence of K such that
A19:
( len r = width (M1 + M2) & M1 + M2 is_line_circulant_about r )
;
take
r
; MATRIX16:def 2 ( len r = width (M1 + M2) & M1 + M2 is_line_circulant_about r )
thus
( len r = width (M1 + M2) & M1 + M2 is_line_circulant_about r )
by A19; verum