let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st n > 0 holds
( M1 is Idempotent iff M1 @ is Idempotent )
let K be Field; :: thesis: for M1 being Matrix of n,K st n > 0 holds
( M1 is Idempotent iff M1 @ is Idempotent )
let M1 be Matrix of n,K; :: thesis: ( n > 0 implies ( M1 is Idempotent iff M1 @ is Idempotent ) )
assume A1: n > 0 ; :: thesis: ( M1 is Idempotent iff M1 @ is Idempotent )
set M2 = M1 @ ;
A2: ( width M1 = n & len M1 = n ) by MATRIX_0:24;
thus ( M1 is Idempotent implies M1 @ is Idempotent ) by A1, A2, MATRIX_3:22; :: thesis: ( M1 @ is Idempotent implies M1 is Idempotent )
A3: ( width (M1 @) = n & len (M1 @) = n ) by MATRIX_0:24;
assume A4: M1 @ is Idempotent ; :: thesis: M1 is Idempotent
M1 = (M1 @) @ by A1, A2, MATRIX_0:57
.= ((M1 @) * (M1 @)) @ by A4
.= ((M1 @) @) * ((M1 @) @) by A1, A3, MATRIX_3:22
.= M1 * ((M1 @) @) by A1, A2, MATRIX_0:57
.= M1 * M1 by A1, A2, MATRIX_0:57 ;
hence M1 is Idempotent ; :: thesis: verum