let n be Element of NAT ; :: thesis: for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
let K be Field; :: thesis: for a being Element of K
for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
let a be Element of K; :: thesis: for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
let M1 be Matrix of n,K; :: thesis: ( M1 is col_circulant implies a * M1 is col_circulant )
assume A1:
M1 is col_circulant
; :: thesis: a * M1 is col_circulant
consider p being FinSequence of K such that
A2:
( len p = len M1 & M1 is_col_circulant_about p )
by A1, Def5;
A4:
( Indices M1 = [:(Seg n),(Seg n):] & len M1 = n & width M1 = n )
by MATRIX_1:25;
A5:
( Indices (a * M1) = [:(Seg n),(Seg n):] & len (a * M1) = n & width (a * M1) = n )
by MATRIX_1:25;
set q = a * p;
A6:
( len (a * p) = len p & len p = n )
by A2, MATRIXR1:16, MATRIX_1:25;
A7:
( dom p = Seg n & dom (a * p) = Seg (len (a * p)) & dom p = Seg (len p) )
by A2, A4, FINSEQ_1:def 3;
for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * i,j = (a * p) . (((i - j) mod (len p)) + 1)
proof
let i,
j be
Nat;
:: thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * i,j = (a * p) . (((i - j) mod (len p)) + 1) )
assume
[i,j] in Indices (a * M1)
;
:: thesis: (a * M1) * i,j = (a * p) . (((i - j) mod (len p)) + 1)
then B2:
[i,j] in Indices M1
by MATRIX_1:27;
then B3:
((i - j) mod (len p)) + 1
in Seg n
by A4, A2, Lm2;
(a * M1) * i,
j =
a * (M1 * i,j)
by B2, MATRIX_3:def 5
.=
(a multfield ) . (M1 * i,j)
by FVSUM_1:61
.=
(a multfield ) . (p . (((i - j) mod (len p)) + 1))
by B2, A2, Def4
.=
(a multfield ) . (p /. (((i - j) mod (len p)) + 1))
by B3, A7, PARTFUN1:def 8
.=
a * (p /. (((i - j) mod (len p)) + 1))
by FVSUM_1:61
.=
(a * p) /. (((i - j) mod (len p)) + 1)
by B3, A7, POLYNOM1:def 2
.=
(a * p) . (((i - j) mod (len p)) + 1)
by B3, A7, A6, PARTFUN1:def 8
;
hence
(a * M1) * i,
j = (a * p) . (((i - j) mod (len p)) + 1)
;
:: thesis: verum
end;
then A9:
a * M1 is_col_circulant_about a * p
by A5, A6, Def4;
set q = a * p;
consider q being FinSequence of K such that
A11:
( len q = len (a * M1) & a * M1 is_col_circulant_about q )
by A5, A6, A9;
take
q
; :: according to MATRIX16:def 5 :: thesis: ( len q = len (a * M1) & a * M1 is_col_circulant_about q )
thus
( len q = len (a * M1) & a * M1 is_col_circulant_about q )
by A11; :: thesis: verum