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 that
A1: M1 is Idempotent and
A2: M2 is invertible ; :: thesis: ((M2 ~) * M1) * M2 is Idempotent
A3: M2 ~ is_reverse_of M2 by A2, MATRIX_6:def 4;
A4: width M2 = n by MATRIX_0:24;
A5: len M2 = n by MATRIX_0:24;
A6: ( len (M1 * M2) = n & width (((M2 ~) * M1) * M2) = n ) by MATRIX_0:24;
A7: len (M2 ~) = n by MATRIX_0:24;
A8: width ((M2 ~) * M1) = n by MATRIX_0:24;
A9: width (M2 ~) = n by MATRIX_0:24;
A10: ( len M1 = n & width M1 = n ) by MATRIX_0:24;
then (((M2 ~) * M1) * M2) * (((M2 ~) * M1) * M2) = (((M2 ~) * M1) * M2) * ((M2 ~) * (M1 * M2)) by A5, A9, MATRIX_3:33
.= ((((M2 ~) * M1) * M2) * (M2 ~)) * (M1 * M2) by A7, A9, A6, MATRIX_3:33
.= (((M2 ~) * M1) * (M2 * (M2 ~))) * (M1 * M2) by A5, A4, A7, A8, MATRIX_3:33
.= (((M2 ~) * M1) * (1. (K,n))) * (M1 * M2) by A3, MATRIX_6:def 2
.= ((M2 ~) * M1) * (M1 * M2) by MATRIX_3:19
.= (((M2 ~) * M1) * M1) * M2 by A10, A5, A8, MATRIX_3:33
.= ((M2 ~) * (M1 * M1)) * M2 by A10, A9, MATRIX_3:33
.= ((M2 ~) * M1) * M2 by A1 ;
hence ((M2 ~) * M1) * M2 is Idempotent ; :: thesis: verum