let n be Nat; for K being Field
for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds
M1 = 1. (K,n)
let K be Field; for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds
M1 = 1. (K,n)
let M1 be Matrix of n,K; ( M1 is invertible & M1 is Idempotent implies M1 = 1. (K,n) )
A1:
( len M1 = n & width M1 = n )
by MATRIX_0:24;
A2:
width (M1 ~) = n
by MATRIX_0:24;
assume A3:
( M1 is invertible & M1 is Idempotent )
; M1 = 1. (K,n)
then A4:
M1 ~ is_reverse_of M1
by MATRIX_6:def 4;
M1 * M1 = M1
by A3;
then 1. (K,n) =
(M1 ~) * (M1 * M1)
by A4, MATRIX_6:def 2
.=
((M1 ~) * M1) * M1
by A1, A2, MATRIX_3:33
.=
(1. (K,n)) * M1
by A4, MATRIX_6:def 2
.=
M1
by MATRIX_3:18
;
hence
M1 = 1. (K,n)
; verum