let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is invertible holds
((M2 ~ ) * M1) * M2 is Idempotent
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is invertible holds
((M2 ~ ) * M1) * M2 is Idempotent
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is Idempotent & M2 is invertible implies ((M2 ~ ) * M1) * M2 is Idempotent )
assume A1: ( M1 is Idempotent & M2 is invertible ) ; :: thesis: ((M2 ~ ) * M1) * M2 is Idempotent
then A2: ( M1 * M1 = M1 & M2 ~ is_reverse_of M2 ) by Def1, MATRIX_6:def 4;
A3: ( len M1 = n & width M1 = n & len M2 = n & width M2 = n & len (M2 ~ ) = n & width (M2 ~ ) = n ) by MATRIX_1:25;
A4: ( len (M1 * M2) = n & width (M1 * M2) = n & len ((M2 ~ ) * M1) = n & width ((M2 ~ ) * M1) = n ) by MATRIX_1:25;
A5: ( len (((M2 ~ ) * M1) * M2) = n & width (((M2 ~ ) * M1) * M2) = n ) by MATRIX_1:25;
(((M2 ~ ) * M1) * M2) * (((M2 ~ ) * M1) * M2) = (((M2 ~ ) * M1) * M2) * ((M2 ~ ) * (M1 * M2)) by A3, MATRIX_3:35
.= ((((M2 ~ ) * M1) * M2) * (M2 ~ )) * (M1 * M2) by A3, A4, A5, MATRIX_3:35
.= (((M2 ~ ) * M1) * (M2 * (M2 ~ ))) * (M1 * M2) by A3, A4, MATRIX_3:35
.= (((M2 ~ ) * M1) * (1. K,n)) * (M1 * M2) by A2, MATRIX_6:def 2
.= ((M2 ~ ) * M1) * (M1 * M2) by MATRIX_3:21
.= (((M2 ~ ) * M1) * M1) * M2 by A3, A4, MATRIX_3:35
.= ((M2 ~ ) * (M1 * M1)) * M2 by A3, MATRIX_3:35
.= ((M2 ~ ) * M1) * M2 by A1, Def1 ;
hence ((M2 ~ ) * M1) * M2 is Idempotent by Def1; :: thesis: verum