let n be Nat; for K being Field
for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 holds
(M1 @) * (M2 @) is Idempotent
let K be Field; for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 holds
(M1 @) * (M2 @) is Idempotent
let M1, M2 be Matrix of n,K; ( M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies (M1 @) * (M2 @) is Idempotent )
assume that
A1:
M1 is Idempotent
and
A2:
M2 is Idempotent
and
A3:
M1 commutes_with M2
; (M1 @) * (M2 @) is Idempotent
set M3 = (M1 @) * (M2 @);
per cases
( n > 0 or n = 0 )
by NAT_1:3;
suppose A4:
n > 0
;
(M1 @) * (M2 @) is Idempotent A5:
M1 * M1 = M1
by A1;
A6:
len M1 = n
by MATRIX_0:24;
A7:
len (M1 @) = n
by MATRIX_0:24;
A8:
width (M2 @) = n
by MATRIX_0:24;
A9:
width M2 = n
by MATRIX_0:24;
A10:
len M2 = n
by MATRIX_0:24;
A11:
width M1 = n
by MATRIX_0:24;
A12:
(
width (M1 @) = n &
len (M2 @) = n )
by MATRIX_0:24;
width ((M1 @) * (M2 @)) = n
by MATRIX_0:24;
then ((M1 @) * (M2 @)) * ((M1 @) * (M2 @)) =
(((M1 @) * (M2 @)) * (M1 @)) * (M2 @)
by A7, A12, MATRIX_3:33
.=
((M1 @) * ((M2 @) * (M1 @))) * (M2 @)
by A7, A12, A8, MATRIX_3:33
.=
((M1 @) * ((M1 * M2) @)) * (M2 @)
by A4, A11, A10, A9, MATRIX_3:22
.=
((M1 @) * ((M2 * M1) @)) * (M2 @)
by A3, MATRIX_6:def 1
.=
((M1 @) * ((M1 @) * (M2 @))) * (M2 @)
by A4, A6, A11, A9, MATRIX_3:22
.=
(((M1 @) * (M1 @)) * (M2 @)) * (M2 @)
by A7, A12, MATRIX_3:33
.=
(((M1 * M1) @) * (M2 @)) * (M2 @)
by A4, A6, A11, MATRIX_3:22
.=
(M1 @) * ((M2 @) * (M2 @))
by A5, A12, A8, MATRIX_3:33
.=
(M1 @) * ((M2 * M2) @)
by A4, A10, A9, MATRIX_3:22
.=
(M1 @) * (M2 @)
by A2
;
hence
(M1 @) * (M2 @) is
Idempotent
;
verum end; end;