let M be Matrix of n,K; :: thesis: ( M is line_circulant implies M is subsymmetric )

assume M is line_circulant ; :: thesis: M is subsymmetric

then consider p being FinSequence of K such that

len p = width M and

A1: M is_line_circulant_about p by MATRIX16:def 2;

A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;

let i, j, k, l be Nat; :: according to MATRIX17:def 1 :: thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = M * (k,l) )

assume that

A3: [i,j] in Indices M and

A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; :: thesis: M * (i,j) = M * (k,l)

( k in Seg n & l in Seg n ) by A3, A2, A4, Lm2;

then A5: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;

M * (k,l) = p . (((((n + 1) - i) - ((n + 1) - j)) mod (len p)) + 1) by A1, A2, A4, A5, MATRIX16:def 1

.= p . (((j - i) mod (len p)) + 1) ;

hence M * (i,j) = M * (k,l) by A3, A1, MATRIX16:def 1; :: thesis: verum

assume M is line_circulant ; :: thesis: M is subsymmetric

then consider p being FinSequence of K such that

len p = width M and

A1: M is_line_circulant_about p by MATRIX16:def 2;

A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;

let i, j, k, l be Nat; :: according to MATRIX17:def 1 :: thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = M * (k,l) )

assume that

A3: [i,j] in Indices M and

A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; :: thesis: M * (i,j) = M * (k,l)

( k in Seg n & l in Seg n ) by A3, A2, A4, Lm2;

then A5: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;

M * (k,l) = p . (((((n + 1) - i) - ((n + 1) - j)) mod (len p)) + 1) by A1, A2, A4, A5, MATRIX16:def 1

.= p . (((j - i) mod (len p)) + 1) ;

hence M * (i,j) = M * (k,l) by A3, A1, MATRIX16:def 1; :: thesis: verum