let n be Element of NAT ; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is line_circulant holds
- M1 is line_circulant
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is line_circulant holds
- M1 is line_circulant
let M1 be Matrix of n,K; :: thesis: ( M1 is line_circulant implies - M1 is line_circulant )
A1: width M1 = n by MATRIX_1:24;
A2: Indices (- M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume M1 is line_circulant ; :: thesis: - M1 is line_circulant
then consider p being FinSequence of K such that
A3: len p = width M1 and
A4: M1 is_line_circulant_about p by Def2;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then A5: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A6: ( width (- M1) = n & len (- p) = len p ) by CARD_1:def 7, MATRIX_1:24;
A7: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices (- M1) holds
(- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (- M1) implies (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) )
assume A8: [i,j] in Indices (- M1) ; :: thesis: (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
then ((j - i) mod n) + 1 in Seg n by A2, Lm3;
then A9: ((j - i) mod (len p)) + 1 in dom p by A3, A1, FINSEQ_1:def 3;
(- M1) * (i,j) = - (M1 * (i,j)) by A7, A2, A8, MATRIX_3:def 2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def 13
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A4, A7, A2, A8, Def1
.= (- p) . (((j - i) mod (len p)) + 1) by A9, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) by A5, CARD_1:def 7; :: thesis: verum

end;

then - M1 is_line_circulant_about - p by A3, A1, A6, Def1;
then consider r being FinSequence of K such that
A10: ( len r = width (- M1) & - M1 is_line_circulant_about r ) by A3, A6, MATRIX_1:24;
take r ; :: according to MATRIX16:def 2 :: thesis: ( len r = width (- M1) & - M1 is_line_circulant_about r )
thus ( len r = width (- M1) & - M1 is_line_circulant_about r ) by A10; :: thesis: verum