:: MATRIX_8 semantic presentation

begin


definition
let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
attrM1 is Idempotent  means :Def1: :: MATRIX_8:def 1
M1 * M1 = M1;
attrM1 is Nilpotent  means :Def2: :: MATRIX_8:def 2
M1 * M1 = 0. (K,n);
attrM1 is Involutory  means :Def3: :: MATRIX_8:def 3
M1 * M1 = 1. (K,n);
attrM1 is Self_Reversible  means :Def4: :: MATRIX_8:def 4
( M1 is invertible & M1 ~ = M1 );
end;

:: deftheorem Def1 defines Idempotent MATRIX_8:def_1_:_
 for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( M1 is Idempotent iff M1 * M1 = M1 );

:: deftheorem Def2 defines Nilpotent MATRIX_8:def_2_:_
 for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( M1 is Nilpotent iff M1 * M1 = 0. (K,n) );

:: deftheorem Def3 defines Involutory MATRIX_8:def_3_:_
 for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( M1 is Involutory iff M1 * M1 = 1. (K,n) );

:: deftheorem Def4 defines Self_Reversible MATRIX_8:def_4_:_
 for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( M1 is Self_Reversible iff ( M1 is invertible & M1 ~ = M1 ) );

theorem Th1: :: MATRIX_8:1
for n being Nat
for K being Field holds
( 1. (K,n) is Idempotent & 1. (K,n) is Involutory )
proof
let n be Nat; ::_thesis: for K being Field holds
( 1. (K,n) is Idempotent & 1. (K,n) is Involutory )
let K be Field; ::_thesis: ( 1. (K,n) is Idempotent & 1. (K,n) is Involutory )
 (1. (K,n)) * (1. (K,n)) = 1. (K,n) by MATRIX_3:18;
hence  ( 1. (K,n) is Idempotent & 1. (K,n) is Involutory ) by Def1, Def3; ::_thesis: verum
end;

theorem Th2: :: MATRIX_8:2
for n being Nat
for K being Field holds
( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent )
proof
let n be Nat; ::_thesis: for K being Field holds
( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent )
let K be Field; ::_thesis: ( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent )
 ( width (0. (K,n,n)) = n & len (0. (K,n,n)) = n ) by MATRIX_1:24;
then  (0. (K,n,n)) * (0. (K,n)) = 0. (K,n,n) by MATRIX_6:1;
hence  ( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent ) by Def1, Def2; ::_thesis: verum
end;

registration
let n be Nat;
let K be Field;
cluster 1. (K,n) ->  Idempotent Involutory ;
coherence
 ( 1. (K,n) is Idempotent & 1. (K,n) is Involutory ) by Th1;
cluster 0. (K,n) ->  Idempotent Nilpotent ;
coherence
 ( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent ) by Th2;
end;

theorem :: MATRIX_8:3
for n being Nat
for K being Field
for M1 being Matrix of n,K st n > 0 holds
( M1 is Idempotent iff M1 @ is Idempotent )
proof
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_1:24;
thus  ( M1 is Idempotent implies M1 @ is Idempotent ) ::_thesis: ( M1 @ is Idempotent implies M1 is Idempotent )
proof
assume A3: M1 is Idempotent ; ::_thesis: M1 @ is Idempotent
(M1 @) * (M1 @) = (M1 * M1) @ by A1, A2, MATRIX_3:22
.= M1 @ by A3, Def1 ;
hence  M1 @ is Idempotent by Def1; ::_thesis: verum
end;
A4: ( width (M1 @) = n & len (M1 @) = n ) by MATRIX_1:24;
assume A5: M1 @ is Idempotent ; ::_thesis: M1 is Idempotent
M1 = (M1 @) @ by A1, A2, MATRIX_2:13
.= ((M1 @) * (M1 @)) @ by A5, Def1
.= ((M1 @) @) * ((M1 @) @) by A1, A4, MATRIX_3:22
.= M1 * ((M1 @) @) by A1, A2, MATRIX_2:13
.= M1 * M1 by A1, A2, MATRIX_2:13 ;
hence  M1 is Idempotent by Def1; ::_thesis: verum
end;

theorem :: MATRIX_8:4
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Involutory holds
M1 is invertible
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is Involutory holds
M1 is invertible
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Involutory holds
M1 is invertible
let M1 be Matrix of n,K; ::_thesis: ( M1 is Involutory implies M1 is invertible )
assume  M1 is Involutory ; ::_thesis: M1 is invertible
then  M1 * M1 = 1. (K,n) by Def3;
then  M1 is_reverse_of M1 by MATRIX_6:def_2;
hence  M1 is invertible by MATRIX_6:def_3; ::_thesis: verum
end;

theorem :: MATRIX_8:5
for n being 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 * M1 commutes_with M2 * M2
proof
let n be Nat; ::_thesis: 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 * M1 commutes_with M2 * M2
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 holds
M1 * M1 commutes_with M2 * M2
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies M1 * M1 commutes_with M2 * M2 )
assume that
A1: M1 is Idempotent and
A2: ( M2 is Idempotent & M1 commutes_with M2 ) ; ::_thesis: M1 * M1 commutes_with M2 * M2
 M1 * M1 = M1 by A1, Def1;
hence  M1 * M1 commutes_with M2 * M2 by A2, Def1; ::_thesis: verum
end;

theorem :: MATRIX_8:6
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds
M1 + M2 is Idempotent
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds
M1 + M2 is Idempotent
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds
M1 + M2 is Idempotent
let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) implies M1 + M2 is Idempotent )
assume that
A1: n > 0 and
A2: ( M1 is Idempotent & M2 is Idempotent ) and
A3: M1 commutes_with M2 and
A4: M1 * M2 = 0. (K,n) ; ::_thesis: M1 + M2 is Idempotent
A5: M1 * M2 = 0. (K,n,n) by A4;
A6: ( M1 * M1 = M1 & M2 * M2 = M2 ) by A2, Def1;
(M1 + M2) * (M1 + M2) = (((M1 * M1) + (0. (K,n))) + (0. (K,n))) + (M2 * M2) by A1, A3, A4, MATRIX_6:35
.= ((M1 * M1) + (0. (K,n))) + (M2 * M2) by A5, MATRIX_3:4
.= M1 + M2 by A6, A5, MATRIX_3:4 ;
hence  M1 + M2 is Idempotent by Def1; ::_thesis: verum
end;

theorem :: MATRIX_8:7
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 * M2 = - (M2 * M1) holds
M1 + M2 is Idempotent
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 * M2 = - (M2 * M1) holds
M1 + M2 is Idempotent
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 * M2 = - (M2 * M1) holds
M1 + M2 is Idempotent
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is Idempotent & M2 is Idempotent & M1 * M2 = - (M2 * M1) implies M1 + M2 is Idempotent )
assume that
A1: ( M1 is Idempotent & M2 is Idempotent ) and
A2: M1 * M2 = - (M2 * M1) ; ::_thesis: M1 + M2 is Idempotent
A3: ( M1 * M1 = M1 & M2 * M2 = M2 ) by A1, Def1;
percases ( n > 0 or n = 0 ) by NAT_1:3;
supposeA4: n > 0 ; ::_thesis: M1 + M2 is Idempotent
A5: ( len (M1 * M2) = n & width (M1 * M2) = n ) by MATRIX_1:24;
A6: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
A7: ( len ((M1 * M1) + (M2 * M1)) = n & width ((M1 * M1) + (M2 * M1)) = n ) by MATRIX_1:24;
A8: ( len (M2 * M1) = n & width (M2 * M1) = n ) by MATRIX_1:24;
A9: ( len (M1 * M1) = n & width (M1 * M1) = n ) by MATRIX_1:24;
A10: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
 ( len (M1 + M2) = n & width (M1 + M2) = n ) by MATRIX_1:24;
then (M1 + M2) * (M1 + M2) = ((M1 + M2) * M1) + ((M1 + M2) * M2) by A4, A10, A6, MATRIX_4:62
.= ((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2) by A4, A10, A6, MATRIX_4:63
.= ((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) by A4, A10, A6, MATRIX_4:63
.= (((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2) by A5, A7, MATRIX_3:3
.= ((M1 * M1) + ((M2 * M1) + (- (M2 * M1)))) + (M2 * M2) by A2, A9, A8, MATRIX_3:3
.= ((M1 * M1) + (0. (K,n,n))) + (M2 * M2) by A8, MATRIX_4:2
.= M1 + M2 by A3, MATRIX_3:4 ;
hence  M1 + M2 is Idempotent by Def1; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: M1 + M2 is Idempotent
then  (M1 + M2) * (M1 + M2) = M1 + M2 by MATRIX_1:35;
hence  M1 + M2 is Idempotent by Def1; ::_thesis: verum
end;
end;
end;

theorem :: MATRIX_8:8
for n being Nat
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
proof
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_1:24;
A5: len M2 = n by MATRIX_1:24;
A6: ( len (M1 * M2) = n & width (((M2 ~) * M1) * M2) = n ) by MATRIX_1:24;
A7: len (M2 ~) = n by MATRIX_1:24;
A8: width ((M2 ~) * M1) = n by MATRIX_1:24;
A9: width (M2 ~) = n by MATRIX_1:24;
A10: ( len M1 = n & width M1 = n ) by MATRIX_1: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, Def1 ;
hence  ((M2 ~) * M1) * M2 is Idempotent by Def1; ::_thesis: verum
end;

theorem :: MATRIX_8:9
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds
M1 ~ is Idempotent
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds
M1 ~ is Idempotent
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds
M1 ~ is Idempotent
let M1 be Matrix of n,K; ::_thesis: ( M1 is invertible & M1 is Idempotent implies M1 ~ is Idempotent )
assume A1: ( M1 is invertible & M1 is Idempotent ) ; ::_thesis: M1 ~ is Idempotent
then M1 ~ = (M1 * M1) ~ by Def1
.= (M1 ~) * (M1 ~) by A1, MATRIX_6:36 ;
hence  M1 ~ is Idempotent by Def1; ::_thesis: verum
end;

theorem Th10: :: MATRIX_8:10
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds
M1 = 1. (K,n)
proof
let n be Nat; ::_thesis: 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; ::_thesis: 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; ::_thesis: ( M1 is invertible & M1 is Idempotent implies M1 = 1. (K,n) )
A1: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
A2: width (M1 ~) = n by MATRIX_1:24;
assume A3: ( M1 is invertible & M1 is Idempotent ) ; ::_thesis: M1 = 1. (K,n)
then A4: M1 ~ is_reverse_of M1 by MATRIX_6:def_4;
 M1 * M1 = M1 by A3, Def1;
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) ; ::_thesis: verum
end;

theorem :: MATRIX_8:11
for n being 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
proof
let n be Nat; ::_thesis: 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; ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: M1 * M2 is Idempotent
A4: len M1 = n by MATRIX_1:24;
A5: width M2 = n by MATRIX_1:24;
A6: ( width M1 = n & len M2 = n ) by MATRIX_1:24;
 width (M1 * M2) = n by MATRIX_1:24;
then (M1 * M2) * (M1 * M2) = ((M1 * M2) * M1) * M2 by A4, A6, MATRIX_3:33
.= (M1 * (M2 * M1)) * M2 by A4, A6, A5, MATRIX_3:33
.= (M1 * (M1 * M2)) * M2 by A3, MATRIX_6:def_1
.= ((M1 * M1) * M2) * M2 by A4, A6, MATRIX_3:33
.= (M1 * M2) * M2 by A1, Def1
.= M1 * (M2 * M2) by A6, A5, MATRIX_3:33
.= M1 * M2 by A2, Def1 ;
hence  M1 * M2 is Idempotent by Def1; ::_thesis: verum
end;

theorem :: MATRIX_8:12
for n being 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
proof
let n be Nat; ::_thesis: 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; ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: (M1 @) * (M2 @) is Idempotent
set M3 = (M1 @) * (M2 @);
percases ( n > 0 or n = 0 ) by NAT_1:3;
supposeA4: n > 0 ; ::_thesis: (M1 @) * (M2 @) is Idempotent
A5: M1 * M1 = M1 by A1, Def1;
A6: len M1 = n by MATRIX_1:24;
A7: len (M1 @) = n by MATRIX_1:24;
A8: width (M2 @) = n by MATRIX_1:24;
A9: width M2 = n by MATRIX_1:24;
A10: len M2 = n by MATRIX_1:24;
A11: width M1 = n by MATRIX_1:24;
A12: ( width (M1 @) = n & len (M2 @) = n ) by MATRIX_1:24;
 width ((M1 @) * (M2 @)) = n by MATRIX_1: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, Def1 ;
hence  (M1 @) * (M2 @) is Idempotent by Def1; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: (M1 @) * (M2 @) is Idempotent
then  ((M1 @) * (M2 @)) * ((M1 @) * (M2 @)) = (M1 @) * (M2 @) by MATRIX_1:35;
hence  (M1 @) * (M2 @) is Idempotent by Def1; ::_thesis: verum
end;
end;
end;

theorem :: MATRIX_8:13
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 is invertible holds
M1 * M2 is Idempotent
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 is invertible holds
M1 * M2 is Idempotent
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 is invertible holds
M1 * M2 is Idempotent
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is Idempotent & M2 is Idempotent & M1 is invertible implies M1 * M2 is Idempotent )
assume that
A1: M1 is Idempotent and
A2: M2 is Idempotent and
A3: M1 is invertible ; ::_thesis: M1 * M2 is Idempotent
 M1 = 1. (K,n) by A1, A3, Th10;
hence  M1 * M2 is Idempotent by A2, MATRIX_3:18; ::_thesis: verum
end;

theorem :: MATRIX_8:14
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds
M1 is symmetric
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds
M1 is symmetric
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds
M1 is symmetric
let M1 be Matrix of n,K; ::_thesis: ( M1 is Idempotent & M1 is Orthogonal implies M1 is symmetric )
assume A1: ( M1 is Idempotent & M1 is Orthogonal ) ; ::_thesis: M1 is symmetric
then  M1 is invertible by MATRIX_6:def_7;
then  M1 = 1. (K,n) by A1, Th10;
hence  M1 is symmetric ; ::_thesis: verum
end;

theorem :: MATRIX_8:15
for n being Nat
for K being Field
for M2, M1 being Matrix of n,K st M2 * M1 = 1. (K,n) holds
M1 * M2 is Idempotent
proof
let n be Nat; ::_thesis: for K being Field
for M2, M1 being Matrix of n,K st M2 * M1 = 1. (K,n) holds
M1 * M2 is Idempotent
let K be Field; ::_thesis: for M2, M1 being Matrix of n,K st M2 * M1 = 1. (K,n) holds
M1 * M2 is Idempotent
let M2, M1 be Matrix of n,K; ::_thesis: ( M2 * M1 = 1. (K,n) implies M1 * M2 is Idempotent )
assume A1: M2 * M1 = 1. (K,n) ; ::_thesis: M1 * M2 is Idempotent
A2: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
A3: width M2 = n by MATRIX_1:24;
A4: len M2 = n by MATRIX_1:24;
 width (M1 * M2) = n by MATRIX_1:24;
then (M1 * M2) * (M1 * M2) = ((M1 * M2) * M1) * M2 by A2, A4, MATRIX_3:33
.= (M1 * (1. (K,n))) * M2 by A1, A2, A4, A3, MATRIX_3:33
.= M1 * M2 by MATRIX_3:19 ;
hence  M1 * M2 is Idempotent by Def1; ::_thesis: verum
end;

theorem :: MATRIX_8:16
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds
M1 = 1. (K,n)
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds
M1 = 1. (K,n)
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds
M1 = 1. (K,n)
let M1 be Matrix of n,K; ::_thesis: ( M1 is Idempotent & M1 is Orthogonal implies M1 = 1. (K,n) )
assume A1: ( M1 is Idempotent & M1 is Orthogonal ) ; ::_thesis: M1 = 1. (K,n)
then  M1 is invertible by MATRIX_6:def_7;
hence  M1 = 1. (K,n) by A1, Th10; ::_thesis: verum
end;

theorem :: MATRIX_8:17
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is symmetric holds
M1 * (M1 @) is symmetric
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is symmetric holds
M1 * (M1 @) is symmetric
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is symmetric holds
M1 * (M1 @) is symmetric
let M1 be Matrix of n,K; ::_thesis: ( M1 is symmetric implies M1 * (M1 @) is symmetric )
assume A1: M1 is symmetric ; ::_thesis: M1 * (M1 @) is symmetric
percases ( n > 0 or n = 0 ) by NAT_1:3;
supposeA2: n > 0 ; ::_thesis: M1 * (M1 @) is symmetric
A3: ( width M1 = n & len M1 = n ) by MATRIX_1:24;
(M1 * (M1 @)) @ = (M1 * M1) @ by A1, MATRIX_6:def_5
.= (M1 @) * (M1 @) by A2, A3, MATRIX_3:22
.= M1 * (M1 @) by A1, MATRIX_6:def_5 ;
hence  M1 * (M1 @) is symmetric by MATRIX_6:def_5; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: M1 * (M1 @) is symmetric
then  (M1 * (M1 @)) @ = M1 * (M1 @) by MATRIX_1:35;
hence  M1 * (M1 @) is symmetric by MATRIX_6:def_5; ::_thesis: verum
end;
end;
end;

theorem :: MATRIX_8:18
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is symmetric holds
(M1 @) * M1 is symmetric
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is symmetric holds
(M1 @) * M1 is symmetric
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is symmetric holds
(M1 @) * M1 is symmetric
let M1 be Matrix of n,K; ::_thesis: ( M1 is symmetric implies (M1 @) * M1 is symmetric )
assume A1: M1 is symmetric ; ::_thesis: (M1 @) * M1 is symmetric
percases ( n > 0 or n = 0 ) by NAT_1:3;
supposeA2: n > 0 ; ::_thesis: (M1 @) * M1 is symmetric
A3: ( width M1 = n & len M1 = n ) by MATRIX_1:24;
((M1 @) * M1) @ = (M1 * M1) @ by A1, MATRIX_6:def_5
.= (M1 @) * (M1 @) by A2, A3, MATRIX_3:22
.= (M1 @) * M1 by A1, MATRIX_6:def_5 ;
hence  (M1 @) * M1 is symmetric by MATRIX_6:def_5; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: (M1 @) * M1 is symmetric
then  ((M1 @) * M1) @ = (M1 @) * M1 by MATRIX_1:35;
hence  (M1 @) * M1 is symmetric by MATRIX_6:def_5; ::_thesis: verum
end;
end;
end;

theorem :: MATRIX_8:19
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is invertible & M1 * M2 = M1 * M3 holds
M2 = M3
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is invertible & M1 * M2 = M1 * M3 holds
M2 = M3
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is invertible & M1 * M2 = M1 * M3 holds
M2 = M3
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is invertible & M1 * M2 = M1 * M3 implies M2 = M3 )
assume that
A1: M1 is invertible and
A2: M1 * M2 = M1 * M3 ; ::_thesis: M2 = M3
A3: M1 ~ is_reverse_of M1 by A1, MATRIX_6:def_4;
A4: len M2 = n by MATRIX_1:24;
A5: ( width M1 = n & len M1 = n ) by MATRIX_1:24;
A6: len M3 = n by MATRIX_1:24;
A7: width (M1 ~) = n by MATRIX_1:24;
M2 = (1. (K,n)) * M2 by MATRIX_3:18
.= ((M1 ~) * M1) * M2 by A3, MATRIX_6:def_2
.= (M1 ~) * (M1 * M3) by A2, A5, A4, A7, MATRIX_3:33
.= ((M1 ~) * M1) * M3 by A5, A6, A7, MATRIX_3:33
.= (1. (K,n)) * M3 by A3, MATRIX_6:def_2
.= M3 by MATRIX_3:18 ;
hence  M2 = M3 ; ::_thesis: verum
end;

theorem :: MATRIX_8:20
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 * M1 = M3 * M1 holds
M2 = M3
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 * M1 = M3 * M1 holds
M2 = M3
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 * M1 = M3 * M1 holds
M2 = M3
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is invertible & M2 * M1 = M3 * M1 implies M2 = M3 )
assume that
A1: M1 is invertible and
A2: M2 * M1 = M3 * M1 ; ::_thesis: M2 = M3
A3: M1 ~ is_reverse_of M1 by A1, MATRIX_6:def_4;
A4: width M2 = n by MATRIX_1:24;
A5: ( width M1 = n & len M1 = n ) by MATRIX_1:24;
A6: width M3 = n by MATRIX_1:24;
A7: len (M1 ~) = n by MATRIX_1:24;
M2 = M2 * (1. (K,n)) by MATRIX_3:19
.= M2 * (M1 * (M1 ~)) by A3, MATRIX_6:def_2
.= (M3 * M1) * (M1 ~) by A2, A5, A4, A7, MATRIX_3:33
.= M3 * (M1 * (M1 ~)) by A5, A6, A7, MATRIX_3:33
.= M3 * (1. (K,n)) by A3, MATRIX_6:def_2
.= M3 by MATRIX_3:19 ;
hence  M2 = M3 ; ::_thesis: verum
end;

theorem :: MATRIX_8:21
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds
M2 = 0. (K,n)
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds
M2 = 0. (K,n)
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds
M2 = 0. (K,n)
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is invertible & M2 * M1 = 0. (K,n) implies M2 = 0. (K,n) )
assume that
A1: M1 is invertible and
A2: M2 * M1 = 0. (K,n) ; ::_thesis: M2 = 0. (K,n)
A3: M1 ~ is_reverse_of M1 by A1, MATRIX_6:def_4;
A4: width M2 = n by MATRIX_1:24;
A5: ( width M1 = n & len M1 = n ) by MATRIX_1:24;
A6: width (M1 ~) = n by MATRIX_1:24;
A7: len (M1 ~) = n by MATRIX_1:24;
M2 = M2 * (1. (K,n)) by MATRIX_3:19
.= M2 * (M1 * (M1 ~)) by A3, MATRIX_6:def_2
.= (M2 * M1) * (M1 ~) by A5, A4, A7, MATRIX_3:33
.= 0. (K,n,n) by A2, A6, A7, MATRIX_6:1
.= 0. (K,n) ;
hence  M2 = 0. (K,n) ; ::_thesis: verum
end;

theorem :: MATRIX_8:22
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds
M2 = 0. (K,n)
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds
M2 = 0. (K,n)
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds
M2 = 0. (K,n)
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is invertible & M2 * M1 = 0. (K,n) implies M2 = 0. (K,n) )
assume that
A1: M1 is invertible and
A2: M2 * M1 = 0. (K,n) ; ::_thesis: M2 = 0. (K,n)
A3: M1 ~ is_reverse_of M1 by A1, MATRIX_6:def_4;
A4: width M2 = n by MATRIX_1:24;
A5: ( width M1 = n & len M1 = n ) by MATRIX_1:24;
A6: width (M1 ~) = n by MATRIX_1:24;
A7: len (M1 ~) = n by MATRIX_1:24;
M2 = M2 * (1. (K,n)) by MATRIX_3:19
.= M2 * (M1 * (M1 ~)) by A3, MATRIX_6:def_2
.= (M2 * M1) * (M1 ~) by A5, A4, A7, MATRIX_3:33
.= 0. (K,n,n) by A2, A6, A7, MATRIX_6:1
.= 0. (K,n) ;
hence  M2 = 0. (K,n) ; ::_thesis: verum
end;

theorem :: MATRIX_8:23
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is Nilpotent & M1 commutes_with M2 & n > 0 holds
M1 * M2 is Nilpotent
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is Nilpotent & M1 commutes_with M2 & n > 0 holds
M1 * M2 is Nilpotent
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is Nilpotent & M1 commutes_with M2 & n > 0 holds
M1 * M2 is Nilpotent
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is Nilpotent & M1 commutes_with M2 & n > 0 implies M1 * M2 is Nilpotent )
assume that
A1: M1 is Nilpotent and
A2: M1 commutes_with M2 and
A3: n > 0 ; ::_thesis: M1 * M2 is Nilpotent
A4: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
A5: width M2 = n by MATRIX_1:24;
A6: width (M2 * M1) = n by MATRIX_1:24;
A7: len M2 = n by MATRIX_1:24;
(M1 * M2) * (M1 * M2) = (M2 * M1) * (M1 * M2) by A2, MATRIX_6:def_1
.= ((M2 * M1) * M1) * M2 by A4, A7, A6, MATRIX_3:33
.= (M2 * (M1 * M1)) * M2 by A4, A5, MATRIX_3:33
.= (M2 * (0. (K,n))) * M2 by A1, Def2
.= (0. (K,n,n)) * M2 by A3, A7, A5, MATRIX_6:2
.= 0. (K,n) by A7, A5, MATRIX_6:1 ;
hence  M1 * M2 is Nilpotent by Def2; ::_thesis: verum
end;

theorem :: MATRIX_8:24
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is Nilpotent & M2 is Nilpotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds
M1 + M2 is Nilpotent
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is Nilpotent & M2 is Nilpotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds
M1 + M2 is Nilpotent
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 is Nilpotent & M2 is Nilpotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds
M1 + M2 is Nilpotent
let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 is Nilpotent & M2 is Nilpotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) implies M1 + M2 is Nilpotent )
assume that
A1: n > 0 and
A2: ( M1 is Nilpotent & M2 is Nilpotent ) and
A3: M1 commutes_with M2 and
A4: M1 * M2 = 0. (K,n) ; ::_thesis: M1 + M2 is Nilpotent
A5: M1 * M2 = 0. (K,n,n) by A4;
A6: ( M1 * M1 = 0. (K,n) & M2 * M2 = 0. (K,n) ) by A2, Def2;
(M1 + M2) * (M1 + M2) = (((M1 * M1) + (0. (K,n))) + (0. (K,n))) + (M2 * M2) by A1, A3, A4, MATRIX_6:35
.= ((M1 * M1) + (0. (K,n))) + (M2 * M2) by A5, MATRIX_3:4
.= (0. (K,n)) + (0. (K,n)) by A6, A5, MATRIX_3:4
.= 0. (K,n,n) by MATRIX_3:4
.= 0. (K,n) ;
hence  M1 + M2 is Nilpotent by Def2; ::_thesis: verum
end;

theorem :: MATRIX_8:25
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is Nilpotent & M2 is Nilpotent & M1 * M2 = - (M2 * M1) & n > 0 holds
M1 + M2 is Nilpotent
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is Nilpotent & M2 is Nilpotent & M1 * M2 = - (M2 * M1) & n > 0 holds
M1 + M2 is Nilpotent
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is Nilpotent & M2 is Nilpotent & M1 * M2 = - (M2 * M1) & n > 0 holds
M1 + M2 is Nilpotent
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is Nilpotent & M2 is Nilpotent & M1 * M2 = - (M2 * M1) & n > 0 implies M1 + M2 is Nilpotent )
assume that
A1: ( M1 is Nilpotent & M2 is Nilpotent ) and
A2: M1 * M2 = - (M2 * M1) and
A3: n > 0 ; ::_thesis: M1 + M2 is Nilpotent
A4: ( M1 * M1 = 0. (K,n) & M2 * M2 = 0. (K,n) ) by A1, Def2;
A5: ( len (M1 * M1) = n & width (M1 * M1) = n ) by MATRIX_1:24;
A6: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
A7: ( len ((M1 * M1) + (M2 * M1)) = n & width ((M1 * M1) + (M2 * M1)) = n ) by MATRIX_1:24;
A8: ( len (M2 * M1) = n & width (M2 * M1) = n ) by MATRIX_1:24;
A9: ( len (M1 * M2) = n & width (M1 * M2) = n ) by MATRIX_1:24;
A10: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
 ( len (M1 + M2) = n & width (M1 + M2) = n ) by MATRIX_1:24;
then (M1 + M2) * (M1 + M2) = ((M1 + M2) * M1) + ((M1 + M2) * M2) by A3, A6, A10, MATRIX_4:62
.= ((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2) by A3, A6, A10, MATRIX_4:63
.= ((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) by A3, A6, A10, MATRIX_4:63
.= (((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2) by A9, A7, MATRIX_3:3
.= ((M1 * M1) + ((M2 * M1) + (- (M2 * M1)))) + (M2 * M2) by A2, A5, A8, MATRIX_3:3
.= ((M1 * M1) + (0. (K,n,n))) + (M2 * M2) by A8, MATRIX_4:2
.= (0. (K,n)) + (0. (K,n)) by A4, MATRIX_3:4
.= 0. (K,n,n) by MATRIX_3:4
.= 0. (K,n) ;
hence  M1 + M2 is Nilpotent by Def2; ::_thesis: verum
end;

theorem :: MATRIX_8:26
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Nilpotent & n > 0 holds
M1 @ is Nilpotent
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is Nilpotent & n > 0 holds
M1 @ is Nilpotent
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Nilpotent & n > 0 holds
M1 @ is Nilpotent
let M1 be Matrix of n,K; ::_thesis: ( M1 is Nilpotent & n > 0 implies M1 @ is Nilpotent )
assume that
A1: M1 is Nilpotent and
A2: n > 0 ; ::_thesis: M1 @ is Nilpotent
 ( len M1 = n & width M1 = n ) by MATRIX_1:24;
then (M1 @) * (M1 @) = (M1 * M1) @ by A2, MATRIX_3:22
.= (0. (K,n)) @ by A1, Def2
.= (n,n) --> (0. K) by MATRIX_6:20
.= 0. (K,n) ;
hence  M1 @ is Nilpotent by Def2; ::_thesis: verum
end;

theorem :: MATRIX_8:27
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Nilpotent & M1 is Idempotent holds
M1 = 0. (K,n)
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is Nilpotent & M1 is Idempotent holds
M1 = 0. (K,n)
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Nilpotent & M1 is Idempotent holds
M1 = 0. (K,n)
let M1 be Matrix of n,K; ::_thesis: ( M1 is Nilpotent & M1 is Idempotent implies M1 = 0. (K,n) )
assume A1: ( M1 is Nilpotent & M1 is Idempotent ) ; ::_thesis: M1 = 0. (K,n)
then  M1 * M1 = 0. (K,n) by Def2;
hence  M1 = 0. (K,n) by A1, Def1; ::_thesis: verum
end;

theorem Th28: :: MATRIX_8:28
for n being Nat
for K being Field st n > 0 holds
0. (K,n) <> 1. (K,n)
proof
let n be Nat; ::_thesis: for K being Field st n > 0 holds
0. (K,n) <> 1. (K,n)
let K be Field; ::_thesis: ( n > 0 implies 0. (K,n) <> 1. (K,n) )
A1: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume  n > 0 ; ::_thesis: 0. (K,n) <> 1. (K,n)
then  n >= 0 + 1 by INT_1:7;
then  1 in Seg n ;
then A2: [1,1] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
assume A3: 0. (K,n) = 1. (K,n) ; ::_thesis: contradiction
 Indices (0. (K,n)) = Indices (1. (K,n)) by MATRIX_1:26;
then  (0. (K,n)) * (1,1) = 0. K by A2, A1, MATRIX_1:29;
then  0. K = 1. K by A2, A3, A1, MATRIX_1:def_11;
hence  contradiction ; ::_thesis: verum
end;

theorem :: MATRIX_8:29
for n being Nat
for K being Field
for M1 being Matrix of n,K st n > 0 & M1 is Nilpotent holds
not M1 is invertible
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st n > 0 & M1 is Nilpotent holds
not M1 is invertible
let K be Field; ::_thesis: for M1 being Matrix of n,K st n > 0 & M1 is Nilpotent holds
not M1 is invertible
let M1 be Matrix of n,K; ::_thesis: ( n > 0 & M1 is Nilpotent implies not M1 is invertible )
assume that
A1: n > 0 and
A2: M1 is Nilpotent ; ::_thesis: not M1 is invertible
A3: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
assume  M1 is invertible ; ::_thesis: contradiction
then consider M2 being Matrix of n,K such that
A4: M1 is_reverse_of M2 by MATRIX_6:def_3;
A5: width M2 = n by MATRIX_1:24;
A6: len M2 = n by MATRIX_1:24;
M1 = M1 * (1. (K,n)) by MATRIX_3:19
.= M1 * (M1 * M2) by A4, MATRIX_6:def_2
.= (M1 * M1) * M2 by A3, A6, MATRIX_3:33
.= (0. (K,n)) * M2 by A2, Def2
.= 0. (K,n,n) by A6, A5, MATRIX_6:1 ;
then A7: M1 * M2 = 0. (K,n) by A6, A5, MATRIX_6:1;
 M1 * M2 = 1. (K,n) by A4, MATRIX_6:def_2;
hence  contradiction by A1, A7, Th28; ::_thesis: verum
end;

theorem :: MATRIX_8:30
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Self_Reversible holds
M1 is Involutory
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is Self_Reversible holds
M1 is Involutory
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Self_Reversible holds
M1 is Involutory
let M1 be Matrix of n,K; ::_thesis: ( M1 is Self_Reversible implies M1 is Involutory )
assume A1: M1 is Self_Reversible ; ::_thesis: M1 is Involutory
then  M1 is invertible by Def4;
then  M1 ~ is_reverse_of M1 by MATRIX_6:def_4;
then A2: M1 * (M1 ~) = 1. (K,n) by MATRIX_6:def_2;
 M1 * M1 = M1 * (M1 ~) by A1, Def4;
hence  M1 is Involutory by A2, Def3; ::_thesis: verum
end;

theorem :: MATRIX_8:31
for n being Nat
for K being Field holds 1. (K,n) is Self_Reversible
proof
let n be Nat; ::_thesis: for K being Field holds 1. (K,n) is Self_Reversible
let K be Field; ::_thesis: 1. (K,n) is Self_Reversible
 ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) by MATRIX_6:8;
hence  1. (K,n) is Self_Reversible by Def4; ::_thesis: verum
end;

theorem :: MATRIX_8:32
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is Idempotent holds
M1 = 1. (K,n)
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is Idempotent holds
M1 = 1. (K,n)
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is Idempotent holds
M1 = 1. (K,n)
let M1 be Matrix of n,K; ::_thesis: ( M1 is Self_Reversible & M1 is Idempotent implies M1 = 1. (K,n) )
assume A1: ( M1 is Self_Reversible & M1 is Idempotent ) ; ::_thesis: M1 = 1. (K,n)
then  M1 is invertible by Def4;
then  M1 ~ is_reverse_of M1 by MATRIX_6:def_4;
then  1. (K,n) = M1 * (M1 ~) by MATRIX_6:def_2
.= M1 * M1 by A1, Def4 ;
hence  M1 = 1. (K,n) by A1, Def1; ::_thesis: verum
end;

theorem :: MATRIX_8:33
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is symmetric holds
M1 is Orthogonal
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is symmetric holds
M1 is Orthogonal
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is symmetric holds
M1 is Orthogonal
let M1 be Matrix of n,K; ::_thesis: ( M1 is Self_Reversible & M1 is symmetric implies M1 is Orthogonal )
assume A1: ( M1 is Self_Reversible & M1 is symmetric ) ; ::_thesis: M1 is Orthogonal
then A2: M1 = M1 @ by MATRIX_6:def_5;
 ( M1 is invertible & M1 = M1 ~ ) by A1, Def4;
hence  M1 is Orthogonal by A2, MATRIX_6:def_7; ::_thesis: verum
end;

definition
let n be Nat;
let K be Field;
let M1, M2 be Matrix of n,K;
predM1 is_similar_to M2 means :Def5: :: MATRIX_8:def 5
 ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~) * M2) * M );
reflexivity
 for M1 being Matrix of n,K ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~) * M1) * M )
proof
let M1 be Matrix of n,K; ::_thesis: ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~) * M1) * M )
take  1. (K,n) ; ::_thesis: ( 1. (K,n) is invertible & M1 = (((1. (K,n)) ~) * M1) * (1. (K,n)) )
(((1. (K,n)) ~) * M1) * (1. (K,n)) = ((1. (K,n)) * M1) * (1. (K,n)) by MATRIX_6:8
.= M1 * (1. (K,n)) by MATRIX_3:18
.= M1 by MATRIX_3:19 ;
hence  ( 1. (K,n) is invertible & M1 = (((1. (K,n)) ~) * M1) * (1. (K,n)) ) by MATRIX_6:8; ::_thesis: verum
end;
symmetry
 for M1, M2 being Matrix of n,K st ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~) * M2) * M ) holds
ex M being Matrix of n,K st
( M is invertible & M2 = ((M ~) * M1) * M )
proof
let M1, M2 be Matrix of n,K; ::_thesis: ( ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~) * M2) * M ) implies ex M being Matrix of n,K st
( M is invertible & M2 = ((M ~) * M1) * M ) )
given M being Matrix of n,K such that A1: M is invertible and
A2: M1 = ((M ~) * M2) * M ; ::_thesis: ex M being Matrix of n,K st
( M is invertible & M2 = ((M ~) * M1) * M )
A3: M ~ is_reverse_of M by A1, MATRIX_6:def_4;
take  M ~ ; ::_thesis: ( M ~ is invertible & M2 = (((M ~) ~) * M1) * (M ~) )
A4: width M2 = n by MATRIX_1:24;
A5: len M = n by MATRIX_1:24;
A6: ( len M2 = n & width (M ~) = n ) by MATRIX_1:24;
A7: width M = n by MATRIX_1:24;
A8: ( len ((M ~) * M2) = n & width ((M ~) * M2) = n ) by MATRIX_1:24;
A9: len (M ~) = n by MATRIX_1:24;
(((M ~) ~) * M1) * (M ~) = (M * (((M ~) * M2) * M)) * (M ~) by A1, A2, MATRIX_6:16
.= ((M * ((M ~) * M2)) * M) * (M ~) by A5, A7, A8, MATRIX_3:33
.= (((M * (M ~)) * M2) * M) * (M ~) by A7, A9, A6, MATRIX_3:33
.= (((1. (K,n)) * M2) * M) * (M ~) by A3, MATRIX_6:def_2
.= (M2 * M) * (M ~) by MATRIX_3:18
.= M2 * (M * (M ~)) by A4, A5, A7, A9, MATRIX_3:33
.= M2 * (1. (K,n)) by A3, MATRIX_6:def_2
.= M2 by MATRIX_3:19 ;
hence  ( M ~ is invertible & M2 = (((M ~) ~) * M1) * (M ~) ) by A1, MATRIX_6:16; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines is_similar_to MATRIX_8:def_5_:_
 for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds
( M1 is_similar_to M2 iff ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~) * M2) * M ) );

theorem :: MATRIX_8:34
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is_similar_to M2 & M2 is_similar_to M3 holds
M1 is_similar_to M3
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is_similar_to M2 & M2 is_similar_to M3 holds
M1 is_similar_to M3
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is_similar_to M2 & M2 is_similar_to M3 holds
M1 is_similar_to M3
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is_similar_to M2 & M2 is_similar_to M3 implies M1 is_similar_to M3 )
assume that
A1: M1 is_similar_to M2 and
A2: M2 is_similar_to M3 ; ::_thesis: M1 is_similar_to M3
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 ~) * M2) * M4 by A1, Def5;
consider M5 being Matrix of n,K such that
A5: M5 is invertible and
A6: M2 = ((M5 ~) * M3) * M5 by A2, Def5;
A7: len M5 = n by MATRIX_1:24;
take  M5 * M4 ; :: according to MATRIX_8:def_5 ::_thesis: ( M5 * M4 is invertible & M1 = (((M5 * M4) ~) * M3) * (M5 * M4) )
A8: width ((M5 * M4) ~) = n by MATRIX_1:24;
A9: ( len (M3 * M5) = n & width (M3 * M5) = n ) by MATRIX_1:24;
A10: len M4 = n by MATRIX_1:24;
A11: width M5 = n by MATRIX_1:24;
A12: len M3 = n by MATRIX_1:24;
A13: len (M5 * M4) = n by MATRIX_1:24;
A14: width (M4 ~) = n by MATRIX_1:24;
A15: ( len (M5 ~) = n & width (M5 ~) = n ) by MATRIX_1:24;
A16: width M3 = n by MATRIX_1:24;
 ( len ((M5 ~) * M3) = n & width ((M5 ~) * M3) = n ) by MATRIX_1:24;
then M1 = (((M4 ~) * ((M5 ~) * M3)) * M5) * M4 by A4, A6, A7, A14, MATRIX_3:33
.= ((((M4 ~) * (M5 ~)) * M3) * M5) * M4 by A12, A14, A15, MATRIX_3:33
.= ((((M5 * M4) ~) * M3) * M5) * M4 by A3, A5, MATRIX_6:36
.= (((M5 * M4) ~) * (M3 * M5)) * M4 by A12, A16, A7, A8, MATRIX_3:33
.= ((M5 * M4) ~) * ((M3 * M5) * M4) by A10, A8, A9, MATRIX_3:33
.= ((M5 * M4) ~) * (M3 * (M5 * M4)) by A16, A10, A7, A11, MATRIX_3:33
.= (((M5 * M4) ~) * M3) * (M5 * M4) by A12, A16, A8, A13, MATRIX_3:33 ;
hence  ( M5 * M4 is invertible & M1 = (((M5 * M4) ~) * M3) * (M5 * M4) ) by A3, A5, MATRIX_6:36; ::_thesis: verum
end;

theorem :: MATRIX_8:35
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Idempotent holds
M1 is Idempotent
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Idempotent holds
M1 is Idempotent
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Idempotent holds
M1 is Idempotent
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_similar_to M2 & M2 is Idempotent implies M1 is Idempotent )
assume that
A1: M1 is_similar_to M2 and
A2: M2 is Idempotent ; ::_thesis: M1 is Idempotent
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 ~) * M2) * M4 by A1, Def5;
A5: M4 ~ is_reverse_of M4 by A3, MATRIX_6:def_4;
A6: width M4 = n by MATRIX_1:24;
A7: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
A8: ( len (M2 * M4) = n & width (((M4 ~) * M2) * M4) = n ) by MATRIX_1:24;
A9: len (M4 ~) = n by MATRIX_1:24;
A10: width ((M4 ~) * M2) = n by MATRIX_1:24;
A11: width (M4 ~) = n by MATRIX_1:24;
A12: len M4 = n by MATRIX_1:24;
then M1 * M1 = (((M4 ~) * M2) * M4) * ((M4 ~) * (M2 * M4)) by A4, A7, A11, MATRIX_3:33
.= ((((M4 ~) * M2) * M4) * (M4 ~)) * (M2 * M4) by A9, A11, A8, MATRIX_3:33
.= (((M4 ~) * M2) * (M4 * (M4 ~))) * (M2 * M4) by A12, A6, A9, A10, MATRIX_3:33
.= (((M4 ~) * M2) * (1. (K,n))) * (M2 * M4) by A5, MATRIX_6:def_2
.= ((M4 ~) * M2) * (M2 * M4) by MATRIX_3:19
.= (((M4 ~) * M2) * M2) * M4 by A12, A7, A10, MATRIX_3:33
.= ((M4 ~) * (M2 * M2)) * M4 by A7, A11, MATRIX_3:33
.= M1 by A2, A4, Def1 ;
hence  M1 is Idempotent by Def1; ::_thesis: verum
end;

theorem :: MATRIX_8:36
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Nilpotent & n > 0 holds
M1 is Nilpotent
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Nilpotent & n > 0 holds
M1 is Nilpotent
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Nilpotent & n > 0 holds
M1 is Nilpotent
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_similar_to M2 & M2 is Nilpotent & n > 0 implies M1 is Nilpotent )
assume that
A1: M1 is_similar_to M2 and
A2: M2 is Nilpotent and
A3: n > 0 ; ::_thesis: M1 is Nilpotent
consider M4 being Matrix of n,K such that
A4: M4 is invertible and
A5: M1 = ((M4 ~) * M2) * M4 by A1, Def5;
A6: M4 ~ is_reverse_of M4 by A4, MATRIX_6:def_4;
A7: width M4 = n by MATRIX_1:24;
A8: width (M4 ~) = n by MATRIX_1:24;
A9: width ((M4 ~) * M2) = n by MATRIX_1:24;
A10: len (M4 ~) = n by MATRIX_1:24;
A11: ( len (M2 * M4) = n & width (((M4 ~) * M2) * M4) = n ) by MATRIX_1:24;
A12: len M4 = n by MATRIX_1:24;
A13: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
then M1 * M1 = (((M4 ~) * M2) * M4) * ((M4 ~) * (M2 * M4)) by A5, A12, A8, MATRIX_3:33
.= ((((M4 ~) * M2) * M4) * (M4 ~)) * (M2 * M4) by A10, A8, A11, MATRIX_3:33
.= (((M4 ~) * M2) * (M4 * (M4 ~))) * (M2 * M4) by A12, A7, A10, A9, MATRIX_3:33
.= (((M4 ~) * M2) * (1. (K,n))) * (M2 * M4) by A6, MATRIX_6:def_2
.= ((M4 ~) * M2) * (M2 * M4) by MATRIX_3:19
.= (((M4 ~) * M2) * M2) * M4 by A12, A13, A9, MATRIX_3:33
.= ((M4 ~) * (M2 * M2)) * M4 by A13, A8, MATRIX_3:33
.= ((M4 ~) * (0. (K,n))) * M4 by A2, Def2
.= (0. (K,n,n)) * M4 by A3, A10, A8, MATRIX_6:2
.= 0. (K,n) by A12, A7, MATRIX_6:1 ;
hence  M1 is Nilpotent by Def2; ::_thesis: verum
end;

theorem :: MATRIX_8:37
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Involutory holds
M1 is Involutory
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Involutory holds
M1 is Involutory
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Involutory holds
M1 is Involutory
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_similar_to M2 & M2 is Involutory implies M1 is Involutory )
assume that
A1: M1 is_similar_to M2 and
A2: M2 is Involutory ; ::_thesis: M1 is Involutory
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 ~) * M2) * M4 by A1, Def5;
A5: M4 ~ is_reverse_of M4 by A3, MATRIX_6:def_4;
A6: width ((M4 ~) * M2) = n by MATRIX_1:24;
A7: width (M4 ~) = n by MATRIX_1:24;
A8: ( len (M2 * M4) = n & width (((M4 ~) * M2) * M4) = n ) by MATRIX_1:24;
A9: len (M4 ~) = n by MATRIX_1:24;
A10: width M4 = n by MATRIX_1:24;
A11: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
A12: len M4 = n by MATRIX_1:24;
then M1 * M1 = (((M4 ~) * M2) * M4) * ((M4 ~) * (M2 * M4)) by A4, A11, A7, MATRIX_3:33
.= ((((M4 ~) * M2) * M4) * (M4 ~)) * (M2 * M4) by A9, A7, A8, MATRIX_3:33
.= (((M4 ~) * M2) * (M4 * (M4 ~))) * (M2 * M4) by A12, A10, A9, A6, MATRIX_3:33
.= (((M4 ~) * M2) * (1. (K,n))) * (M2 * M4) by A5, MATRIX_6:def_2
.= ((M4 ~) * M2) * (M2 * M4) by MATRIX_3:19
.= (((M4 ~) * M2) * M2) * M4 by A12, A11, A6, MATRIX_3:33
.= ((M4 ~) * (M2 * M2)) * M4 by A11, A7, MATRIX_3:33
.= ((M4 ~) * (1. (K,n))) * M4 by A2, Def3
.= (M4 ~) * M4 by MATRIX_3:19
.= 1. (K,n) by A5, MATRIX_6:def_2 ;
hence  M1 is Involutory by Def3; ::_thesis: verum
end;

theorem :: MATRIX_8:38
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds
M1 + (1. (K,n)) is_similar_to M2 + (1. (K,n))
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds
M1 + (1. (K,n)) is_similar_to M2 + (1. (K,n))
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds
M1 + (1. (K,n)) is_similar_to M2 + (1. (K,n))
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_similar_to M2 & n > 0 implies M1 + (1. (K,n)) is_similar_to M2 + (1. (K,n)) )
assume that
A1: M1 is_similar_to M2 and
A2: n > 0 ; ::_thesis: M1 + (1. (K,n)) is_similar_to M2 + (1. (K,n))
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 ~) * M2) * M4 by A1, Def5;
A5: M4 ~ is_reverse_of M4 by A3, MATRIX_6:def_4;
A6: ( len (1. (K,n)) = n & width (1. (K,n)) = n ) by MATRIX_1:24;
A7: width ((M4 ~) * M2) = n by MATRIX_1:24;
A8: ( len M4 = n & len ((M4 ~) * M2) = n ) by MATRIX_1:24;
take  M4 ; :: according to MATRIX_8:def_5 ::_thesis: ( M4 is invertible & M1 + (1. (K,n)) = ((M4 ~) * (M2 + (1. (K,n)))) * M4 )
A9: ( len (M4 ~) = n & width (M4 ~) = n ) by MATRIX_1:24;
 ( len M2 = n & width M2 = n ) by MATRIX_1:24;
then ((M4 ~) * (M2 + (1. (K,n)))) * M4 = (((M4 ~) * M2) + ((M4 ~) * (1. (K,n)))) * M4 by A2, A9, A6, MATRIX_4:62
.= (((M4 ~) * M2) + (M4 ~)) * M4 by MATRIX_3:19
.= (((M4 ~) * M2) * M4) + ((M4 ~) * M4) by A2, A9, A8, A7, MATRIX_4:63
.= M1 + (1. (K,n)) by A4, A5, MATRIX_6:def_2 ;
hence  ( M4 is invertible & M1 + (1. (K,n)) = ((M4 ~) * (M2 + (1. (K,n)))) * M4 ) by A3; ::_thesis: verum
end;

theorem :: MATRIX_8:39
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds
M1 + M1 is_similar_to M2 + M2
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds
M1 + M1 is_similar_to M2 + M2
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds
M1 + M1 is_similar_to M2 + M2
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_similar_to M2 & n > 0 implies M1 + M1 is_similar_to M2 + M2 )
assume that
A1: M1 is_similar_to M2 and
A2: n > 0 ; ::_thesis: M1 + M1 is_similar_to M2 + M2
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 ~) * M2) * M4 by A1, Def5;
A5: width ((M4 ~) * M2) = n by MATRIX_1:24;
take  M4 ; :: according to MATRIX_8:def_5 ::_thesis: ( M4 is invertible & M1 + M1 = ((M4 ~) * (M2 + M2)) * M4 )
A6: ( len M4 = n & len ((M4 ~) * M2) = n ) by MATRIX_1:24;
A7: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
 ( len (M4 ~) = n & width (M4 ~) = n ) by MATRIX_1:24;
then ((M4 ~) * (M2 + M2)) * M4 = (((M4 ~) * M2) + ((M4 ~) * M2)) * M4 by A2, A7, MATRIX_4:62
.= M1 + M1 by A2, A4, A6, A5, MATRIX_4:63 ;
hence  ( M4 is invertible & M1 + M1 = ((M4 ~) * (M2 + M2)) * M4 ) by A3; ::_thesis: verum
end;

theorem :: MATRIX_8:40
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds
(M1 + M1) + M1 is_similar_to (M2 + M2) + M2
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds
(M1 + M1) + M1 is_similar_to (M2 + M2) + M2
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds
(M1 + M1) + M1 is_similar_to (M2 + M2) + M2
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_similar_to M2 & n > 0 implies (M1 + M1) + M1 is_similar_to (M2 + M2) + M2 )
assume that
A1: M1 is_similar_to M2 and
A2: n > 0 ; ::_thesis: (M1 + M1) + M1 is_similar_to (M2 + M2) + M2
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 ~) * M2) * M4 by A1, Def5;
A5: ( len M4 = n & len ((M4 ~) * M2) = n ) by MATRIX_1:24;
A6: width ((M4 ~) * M2) = n by MATRIX_1:24;
A7: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
A8: ( len (M4 ~) = n & width (M4 ~) = n ) by MATRIX_1:24;
then A9: ((M4 ~) * (M2 + M2)) * M4 = (((M4 ~) * M2) + ((M4 ~) * M2)) * M4 by A2, A7, MATRIX_4:62
.= M1 + M1 by A2, A4, A5, A6, MATRIX_4:63 ;
take  M4 ; :: according to MATRIX_8:def_5 ::_thesis: ( M4 is invertible & (M1 + M1) + M1 = ((M4 ~) * ((M2 + M2) + M2)) * M4 )
A10: ( len ((M4 ~) * (M2 + M2)) = n & width ((M4 ~) * (M2 + M2)) = n ) by MATRIX_1:24;
 ( len (M2 + M2) = n & width (M2 + M2) = n ) by MATRIX_1:24;
then ((M4 ~) * ((M2 + M2) + M2)) * M4 = (((M4 ~) * (M2 + M2)) + ((M4 ~) * M2)) * M4 by A2, A7, A8, MATRIX_4:62
.= (M1 + M1) + M1 by A2, A4, A5, A6, A10, A9, MATRIX_4:63 ;
hence  ( M4 is invertible & (M1 + M1) + M1 = ((M4 ~) * ((M2 + M2) + M2)) * M4 ) by A3; ::_thesis: verum
end;

theorem :: MATRIX_8:41
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible holds
M2 * M1 is_similar_to M1 * M2
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible holds
M2 * M1 is_similar_to M1 * M2
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is invertible holds
M2 * M1 is_similar_to M1 * M2
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is invertible implies M2 * M1 is_similar_to M1 * M2 )
A1: ( len M2 = n & width (M1 ~) = n ) by MATRIX_1:24;
assume A2: M1 is invertible ; ::_thesis: M2 * M1 is_similar_to M1 * M2
then A3: M1 ~ is_reverse_of M1 by MATRIX_6:def_4;
take  M1 ; :: according to MATRIX_8:def_5 ::_thesis: ( M1 is invertible & M2 * M1 = ((M1 ~) * (M1 * M2)) * M1 )
 ( len M1 = n & width M1 = n ) by MATRIX_1:24;
then ((M1 ~) * (M1 * M2)) * M1 = (((M1 ~) * M1) * M2) * M1 by A1, MATRIX_3:33
.= ((1. (K,n)) * M2) * M1 by A3, MATRIX_6:def_2
.= M2 * M1 by MATRIX_3:18 ;
hence  ( M1 is invertible & M2 * M1 = ((M1 ~) * (M1 * M2)) * M1 ) by A2; ::_thesis: verum
end;

theorem :: MATRIX_8:42
for n being Nat
for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds
M1 is invertible
proof
let n be Nat; ::_thesis: for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds
M1 is invertible
let K be Field; ::_thesis: for M2, M1 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds
M1 is invertible
let M2, M1 be Matrix of n,K; ::_thesis: ( M2 is invertible & M1 is_similar_to M2 implies M1 is invertible )
assume that
A1: M2 is invertible and
A2: M1 is_similar_to M2 ; ::_thesis: M1 is invertible
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 ~) * M2) * M4 by A2, Def5;
 M4 ~ is invertible by A3, MATRIX_6:16;
then  (M4 ~) * M2 is invertible by A1, MATRIX_6:36;
hence  M1 is invertible by A3, A4, MATRIX_6:36; ::_thesis: verum
end;

theorem :: MATRIX_8:43
for n being Nat
for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds
M1 ~ is_similar_to M2 ~
proof
let n be Nat; ::_thesis: for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds
M1 ~ is_similar_to M2 ~
let K be Field; ::_thesis: for M2, M1 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds
M1 ~ is_similar_to M2 ~
let M2, M1 be Matrix of n,K; ::_thesis: ( M2 is invertible & M1 is_similar_to M2 implies M1 ~ is_similar_to M2 ~ )
assume that
A1: M2 is invertible and
A2: M1 is_similar_to M2 ; ::_thesis: M1 ~ is_similar_to M2 ~
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 ~) * M2) * M4 by A2, Def5;
A5: ( M4 ~ is invertible & (M4 ~) ~ = M4 ) by A3, MATRIX_6:16;
take  M4 ; :: according to MATRIX_8:def_5 ::_thesis: ( M4 is invertible & M1 ~ = ((M4 ~) * (M2 ~)) * M4 )
A6: ( width (M4 ~) = n & len M4 = n ) by MATRIX_1:24;
A7: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
 ( M2 * M4 is invertible & (M4 ~) * (M2 ~) = (M2 * M4) ~ ) by A1, A3, MATRIX_6:36;
then ((M4 ~) * (M2 ~)) * M4 = ((M4 ~) * (M2 * M4)) ~ by A5, MATRIX_6:36
.= M1 ~ by A4, A6, A7, MATRIX_3:33 ;
hence  ( M4 is invertible & M1 ~ = ((M4 ~) * (M2 ~)) * M4 ) by A3; ::_thesis: verum
end;

definition
let n be Nat;
let K be Field;
let M1, M2 be Matrix of n,K;
predM1 is_congruent_Matrix_of M2 means :Def6: :: MATRIX_8:def 6
 ex M being Matrix of n,K st
( M is invertible & M1 = ((M @) * M2) * M );
reflexivity
 for M1 being Matrix of n,K ex M being Matrix of n,K st
( M is invertible & M1 = ((M @) * M1) * M )
proof
set M = 1. (K,n);
let M1 be Matrix of n,K; ::_thesis: ex M being Matrix of n,K st
( M is invertible & M1 = ((M @) * M1) * M )
(((1. (K,n)) @) * M1) * (1. (K,n)) = ((1. (K,n)) * M1) * (1. (K,n)) by MATRIX_6:10
.= M1 * (1. (K,n)) by MATRIX_3:18
.= M1 by MATRIX_3:19 ;
hence  ex M being Matrix of n,K st
( M is invertible & M1 = ((M @) * M1) * M ) by MATRIX_6:8; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines is_congruent_Matrix_of MATRIX_8:def_6_:_
 for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds
( M1 is_congruent_Matrix_of M2 iff ex M being Matrix of n,K st
( M is invertible & M1 = ((M @) * M2) * M ) );

theorem :: MATRIX_8:44
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M2 is_congruent_Matrix_of M1
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M2 is_congruent_Matrix_of M1
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M2 is_congruent_Matrix_of M1
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_congruent_Matrix_of M2 & n > 0 implies M2 is_congruent_Matrix_of M1 )
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: n > 0 ; ::_thesis: M2 is_congruent_Matrix_of M1
consider M being Matrix of n,K such that
A3: M is invertible and
A4: M1 = ((M @) * M2) * M by A1, Def6;
A5: M ~ is_reverse_of M by A3, MATRIX_6:def_4;
take  M ~ ; :: according to MATRIX_8:def_6 ::_thesis: ( M ~ is invertible & M2 = (((M ~) @) * M1) * (M ~) )
A6: width (M ~) = n by MATRIX_1:24;
A7: ( len (M @) = n & width (M @) = n ) by MATRIX_1:24;
A8: width M = n by MATRIX_1:24;
A9: len (M ~) = n by MATRIX_1:24;
 ( len M = n & width ((M @) * M2) = n ) by MATRIX_1:24;
then A10: M1 * (M ~) = ((M @) * M2) * (M * (M ~)) by A4, A8, A9, MATRIX_3:33
.= ((M @) * M2) * (1. (K,n)) by A5, MATRIX_6:def_2
.= (M @) * M2 by MATRIX_3:19 ;
A11: len M2 = n by MATRIX_1:24;
A12: width ((M ~) @) = n by MATRIX_1:24;
 ( len M1 = n & width M1 = n ) by MATRIX_1:24;
then (((M ~) @) * M1) * (M ~) = ((M ~) @) * (M1 * (M ~)) by A9, A12, MATRIX_3:33
.= (((M ~) @) * (M @)) * M2 by A7, A11, A12, A10, MATRIX_3:33
.= ((M * (M ~)) @) * M2 by A2, A8, A9, A6, MATRIX_3:22
.= ((1. (K,n)) @) * M2 by A5, MATRIX_6:def_2
.= (1. (K,n)) * M2 by MATRIX_6:10
.= M2 by MATRIX_3:18 ;
hence  ( M ~ is invertible & M2 = (((M ~) @) * M1) * (M ~) ) by A3, MATRIX_6:16; ::_thesis: verum
end;

theorem :: MATRIX_8:45
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 holds
M1 is_congruent_Matrix_of M3
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 holds
M1 is_congruent_Matrix_of M3
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 holds
M1 is_congruent_Matrix_of M3
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 implies M1 is_congruent_Matrix_of M3 )
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: M2 is_congruent_Matrix_of M3 and
A3: n > 0 ; ::_thesis: M1 is_congruent_Matrix_of M3
A4: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
consider M4 being Matrix of n,K such that
A5: M4 is invertible and
A6: M1 = ((M4 @) * M2) * M4 by A1, Def6;
A7: len M4 = n by MATRIX_1:24;
consider M5 being Matrix of n,K such that
A8: M5 is invertible and
A9: M2 = ((M5 @) * M3) * M5 by A2, Def6;
A10: len M5 = n by MATRIX_1:24;
A11: ( len M3 = n & len (M5 @) = n ) by MATRIX_1:24;
A12: width M5 = n by MATRIX_1:24;
take  M5 * M4 ; :: according to MATRIX_8:def_6 ::_thesis: ( M5 * M4 is invertible & M1 = (((M5 * M4) @) * M3) * (M5 * M4) )
A13: ( len ((M5 @) * M3) = n & len (M5 * M4) = n ) by MATRIX_1:24;
A14: width (M4 @) = n by MATRIX_1:24;
A15: width (M5 @) = n by MATRIX_1:24;
A16: width ((M5 @) * M3) = n by MATRIX_1:24;
 width M4 = n by MATRIX_1:24;
then (((M5 * M4) @) * M3) * (M5 * M4) = (((M4 @) * (M5 @)) * M3) * (M5 * M4) by A3, A7, A12, MATRIX_3:22
.= ((M4 @) * ((M5 @) * M3)) * (M5 * M4) by A14, A11, A15, MATRIX_3:33
.= (M4 @) * (((M5 @) * M3) * (M5 * M4)) by A14, A16, A13, MATRIX_3:33
.= (M4 @) * ((((M5 @) * M3) * M5) * M4) by A7, A10, A12, A16, MATRIX_3:33
.= M1 by A6, A9, A4, A7, A14, MATRIX_3:33 ;
hence  ( M5 * M4 is invertible & M1 = (((M5 * M4) @) * M3) * (M5 * M4) ) by A5, A8, MATRIX_6:36; ::_thesis: verum
end;

theorem :: MATRIX_8:46
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M1 + M1 is_congruent_Matrix_of M2 + M2
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M1 + M1 is_congruent_Matrix_of M2 + M2
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M1 + M1 is_congruent_Matrix_of M2 + M2
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_congruent_Matrix_of M2 & n > 0 implies M1 + M1 is_congruent_Matrix_of M2 + M2 )
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: n > 0 ; ::_thesis: M1 + M1 is_congruent_Matrix_of M2 + M2
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 @) * M2) * M4 by A1, Def6;
A5: width ((M4 @) * M2) = n by MATRIX_1:24;
take  M4 ; :: according to MATRIX_8:def_6 ::_thesis: ( M4 is invertible & M1 + M1 = ((M4 @) * (M2 + M2)) * M4 )
A6: ( len M4 = n & len ((M4 @) * M2) = n ) by MATRIX_1:24;
A7: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
 ( len (M4 @) = n & width (M4 @) = n ) by MATRIX_1:24;
then ((M4 @) * (M2 + M2)) * M4 = (((M4 @) * M2) + ((M4 @) * M2)) * M4 by A2, A7, MATRIX_4:62
.= M1 + M1 by A2, A4, A6, A5, MATRIX_4:63 ;
hence  ( M4 is invertible & M1 + M1 = ((M4 @) * (M2 + M2)) * M4 ) by A3; ::_thesis: verum
end;

theorem :: MATRIX_8:47
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
(M1 + M1) + M1 is_congruent_Matrix_of (M2 + M2) + M2
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
(M1 + M1) + M1 is_congruent_Matrix_of (M2 + M2) + M2
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
(M1 + M1) + M1 is_congruent_Matrix_of (M2 + M2) + M2
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_congruent_Matrix_of M2 & n > 0 implies (M1 + M1) + M1 is_congruent_Matrix_of (M2 + M2) + M2 )
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: n > 0 ; ::_thesis: (M1 + M1) + M1 is_congruent_Matrix_of (M2 + M2) + M2
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 @) * M2) * M4 by A1, Def6;
A5: ( len M4 = n & len ((M4 @) * M2) = n ) by MATRIX_1:24;
A6: width ((M4 @) * M2) = n by MATRIX_1:24;
A7: ( len M2 = n & width M2 = n ) by MATRIX_1:24;
A8: ( len (M4 @) = n & width (M4 @) = n ) by MATRIX_1:24;
then A9: ((M4 @) * (M2 + M2)) * M4 = (((M4 @) * M2) + ((M4 @) * M2)) * M4 by A2, A7, MATRIX_4:62
.= M1 + M1 by A2, A4, A5, A6, MATRIX_4:63 ;
take  M4 ; :: according to MATRIX_8:def_6 ::_thesis: ( M4 is invertible & (M1 + M1) + M1 = ((M4 @) * ((M2 + M2) + M2)) * M4 )
A10: ( len ((M4 @) * (M2 + M2)) = n & width ((M4 @) * (M2 + M2)) = n ) by MATRIX_1:24;
 ( len (M2 + M2) = n & width (M2 + M2) = n ) by MATRIX_1:24;
then ((M4 @) * ((M2 + M2) + M2)) * M4 = (((M4 @) * (M2 + M2)) + ((M4 @) * M2)) * M4 by A2, A7, A8, MATRIX_4:62
.= (M1 + M1) + M1 by A2, A4, A5, A6, A10, A9, MATRIX_4:63 ;
hence  ( M4 is invertible & (M1 + M1) + M1 = ((M4 @) * ((M2 + M2) + M2)) * M4 ) by A3; ::_thesis: verum
end;

theorem :: MATRIX_8:48
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is Orthogonal holds
M2 * M1 is_congruent_Matrix_of M1 * M2
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is Orthogonal holds
M2 * M1 is_congruent_Matrix_of M1 * M2
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is Orthogonal holds
M2 * M1 is_congruent_Matrix_of M1 * M2
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is Orthogonal implies M2 * M1 is_congruent_Matrix_of M1 * M2 )
A1: ( len M2 = n & width (M1 ~) = n ) by MATRIX_1:24;
assume A2: M1 is Orthogonal ; ::_thesis: M2 * M1 is_congruent_Matrix_of M1 * M2
then  M1 is invertible by MATRIX_6:def_7;
then A3: M1 ~ is_reverse_of M1 by MATRIX_6:def_4;
take  M1 ; :: according to MATRIX_8:def_6 ::_thesis: ( M1 is invertible & M2 * M1 = ((M1 @) * (M1 * M2)) * M1 )
 ( len M1 = n & width M1 = n ) by MATRIX_1:24;
then ((M1 ~) * (M1 * M2)) * M1 = (((M1 ~) * M1) * M2) * M1 by A1, MATRIX_3:33
.= ((1. (K,n)) * M2) * M1 by A3, MATRIX_6:def_2
.= M2 * M1 by MATRIX_3:18 ;
hence  ( M1 is invertible & M2 * M1 = ((M1 @) * (M1 * M2)) * M1 ) by A2, MATRIX_6:def_7; ::_thesis: verum
end;

theorem :: MATRIX_8:49
for n being Nat
for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible & M1 is_congruent_Matrix_of M2 & n > 0 holds
M1 is invertible
proof
let n be Nat; ::_thesis: for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible & M1 is_congruent_Matrix_of M2 & n > 0 holds
M1 is invertible
let K be Field; ::_thesis: for M2, M1 being Matrix of n,K st M2 is invertible & M1 is_congruent_Matrix_of M2 & n > 0 holds
M1 is invertible
let M2, M1 be Matrix of n,K; ::_thesis: ( M2 is invertible & M1 is_congruent_Matrix_of M2 & n > 0 implies M1 is invertible )
assume that
A1: M2 is invertible and
A2: M1 is_congruent_Matrix_of M2 and
A3: n > 0 ; ::_thesis: M1 is invertible
consider M4 being Matrix of n,K such that
A4: M4 is invertible and
A5: M1 = ((M4 @) * M2) * M4 by A2, Def6;
set M6 = (M4 ~) @ ;
set M5 = M4 @ ;
A6: ( width M4 = n & width (M4 ~) = n ) by MATRIX_1:24;
 len M4 = n by MATRIX_1:24;
then A7: ((M4 ~) * M4) @ = (M4 @) * ((M4 ~) @) by A3, A6, MATRIX_3:22;
A8: M4 ~ is_reverse_of M4 by A4, MATRIX_6:def_4;
then  (M4 ~) * M4 = 1. (K,n) by MATRIX_6:def_2;
then A9: (M4 @) * ((M4 ~) @) = 1. (K,n) by A7, MATRIX_6:10;
 len (M4 ~) = n by MATRIX_1:24;
then  (M4 * (M4 ~)) @ = ((M4 ~) @) * (M4 @) by A3, A6, MATRIX_3:22;
then  (M4 @) * ((M4 ~) @) = ((M4 ~) @) * (M4 @) by A8, A7, MATRIX_6:def_2;
then  M4 @ is_reverse_of (M4 ~) @ by A9, MATRIX_6:def_2;
then  M4 @ is invertible by MATRIX_6:def_3;
then  (M4 @) * M2 is invertible by A1, MATRIX_6:36;
hence  M1 is invertible by A4, A5, MATRIX_6:36; ::_thesis: verum
end;

theorem :: MATRIX_8:50
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M1 @ is_congruent_Matrix_of M2 @
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M1 @ is_congruent_Matrix_of M2 @
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M1 @ is_congruent_Matrix_of M2 @
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_congruent_Matrix_of M2 & n > 0 implies M1 @ is_congruent_Matrix_of M2 @ )
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: n > 0 ; ::_thesis: M1 @ is_congruent_Matrix_of M2 @
consider M4 being Matrix of n,K such that
A3: M4 is invertible and
A4: M1 = ((M4 @) * M2) * M4 by A1, Def6;
A5: width (M4 @) = n by MATRIX_1:24;
A6: ( width (M2 * M4) = n & len (M2 * M4) = n ) by MATRIX_1:24;
A7: len M2 = n by MATRIX_1:24;
A8: width M2 = n by MATRIX_1:24;
take  M4 ; :: according to MATRIX_8:def_6 ::_thesis: ( M4 is invertible & M1 @ = ((M4 @) * (M2 @)) * M4 )
A9: len M4 = n by MATRIX_1:24;
A10: width M4 = n by MATRIX_1:24;
then ((M4 @) * (M2 @)) * M4 = ((M4 @) * (M2 @)) * ((M4 @) @) by A2, A9, MATRIX_2:13
.= ((M2 * M4) @) * ((M4 @) @) by A2, A10, A9, A8, MATRIX_3:22
.= ((M4 @) * (M2 * M4)) @ by A2, A5, A6, MATRIX_3:22
.= M1 @ by A4, A9, A8, A7, A5, MATRIX_3:33 ;
hence  ( M4 is invertible & M1 @ = ((M4 @) * (M2 @)) * M4 ) by A3; ::_thesis: verum
end;

theorem :: MATRIX_8:51
for n being Nat
for K being Field
for M4, M2 being Matrix of n,K st M4 is Orthogonal holds
((M4 @) * M2) * M4 is_similar_to M2
proof
let n be Nat; ::_thesis: for K being Field
for M4, M2 being Matrix of n,K st M4 is Orthogonal holds
((M4 @) * M2) * M4 is_similar_to M2
let K be Field; ::_thesis: for M4, M2 being Matrix of n,K st M4 is Orthogonal holds
((M4 @) * M2) * M4 is_similar_to M2
let M4, M2 be Matrix of n,K; ::_thesis: ( M4 is Orthogonal implies ((M4 @) * M2) * M4 is_similar_to M2 )
assume A1: M4 is Orthogonal ; ::_thesis: ((M4 @) * M2) * M4 is_similar_to M2
take  M4 ; :: according to MATRIX_8:def_5 ::_thesis: ( M4 is invertible & ((M4 @) * M2) * M4 = ((M4 ~) * M2) * M4 )
thus  ( M4 is invertible & ((M4 @) * M2) * M4 = ((M4 ~) * M2) * M4 ) by A1, MATRIX_6:def_7; ::_thesis: verum
end;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func Trace M ->  Element of K equals :: MATRIX_8:def 7
 Sum (diagonal_of_Matrix M);
coherence
 Sum (diagonal_of_Matrix M) is Element of K ;
end;

:: deftheorem  defines Trace MATRIX_8:def_7_:_
 for n being Nat
for K being Field
for M being Matrix of n,K holds Trace M = Sum (diagonal_of_Matrix M);

theorem :: MATRIX_8:52
for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace M1 = Trace (M1 @)
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K holds Trace M1 = Trace (M1 @)
let K be Field; ::_thesis: for M1 being Matrix of n,K holds Trace M1 = Trace (M1 @)
let M1 be Matrix of n,K; ::_thesis: Trace M1 = Trace (M1 @)
A1: for i being Nat st i in Seg n holds
(diagonal_of_Matrix M1) . i = (diagonal_of_Matrix (M1 @)) . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies (diagonal_of_Matrix M1) . i = (diagonal_of_Matrix (M1 @)) . i )
assume A2: i in Seg n ; ::_thesis: (diagonal_of_Matrix M1) . i = (diagonal_of_Matrix (M1 @)) . i
then A3: ( (diagonal_of_Matrix M1) . i = M1 * (i,i) & (diagonal_of_Matrix (M1 @)) . i = (M1 @) * (i,i) ) by MATRIX_3:def_10;
 Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
then  [i,i] in Indices M1 by A2, ZFMISC_1:87;
hence  (diagonal_of_Matrix M1) . i = (diagonal_of_Matrix (M1 @)) . i by A3, MATRIX_1:def_6; ::_thesis: verum
end;
 len (diagonal_of_Matrix (M1 @)) = n by MATRIX_3:def_10;
then A4: dom (diagonal_of_Matrix (M1 @)) = Seg n by FINSEQ_1:def_3;
 len (diagonal_of_Matrix M1) = n by MATRIX_3:def_10;
then  dom (diagonal_of_Matrix M1) = Seg n by FINSEQ_1:def_3;
hence  Trace M1 = Trace (M1 @) by A1, A4, FINSEQ_1:13; ::_thesis: verum
end;

theorem Th53: :: MATRIX_8:53
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds Trace (M1 + M2) = (Trace M1) + (Trace M2)
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K holds Trace (M1 + M2) = (Trace M1) + (Trace M2)
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K holds Trace (M1 + M2) = (Trace M1) + (Trace M2)
let M1, M2 be Matrix of n,K; ::_thesis: Trace (M1 + M2) = (Trace M1) + (Trace M2)
A1: len (diagonal_of_Matrix M1) = n by MATRIX_3:def_10;
then A2: dom (diagonal_of_Matrix M1) = Seg n by FINSEQ_1:def_3;
 len (diagonal_of_Matrix (M1 + M2)) = n by MATRIX_3:def_10;
then A3: dom (diagonal_of_Matrix (M1 + M2)) = Seg n by FINSEQ_1:def_3;
A4: len (diagonal_of_Matrix M2) = n by MATRIX_3:def_10;
then  dom (diagonal_of_Matrix M2) = Seg n by FINSEQ_1:def_3;
then A5: dom ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) = Seg n by A2, POLYNOM1:1;
 for i being Nat st i in dom (diagonal_of_Matrix M1) holds
((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i
proof
let i be Nat; ::_thesis: ( i in dom (diagonal_of_Matrix M1) implies ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i )
assume  i in dom (diagonal_of_Matrix M1) ; ::_thesis: ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i
then A6: i in Seg n by A1, FINSEQ_1:def_3;
then A7: (diagonal_of_Matrix (M1 + M2)) . i = (M1 + M2) * (i,i) by MATRIX_3:def_10;
 Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
then A8: [i,i] in Indices M1 by A6, ZFMISC_1:87;
 ( (diagonal_of_Matrix M1) . i = M1 * (i,i) & (diagonal_of_Matrix M2) . i = M2 * (i,i) ) by A6, MATRIX_3:def_10;
then ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (M1 * (i,i)) + (M2 * (i,i)) by A5, A6, FUNCOP_1:22
.= (diagonal_of_Matrix (M1 + M2)) . i by A8, A7, MATRIX_3:def_3 ;
hence  ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i ; ::_thesis: verum
end;
then  Trace (M1 + M2) = Sum ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) by A2, A3, A5, FINSEQ_1:13
.= (Sum (diagonal_of_Matrix M1)) + (Sum (diagonal_of_Matrix M2)) by A1, A4, MATRIX_4:61 ;
hence  Trace (M1 + M2) = (Trace M1) + (Trace M2) ; ::_thesis: verum
end;

theorem :: MATRIX_8:54
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) + M3) = ((Trace M1) + (Trace M2)) + (Trace M3)
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) + M3) = ((Trace M1) + (Trace M2)) + (Trace M3)
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) + M3) = ((Trace M1) + (Trace M2)) + (Trace M3)
let M1, M2, M3 be Matrix of n,K; ::_thesis: Trace ((M1 + M2) + M3) = ((Trace M1) + (Trace M2)) + (Trace M3)
 Trace ((M1 + M2) + M3) = (Trace (M1 + M2)) + (Trace M3) by Th53;
hence  Trace ((M1 + M2) + M3) = ((Trace M1) + (Trace M2)) + (Trace M3) by Th53; ::_thesis: verum
end;

theorem Th55: :: MATRIX_8:55
for n being Nat
for K being Field holds Trace (0. (K,n)) = 0. K
proof
let n be Nat; ::_thesis: for K being Field holds Trace (0. (K,n)) = 0. K
let K be Field; ::_thesis: Trace (0. (K,n)) = 0. K
 len (diagonal_of_Matrix (0. (K,n))) = n by MATRIX_3:def_10;
then A1: dom (diagonal_of_Matrix (0. (K,n))) = Seg n by FINSEQ_1:def_3;
 for i being Nat st i in dom (diagonal_of_Matrix (0. (K,n))) holds
(diagonal_of_Matrix (0. (K,n))) /. i = 0. K
proof
let i be Nat; ::_thesis: ( i in dom (diagonal_of_Matrix (0. (K,n))) implies (diagonal_of_Matrix (0. (K,n))) /. i = 0. K )
assume A2: i in dom (diagonal_of_Matrix (0. (K,n))) ; ::_thesis: (diagonal_of_Matrix (0. (K,n))) /. i = 0. K
 Indices (0. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_1:24;
then  [i,i] in Indices (0. (K,n,n)) by A1, A2, ZFMISC_1:87;
then A3: (0. (K,n)) * (i,i) = 0. K by MATRIX_3:1;
 (diagonal_of_Matrix (0. (K,n))) . i = (0. (K,n)) * (i,i) by A1, A2, MATRIX_3:def_10;
hence  (diagonal_of_Matrix (0. (K,n))) /. i = 0. K by A2, A3, PARTFUN1:def_6; ::_thesis: verum
end;
hence  Trace (0. (K,n)) = 0. K by MATRLIN:11; ::_thesis: verum
end;

theorem Th56: :: MATRIX_8:56
for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace (- M1) = - (Trace M1)
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K holds Trace (- M1) = - (Trace M1)
let K be Field; ::_thesis: for M1 being Matrix of n,K holds Trace (- M1) = - (Trace M1)
let M1 be Matrix of n,K; ::_thesis: Trace (- M1) = - (Trace M1)
A1: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
(Trace M1) + (Trace (- M1)) = Trace (M1 + (- M1)) by Th53
.= Trace (0. (K,n,n)) by A1, MATRIX_4:2
.= Trace (0. (K,n))
.= 0. K by Th55 ;
hence  Trace (- M1) = - (Trace M1) by RLVECT_1:6; ::_thesis: verum
end;

theorem :: MATRIX_8:57
for n being Nat
for K being Field
for M1 being Matrix of n,K holds - (Trace (- M1)) = Trace M1
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K holds - (Trace (- M1)) = Trace M1
let K be Field; ::_thesis: for M1 being Matrix of n,K holds - (Trace (- M1)) = Trace M1
let M1 be Matrix of n,K; ::_thesis: - (Trace (- M1)) = Trace M1
A1: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
(Trace M1) + (Trace (- M1)) = Trace (M1 + (- M1)) by Th53
.= Trace (0. (K,n,n)) by A1, MATRIX_4:2
.= Trace (0. (K,n))
.= 0. K by Th55 ;
hence  - (Trace (- M1)) = Trace M1 by RLVECT_1:6; ::_thesis: verum
end;

theorem :: MATRIX_8:58
for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K
let K be Field; ::_thesis: for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K
let M1 be Matrix of n,K; ::_thesis: Trace (M1 + (- M1)) = 0. K
 ( len M1 = n & width M1 = n ) by MATRIX_1:24;
then  Trace (M1 + (- M1)) = Trace (0. (K,n,n)) by MATRIX_4:2
.= Trace (0. (K,n))
.= 0. K by Th55 ;
hence  Trace (M1 + (- M1)) = 0. K ; ::_thesis: verum
end;

theorem Th59: :: MATRIX_8:59
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds Trace (M1 - M2) = (Trace M1) - (Trace M2)
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K holds Trace (M1 - M2) = (Trace M1) - (Trace M2)
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K holds Trace (M1 - M2) = (Trace M1) - (Trace M2)
let M1, M2 be Matrix of n,K; ::_thesis: Trace (M1 - M2) = (Trace M1) - (Trace M2)
Trace (M1 - M2) = (Trace M1) + (Trace (- M2)) by Th53
.= (Trace M1) + (- (Trace M2)) by Th56 ;
hence  Trace (M1 - M2) = (Trace M1) - (Trace M2) ; ::_thesis: verum
end;

theorem :: MATRIX_8:60
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) + M3) = ((Trace M1) - (Trace M2)) + (Trace M3)
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) + M3) = ((Trace M1) - (Trace M2)) + (Trace M3)
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) + M3) = ((Trace M1) - (Trace M2)) + (Trace M3)
let M1, M2, M3 be Matrix of n,K; ::_thesis: Trace ((M1 - M2) + M3) = ((Trace M1) - (Trace M2)) + (Trace M3)
Trace ((M1 - M2) + M3) = (Trace (M1 - M2)) + (Trace M3) by Th53
.= ((Trace M1) - (Trace M2)) + (Trace M3) by Th59 ;
hence  Trace ((M1 - M2) + M3) = ((Trace M1) - (Trace M2)) + (Trace M3) ; ::_thesis: verum
end;

theorem :: MATRIX_8:61
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) - M3) = ((Trace M1) + (Trace M2)) - (Trace M3)
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) - M3) = ((Trace M1) + (Trace M2)) - (Trace M3)
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) - M3) = ((Trace M1) + (Trace M2)) - (Trace M3)
let M1, M2, M3 be Matrix of n,K; ::_thesis: Trace ((M1 + M2) - M3) = ((Trace M1) + (Trace M2)) - (Trace M3)
Trace ((M1 + M2) - M3) = (Trace (M1 + M2)) - (Trace M3) by Th59
.= ((Trace M1) + (Trace M2)) - (Trace M3) by Th53 ;
hence  Trace ((M1 + M2) - M3) = ((Trace M1) + (Trace M2)) - (Trace M3) ; ::_thesis: verum
end;

theorem :: MATRIX_8:62
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) - M3) = ((Trace M1) - (Trace M2)) - (Trace M3)
proof
let n be Nat; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) - M3) = ((Trace M1) - (Trace M2)) - (Trace M3)
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) - M3) = ((Trace M1) - (Trace M2)) - (Trace M3)
let M1, M2, M3 be Matrix of n,K; ::_thesis: Trace ((M1 - M2) - M3) = ((Trace M1) - (Trace M2)) - (Trace M3)
Trace ((M1 - M2) - M3) = (Trace (M1 - M2)) - (Trace M3) by Th59
.= ((Trace M1) - (Trace M2)) - (Trace M3) by Th59 ;
hence  Trace ((M1 - M2) - M3) = ((Trace M1) - (Trace M2)) - (Trace M3) ; ::_thesis: verum
end;