let M1 be Matrix of n,K; ( M1 = a * M implies M1 is subsymmetric )
assume A1:
M1 = a * M
; M1 is subsymmetric
A2:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
let i, j, k, l be Nat; MATRIX17:def 1 ( [i,j] in Indices M1 & k = (n + 1) - j & l = (n + 1) - i implies M1 * (i,j) = M1 * (k,l) )
assume that
A3:
[i,j] in Indices M1
and
A4:
( k = (n + 1) - j & l = (n + 1) - i )
; M1 * (i,j) = M1 * (k,l)
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
( k in Seg n & l in Seg n )
by A3, A4, Lm2;
then A5:
[k,l] in [:(Seg n),(Seg n):]
by ZFMISC_1:87;
A6:
[i,j] in Indices M
by A2, A3, MATRIX_0:24;
then (a * M) * (i,j) =
a * (M * (i,j))
by MATRIX_3:def 5
.=
a * (M * (k,l))
by A4, A6, Def1
.=
(a * M) * (k,l)
by A2, A5, MATRIX_3:def 5
;
hence
M1 * (i,j) = M1 * (k,l)
by A1; verum