let n be Nat; for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Involutory holds
M1 is Involutory
let K be Field; for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Involutory holds
M1 is Involutory
let M1, M2 be Matrix of n,K; ( M1 is_similar_to M2 & M2 is Involutory implies M1 is Involutory )
assume that
A1:
M1 is_similar_to M2
and
A2:
M2 is Involutory
; M1 is Involutory
consider M4 being Matrix of n,K such that
A3:
M4 is invertible
and
A4:
M1 = ((M4 ~) * M2) * M4
by A1;
A5:
M4 ~ is_reverse_of M4
by A3, MATRIX_6:def 4;
A6:
width ((M4 ~) * M2) = n
by MATRIX_0:24;
A7:
width (M4 ~) = n
by MATRIX_0:24;
A8:
( len (M2 * M4) = n & width (((M4 ~) * M2) * M4) = n )
by MATRIX_0:24;
A9:
len (M4 ~) = n
by MATRIX_0:24;
A10:
width M4 = n
by MATRIX_0:24;
A11:
( len M2 = n & width M2 = n )
by MATRIX_0:24;
A12:
len M4 = n
by MATRIX_0:24;
then M1 * M1 =
(((M4 ~) * M2) * M4) * ((M4 ~) * (M2 * M4))
by A4, A11, A7, MATRIX_3:33
.=
((((M4 ~) * M2) * M4) * (M4 ~)) * (M2 * M4)
by A9, A7, A8, MATRIX_3:33
.=
(((M4 ~) * M2) * (M4 * (M4 ~))) * (M2 * M4)
by A12, A10, A9, A6, MATRIX_3:33
.=
(((M4 ~) * M2) * (1. (K,n))) * (M2 * M4)
by A5, MATRIX_6:def 2
.=
((M4 ~) * M2) * (M2 * M4)
by MATRIX_3:19
.=
(((M4 ~) * M2) * M2) * M4
by A12, A11, A6, MATRIX_3:33
.=
((M4 ~) * (M2 * M2)) * M4
by A11, A7, MATRIX_3:33
.=
((M4 ~) * (1. (K,n))) * M4
by A2
.=
(M4 ~) * M4
by MATRIX_3:19
.=
1. (K,n)
by A5, MATRIX_6:def 2
;
hence
M1 is Involutory
; verum