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

assume M is col_circulant ; :: thesis: M is subsymmetric

then consider p being FinSequence of K such that

A6: len p = len M and

A7: M is_col_circulant_about p by MATRIX16:def 5;

A8: len M = n by MATRIX_0:24;

A9: 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

A10: [i,j] in Indices M and

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

( k in Seg n & l in Seg n ) by A10, A9, A11, Lm2;

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

M * (k,l) = p . (((((n + 1) - j) - ((n + 1) - i)) mod n) + 1) by A6, A7, A8, A9, A11, A12, MATRIX16:def 4

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

hence M * (i,j) = M * (k,l) by A6, A7, A8, A10, MATRIX16:def 4; :: thesis: verum

assume M is col_circulant ; :: thesis: M is subsymmetric

then consider p being FinSequence of K such that

A6: len p = len M and

A7: M is_col_circulant_about p by MATRIX16:def 5;

A8: len M = n by MATRIX_0:24;

A9: 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

A10: [i,j] in Indices M and

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

( k in Seg n & l in Seg n ) by A10, A9, A11, Lm2;

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

M * (k,l) = p . (((((n + 1) - j) - ((n + 1) - i)) mod n) + 1) by A6, A7, A8, A9, A11, A12, MATRIX16:def 4

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

hence M * (i,j) = M * (k,l) by A6, A7, A8, A10, MATRIX16:def 4; :: thesis: verum