let n be Nat; :: thesis: for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is_similar_to M2 & M2 is_similar_to M3 holds
M1 is_similar_to M3
let K be Field; :: thesis: for M1, M2, M3 being Matrix of n,K st M1 is_similar_to M2 & M2 is_similar_to M3 holds
M1 is_similar_to M3
let M1, M2, M3 be Matrix of n,K; :: thesis: ( M1 is_similar_to M2 & M2 is_similar_to M3 implies M1 is_similar_to M3 )
assume that
A1: M1 is_similar_to M2 and
A2: M2 is_similar_to M3 ; :: thesis: M1 is_similar_to M3
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 ~) * M2) * M4 by A1;
consider M5 being Matrix of n,K such that
A5: M5 is invertible and
A6: M2 = ((M5 ~) * M3) * M5 by A2;
A7: len M5 = n by MATRIX_0:24;
take M5 * M4 ; :: according to MATRIX_8:def 5 :: thesis: ( M5 * M4 is invertible & M1 = (((M5 * M4) ~) * M3) * (M5 * M4) )
A8: width ((M5 * M4) ~) = n by MATRIX_0:24;
A9: ( len (M3 * M5) = n & width (M3 * M5) = n ) by MATRIX_0:24;
A10: len M4 = n by MATRIX_0:24;
A11: width M5 = n by MATRIX_0:24;
A12: len M3 = n by MATRIX_0:24;
A13: len (M5 * M4) = n by MATRIX_0:24;
A14: width (M4 ~) = n by MATRIX_0:24;
A15: ( len (M5 ~) = n & width (M5 ~) = n ) by MATRIX_0:24;
A16: width M3 = n by MATRIX_0:24;
( len ((M5 ~) * M3) = n & width ((M5 ~) * M3) = n ) by MATRIX_0:24;
then M1 = (((M4 ~) * ((M5 ~) * M3)) * M5) * M4 by A4, A6, A7, A14, MATRIX_3:33
.= ((((M4 ~) * (M5 ~)) * M3) * M5) * M4 by A12, A14, A15, MATRIX_3:33
.= ((((M5 * M4) ~) * M3) * M5) * M4 by A3, A5, MATRIX_6:36
.= (((M5 * M4) ~) * (M3 * M5)) * M4 by A12, A16, A7, A8, MATRIX_3:33
.= ((M5 * M4) ~) * ((M3 * M5) * M4) by A10, A8, A9, MATRIX_3:33
.= ((M5 * M4) ~) * (M3 * (M5 * M4)) by A16, A10, A7, A11, MATRIX_3:33
.= (((M5 * M4) ~) * M3) * (M5 * M4) by A12, A16, A8, A13, MATRIX_3:33 ;
hence ( M5 * M4 is invertible & M1 = (((M5 * M4) ~) * M3) * (M5 * M4) ) by A3, A5, MATRIX_6:36; :: thesis: verum