let M1, M2 be Matrix of n,K; ( ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~) * M2) * M ) implies ex M being Matrix of n,K st
( M is invertible & M2 = ((M ~) * M1) * M ) )
given M being Matrix of n,K such that A1:
M is invertible
and
A2:
M1 = ((M ~) * M2) * M
; ex M being Matrix of n,K st
( M is invertible & M2 = ((M ~) * M1) * M )
A3:
M ~ is_reverse_of M
by A1, MATRIX_6:def 4;
take
M ~
; ( M ~ is invertible & M2 = (((M ~) ~) * M1) * (M ~) )
A4:
width M2 = n
by MATRIX_0:24;
A5:
len M = n
by MATRIX_0:24;
A6:
( len M2 = n & width (M ~) = n )
by MATRIX_0:24;
A7:
width M = n
by MATRIX_0:24;
A8:
( len ((M ~) * M2) = n & width ((M ~) * M2) = n )
by MATRIX_0:24;
A9:
len (M ~) = n
by MATRIX_0:24;
(((M ~) ~) * M1) * (M ~) =
(M * (((M ~) * M2) * M)) * (M ~)
by A1, A2, MATRIX_6:16
.=
((M * ((M ~) * M2)) * M) * (M ~)
by A5, A7, A8, MATRIX_3:33
.=
(((M * (M ~)) * M2) * M) * (M ~)
by A7, A9, A6, MATRIX_3:33
.=
(((1. (K,n)) * M2) * M) * (M ~)
by A3, MATRIX_6:def 2
.=
(M2 * M) * (M ~)
by MATRIX_3:18
.=
M2 * (M * (M ~))
by A4, A5, A7, A9, MATRIX_3:33
.=
M2 * (1. (K,n))
by A3, MATRIX_6:def 2
.=
M2
by MATRIX_3:19
;
hence
( M ~ is invertible & M2 = (((M ~) ~) * M1) * (M ~) )
by A1; verum