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

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