:: 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;