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, Def5;
consider M5 being Matrix of n,K such that
A5: M5 is invertible and
A6: M2 = ((M5 ~ ) * M3) * M5 by A2, Def5;
A7: len M5 = n by MATRIX_1:25;
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_1:25;
A9: ( len (M3 * M5) = n & width (M3 * M5) = n ) by MATRIX_1:25;
A10: len M4 = n by MATRIX_1:25;
A11: width M5 = n by MATRIX_1:25;
A12: len M3 = n by MATRIX_1:25;
A13: len (M5 * M4) = n by MATRIX_1:25;
A14: width (M4 ~ ) = n by MATRIX_1:25;
A15: ( len (M5 ~ ) = n & width (M5 ~ ) = n ) by MATRIX_1:25;
A16: width M3 = n by MATRIX_1:25;
( len ((M5 ~ ) * M3) = n & width ((M5 ~ ) * M3) = n ) by MATRIX_1:25;
then M1 = (((M4 ~ ) * ((M5 ~ ) * M3)) * M5) * M4 by A4, A6, A7, A14, MATRIX_3:35
.= ((((M4 ~ ) * (M5 ~ )) * M3) * M5) * M4 by A12, A14, A15, MATRIX_3:35
.= ((((M5 * M4) ~ ) * M3) * M5) * M4 by A3, A5, MATRIX_6:37
.= (((M5 * M4) ~ ) * (M3 * M5)) * M4 by A12, A16, A7, A8, MATRIX_3:35
.= ((M5 * M4) ~ ) * ((M3 * M5) * M4) by A10, A8, A9, MATRIX_3:35
.= ((M5 * M4) ~ ) * (M3 * (M5 * M4)) by A16, A10, A7, A11, MATRIX_3:35
.= (((M5 * M4) ~ ) * M3) * (M5 * M4) by A12, A16, A8, A13, MATRIX_3:35 ;
hence ( M5 * M4 is invertible & M1 = (((M5 * M4) ~ ) * M3) * (M5 * M4) ) by A3, A5, MATRIX_6:37; :: thesis: verum