matrix_8.miz



    begin

    reserve i,n for Nat,

K for Field,

M1,M2,M3,M4 for Matrix of n, K;

    definition

      let n be Nat, K be Field, M1 be Matrix of n, K;

      :: MATRIX_8:def1

      attr M1 is Idempotent means (M1 * M1) = M1;

      :: MATRIX_8:def2

      attr M1 is Nilpotent means (M1 * M1) = ( 0. (K,n));

      :: MATRIX_8:def3

      attr M1 is Involutory means (M1 * M1) = ( 1. (K,n));

      :: MATRIX_8:def4

      attr M1 is Self_Reversible means M1 is invertible & (M1 ~ ) = M1;

    end

    theorem :: MATRIX_8:1

    

     Th1: ( 1. (K,n)) is Idempotent Involutory by MATRIX_3: 18;

    theorem :: MATRIX_8:2

    

     Th2: ( 0. (K,n)) is Idempotent Nilpotent

    proof

      ( width ( 0. (K,n,n))) = n & ( len ( 0. (K,n,n))) = n by MATRIX_0: 24;

      then (( 0. (K,n,n)) * ( 0. (K,n))) = ( 0. (K,n,n)) by MATRIX_6: 1;

      hence thesis;

    end;

    registration

      let n be Nat, K be Field;

      cluster ( 1. (K,n)) -> Idempotent Involutory;

      coherence by Th1;

      cluster ( 0. (K,n)) -> Idempotent Nilpotent;

      coherence by Th2;

    end

    theorem :: MATRIX_8:3

    n > 0 implies (M1 is Idempotent iff (M1 @ ) is Idempotent)

    proof

      assume

       A1: n > 0 ;

      set M2 = (M1 @ );

      

       A2: ( width M1) = n & ( len M1) = n by MATRIX_0: 24;

      thus M1 is Idempotent implies M2 is Idempotent by A1, A2, MATRIX_3: 22;

      

       A3: ( width M2) = n & ( len M2) = n by MATRIX_0: 24;

      assume

       A4: M2 is Idempotent;

      M1 = (M2 @ ) by A1, A2, MATRIX_0: 57

      .= ((M2 * M2) @ ) by A4

      .= ((M2 @ ) * (M2 @ )) by A1, A3, MATRIX_3: 22

      .= (M1 * ((M1 @ ) @ )) by A1, A2, MATRIX_0: 57

      .= (M1 * M1) by A1, A2, MATRIX_0: 57;

      hence thesis;

    end;

    theorem :: MATRIX_8:4

    M1 is Involutory implies M1 is invertible by MATRIX_6:def 2, MATRIX_6:def 3;

    theorem :: MATRIX_8:5

    M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies (M1 * M1) commutes_with (M2 * M2);

    theorem :: MATRIX_8:6

    n > 0 & M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 & (M1 * M2) = ( 0. (K,n)) implies (M1 + M2) is Idempotent

    proof

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

      

       A5: (M1 * M2) = ( 0. (K,n,n)) by A4;

      

       A6: (M1 * M1) = M1 & (M2 * M2) = M2 by A2;

      ((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 thesis;

    end;

    theorem :: MATRIX_8:7

    M1 is Idempotent & M2 is Idempotent & (M1 * M2) = ( - (M2 * M1)) implies (M1 + M2) is Idempotent

    proof

      assume that

       A1: M1 is Idempotent & M2 is Idempotent and

       A2: (M1 * M2) = ( - (M2 * M1));

      

       A3: (M1 * M1) = M1 & (M2 * M2) = M2 by A1;

      per cases by NAT_1: 3;

        suppose

         A4: n > 0 ;

        

         A5: ( len (M1 * M2)) = n & ( width (M1 * M2)) = n by MATRIX_0: 24;

        

         A6: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

        

         A7: ( len ((M1 * M1) + (M2 * M1))) = n & ( width ((M1 * M1) + (M2 * M1))) = n by MATRIX_0: 24;

        

         A8: ( len (M2 * M1)) = n & ( width (M2 * M1)) = n by MATRIX_0: 24;

        

         A9: ( len (M1 * M1)) = n & ( width (M1 * M1)) = n by MATRIX_0: 24;

        

         A10: ( len M1) = n & ( width M1) = n by MATRIX_0: 24;

        ( len (M1 + M2)) = n & ( width (M1 + M2)) = n by MATRIX_0: 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 thesis;

      end;

        suppose n = 0 ;

        then ((M1 + M2) * (M1 + M2)) = (M1 + M2) by MATRIX_0: 45;

        hence thesis;

      end;

    end;

    theorem :: MATRIX_8:8

    M1 is Idempotent & M2 is invertible implies (((M2 ~ ) * M1) * M2) is Idempotent

    proof

      assume that

       A1: M1 is Idempotent and

       A2: M2 is invertible;

      

       A3: (M2 ~ ) is_reverse_of M2 by A2, MATRIX_6:def 4;

      

       A4: ( width M2) = n by MATRIX_0: 24;

      

       A5: ( len M2) = n by MATRIX_0: 24;

      

       A6: ( len (M1 * M2)) = n & ( width (((M2 ~ ) * M1) * M2)) = n by MATRIX_0: 24;

      

       A7: ( len (M2 ~ )) = n by MATRIX_0: 24;

      

       A8: ( width ((M2 ~ ) * M1)) = n by MATRIX_0: 24;

      

       A9: ( width (M2 ~ )) = n by MATRIX_0: 24;

      

       A10: ( len M1) = n & ( width M1) = n by MATRIX_0: 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;

      hence thesis;

    end;

    theorem :: MATRIX_8:9

    M1 is invertible Idempotent implies (M1 ~ ) is Idempotent by MATRIX_6: 36;

    theorem :: MATRIX_8:10

    

     Th10: M1 is invertible Idempotent implies M1 = ( 1. (K,n))

    proof

      

       A1: ( len M1) = n & ( width M1) = n by MATRIX_0: 24;

      

       A2: ( width (M1 ~ )) = n by MATRIX_0: 24;

      assume

       A3: M1 is invertible Idempotent;

      then

       A4: (M1 ~ ) is_reverse_of M1 by MATRIX_6:def 4;

      (M1 * M1) = M1 by A3;

      

      then ( 1. (K,n)) = ((M1 ~ ) * (M1 * M1)) by A4, MATRIX_6:def 2

      .= (((M1 ~ ) * M1) * M1) by A1, A2, MATRIX_3: 33

      .= (( 1. (K,n)) * M1) by A4, MATRIX_6:def 2

      .= M1 by MATRIX_3: 18;

      hence thesis;

    end;

    theorem :: MATRIX_8:11

    M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies (M1 * M2) is Idempotent

    proof

      assume that

       A1: M1 is Idempotent and

       A2: M2 is Idempotent and

       A3: M1 commutes_with M2;

      

       A4: ( len M1) = n by MATRIX_0: 24;

      

       A5: ( width M2) = n by MATRIX_0: 24;

      

       A6: ( width M1) = n & ( len M2) = n by MATRIX_0: 24;

      ( width (M1 * M2)) = n by MATRIX_0: 24;

      

      then ((M1 * M2) * (M1 * M2)) = (((M1 * M2) * M1) * M2) by 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

      .= (M1 * (M2 * M2)) by A6, A5, MATRIX_3: 33

      .= (M1 * M2) by A2;

      hence thesis;

    end;

    theorem :: MATRIX_8:12

    M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies ((M1 @ ) * (M2 @ )) is Idempotent

    proof

      assume that

       A1: M1 is Idempotent and

       A2: M2 is Idempotent and

       A3: M1 commutes_with M2;

      set M3 = ((M1 @ ) * (M2 @ ));

      per cases by NAT_1: 3;

        suppose

         A4: n > 0 ;

        

         A5: (M1 * M1) = M1 by A1;

        

         A6: ( len M1) = n by MATRIX_0: 24;

        

         A7: ( len (M1 @ )) = n by MATRIX_0: 24;

        

         A8: ( width (M2 @ )) = n by MATRIX_0: 24;

        

         A9: ( width M2) = n by MATRIX_0: 24;

        

         A10: ( len M2) = n by MATRIX_0: 24;

        

         A11: ( width M1) = n by MATRIX_0: 24;

        

         A12: ( width (M1 @ )) = n & ( len (M2 @ )) = n by MATRIX_0: 24;

        ( width M3) = n by MATRIX_0: 24;

        

        then (M3 * M3) = ((((M1 @ ) * (M2 @ )) * (M1 @ )) * (M2 @ )) by A7, A12, MATRIX_3: 33

        .= (((M1 @ ) * ((M2 @ ) * (M1 @ ))) * (M2 @ )) by A7, A12, A8, MATRIX_3: 33

        .= (((M1 @ ) * ((M1 * M2) @ )) * (M2 @ )) by A4, A11, A10, A9, MATRIX_3: 22

        .= (((M1 @ ) * ((M2 * M1) @ )) * (M2 @ )) by A3, MATRIX_6:def 1

        .= (((M1 @ ) * ((M1 @ ) * (M2 @ ))) * (M2 @ )) by A4, A6, A11, A9, MATRIX_3: 22

        .= ((((M1 @ ) * (M1 @ )) * (M2 @ )) * (M2 @ )) by A7, A12, MATRIX_3: 33

        .= ((((M1 * M1) @ ) * (M2 @ )) * (M2 @ )) by A4, A6, A11, MATRIX_3: 22

        .= ((M1 @ ) * ((M2 @ ) * (M2 @ ))) by A5, A12, A8, MATRIX_3: 33

        .= ((M1 @ ) * ((M2 * M2) @ )) by A4, A10, A9, MATRIX_3: 22

        .= ((M1 @ ) * (M2 @ )) by A2;

        hence thesis;

      end;

        suppose n = 0 ;

        then (((M1 @ ) * (M2 @ )) * ((M1 @ ) * (M2 @ ))) = ((M1 @ ) * (M2 @ )) by MATRIX_0: 45;

        hence thesis;

      end;

    end;

    theorem :: MATRIX_8:13

    M1 is Idempotent & M2 is Idempotent & M1 is invertible implies (M1 * M2) is Idempotent

    proof

      assume that

       A1: M1 is Idempotent and

       A2: M2 is Idempotent and

       A3: M1 is invertible;

      M1 = ( 1. (K,n)) by A1, A3, Th10;

      hence thesis by A2, MATRIX_3: 18;

    end;

    theorem :: MATRIX_8:14

    M1 is Idempotent Orthogonal implies M1 is symmetric

    proof

      assume

       A1: M1 is Idempotent Orthogonal;

      then M1 is invertible by MATRIX_6:def 7;

      then M1 = ( 1. (K,n)) by A1, Th10;

      hence thesis;

    end;

    theorem :: MATRIX_8:15

    (M2 * M1) = ( 1. (K,n)) implies (M1 * M2) is Idempotent

    proof

      assume

       A1: (M2 * M1) = ( 1. (K,n));

      

       A2: ( len M1) = n & ( width M1) = n by MATRIX_0: 24;

      

       A3: ( width M2) = n by MATRIX_0: 24;

      

       A4: ( len M2) = n by MATRIX_0: 24;

      ( width (M1 * M2)) = n by MATRIX_0: 24;

      

      then ((M1 * M2) * (M1 * M2)) = (((M1 * M2) * M1) * M2) by 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 thesis;

    end;

    theorem :: MATRIX_8:16

    M1 is Idempotent Orthogonal implies M1 = ( 1. (K,n)) by Th10, MATRIX_6:def 7;

    theorem :: MATRIX_8:17

    M1 is symmetric implies (M1 * (M1 @ )) is symmetric

    proof

      assume

       A1: M1 is symmetric;

      per cases by NAT_1: 3;

        suppose

         A2: n > 0 ;

        

         A3: ( width M1) = n & ( len M1) = n by MATRIX_0: 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 thesis by MATRIX_6:def 5;

      end;

        suppose n = 0 ;

        then ((M1 * (M1 @ )) @ ) = (M1 * (M1 @ )) by MATRIX_0: 45;

        hence thesis by MATRIX_6:def 5;

      end;

    end;

    theorem :: MATRIX_8:18

    M1 is symmetric implies ((M1 @ ) * M1) is symmetric

    proof

      assume

       A1: M1 is symmetric;

      per cases by NAT_1: 3;

        suppose

         A2: n > 0 ;

        

         A3: ( width M1) = n & ( len M1) = n by MATRIX_0: 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 thesis by MATRIX_6:def 5;

      end;

        suppose n = 0 ;

        then (((M1 @ ) * M1) @ ) = ((M1 @ ) * M1) by MATRIX_0: 45;

        hence thesis by MATRIX_6:def 5;

      end;

    end;

    theorem :: MATRIX_8:19

    M1 is invertible & (M1 * M2) = (M1 * M3) implies M2 = M3

    proof

      assume that

       A1: M1 is invertible and

       A2: (M1 * M2) = (M1 * M3);

      

       A3: (M1 ~ ) is_reverse_of M1 by A1, MATRIX_6:def 4;

      

       A4: ( len M2) = n by MATRIX_0: 24;

      

       A5: ( width M1) = n & ( len M1) = n by MATRIX_0: 24;

      

       A6: ( len M3) = n by MATRIX_0: 24;

      

       A7: ( width (M1 ~ )) = n by MATRIX_0: 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 thesis;

    end;

    theorem :: MATRIX_8:20

    M1 is invertible & (M2 * M1) = (M3 * M1) implies M2 = M3

    proof

      assume that

       A1: M1 is invertible and

       A2: (M2 * M1) = (M3 * M1);

      

       A3: (M1 ~ ) is_reverse_of M1 by A1, MATRIX_6:def 4;

      

       A4: ( width M2) = n by MATRIX_0: 24;

      

       A5: ( width M1) = n & ( len M1) = n by MATRIX_0: 24;

      

       A6: ( width M3) = n by MATRIX_0: 24;

      

       A7: ( len (M1 ~ )) = n by MATRIX_0: 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 thesis;

    end;

    theorem :: MATRIX_8:21

    M1 is invertible & (M2 * M1) = ( 0. (K,n)) implies M2 = ( 0. (K,n))

    proof

      assume that

       A1: M1 is invertible and

       A2: (M2 * M1) = ( 0. (K,n));

      

       A3: (M1 ~ ) is_reverse_of M1 by A1, MATRIX_6:def 4;

      

       A4: ( width M2) = n by MATRIX_0: 24;

      

       A5: ( width M1) = n & ( len M1) = n by MATRIX_0: 24;

      

       A6: ( width (M1 ~ )) = n by MATRIX_0: 24;

      

       A7: ( len (M1 ~ )) = n by MATRIX_0: 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 thesis;

    end;

    theorem :: MATRIX_8:22

    M1 is invertible & (M2 * M1) = ( 0. (K,n)) implies M2 = ( 0. (K,n))

    proof

      assume that

       A1: M1 is invertible and

       A2: (M2 * M1) = ( 0. (K,n));

      

       A3: (M1 ~ ) is_reverse_of M1 by A1, MATRIX_6:def 4;

      

       A4: ( width M2) = n by MATRIX_0: 24;

      

       A5: ( width M1) = n & ( len M1) = n by MATRIX_0: 24;

      

       A6: ( width (M1 ~ )) = n by MATRIX_0: 24;

      

       A7: ( len (M1 ~ )) = n by MATRIX_0: 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 thesis;

    end;

    theorem :: MATRIX_8:23

    M1 is Nilpotent & M1 commutes_with M2 & n > 0 implies (M1 * M2) is Nilpotent

    proof

      assume that

       A1: M1 is Nilpotent and

       A2: M1 commutes_with M2 and

       A3: n > 0 ;

      

       A4: ( len M1) = n & ( width M1) = n by MATRIX_0: 24;

      

       A5: ( width M2) = n by MATRIX_0: 24;

      

       A6: ( width (M2 * M1)) = n by MATRIX_0: 24;

      

       A7: ( len M2) = n by MATRIX_0: 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

      .= (( 0. (K,n,n)) * M2) by A3, A7, A5, MATRIX_6: 2

      .= ( 0. (K,n)) by A7, A5, MATRIX_6: 1;

      hence thesis;

    end;

    theorem :: MATRIX_8:24

    n > 0 & M1 is Nilpotent & M2 is Nilpotent & M1 commutes_with M2 & (M1 * M2) = ( 0. (K,n)) implies (M1 + M2) is Nilpotent

    proof

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

      

       A5: (M1 * M2) = ( 0. (K,n,n)) by A4;

      

       A6: (M1 * M1) = ( 0. (K,n)) & (M2 * M2) = ( 0. (K,n)) by A2;

      ((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 thesis;

    end;

    theorem :: MATRIX_8:25

    M1 is Nilpotent & M2 is Nilpotent & (M1 * M2) = ( - (M2 * M1)) & n > 0 implies (M1 + M2) is Nilpotent

    proof

      assume that

       A1: M1 is Nilpotent & M2 is Nilpotent and

       A2: (M1 * M2) = ( - (M2 * M1)) and

       A3: n > 0 ;

      

       A4: (M1 * M1) = ( 0. (K,n)) & (M2 * M2) = ( 0. (K,n)) by A1;

      

       A5: ( len (M1 * M1)) = n & ( width (M1 * M1)) = n by MATRIX_0: 24;

      

       A6: ( len M1) = n & ( width M1) = n by MATRIX_0: 24;

      

       A7: ( len ((M1 * M1) + (M2 * M1))) = n & ( width ((M1 * M1) + (M2 * M1))) = n by MATRIX_0: 24;

      

       A8: ( len (M2 * M1)) = n & ( width (M2 * M1)) = n by MATRIX_0: 24;

      

       A9: ( len (M1 * M2)) = n & ( width (M1 * M2)) = n by MATRIX_0: 24;

      

       A10: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

      ( len (M1 + M2)) = n & ( width (M1 + M2)) = n by MATRIX_0: 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 thesis;

    end;

    theorem :: MATRIX_8:26

    M1 is Nilpotent & n > 0 implies (M1 @ ) is Nilpotent

    proof

      assume that

       A1: M1 is Nilpotent and

       A2: n > 0 ;

      ( len M1) = n & ( width M1) = n by MATRIX_0: 24;

      

      then ((M1 @ ) * (M1 @ )) = ((M1 * M1) @ ) by A2, MATRIX_3: 22

      .= (( 0. (K,n)) @ ) by A1

      .= ((n,n) --> ( 0. K)) by MATRIX_6: 20

      .= ( 0. (K,n));

      hence thesis;

    end;

    theorem :: MATRIX_8:27

    M1 is Nilpotent Idempotent implies M1 = ( 0. (K,n));

    theorem :: MATRIX_8:28

    

     Th28: n > 0 implies ( 0. (K,n)) <> ( 1. (K,n))

    proof

      

       A1: ( Indices ( 1. (K,n))) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume n > 0 ;

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

      ( Indices ( 0. (K,n))) = ( Indices ( 1. (K,n))) by MATRIX_0: 26;

      then (( 0. (K,n)) * (1,1)) = ( 0. K) by A2, A1, MATRIX_1: 1;

      then ( 0. K) = ( 1. K) by A2, A3, A1, MATRIX_1:def 3;

      hence contradiction;

    end;

    theorem :: MATRIX_8:29

    n > 0 & M1 is Nilpotent implies not M1 is invertible

    proof

      assume that

       A1: n > 0 and

       A2: M1 is Nilpotent;

      

       A3: ( len M1) = n & ( width M1) = n by MATRIX_0: 24;

      assume M1 is invertible;

      then

      consider M2 be Matrix of n, K such that

       A4: M1 is_reverse_of M2 by MATRIX_6:def 3;

      

       A5: ( width M2) = n by MATRIX_0: 24;

      

       A6: ( len M2) = n by MATRIX_0: 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

      .= ( 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;

    end;

    theorem :: MATRIX_8:30

    M1 is Self_Reversible implies M1 is Involutory

    proof

      assume

       A1: M1 is Self_Reversible;

      then M1 is invertible;

      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;

      hence thesis by A2;

    end;

    theorem :: MATRIX_8:31

    ( 1. (K,n)) is Self_Reversible by MATRIX_6: 8;

    theorem :: MATRIX_8:32

    M1 is Self_Reversible Idempotent implies M1 = ( 1. (K,n))

    proof

      assume

       A1: M1 is Self_Reversible Idempotent;

      then M1 is invertible;

      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;

      hence thesis by A1;

    end;

    theorem :: MATRIX_8:33

    M1 is Self_Reversible symmetric implies M1 is Orthogonal

    proof

      assume

       A1: M1 is Self_Reversible symmetric;

      then

       A2: M1 = (M1 @ ) by MATRIX_6:def 5;

      M1 is invertible & M1 = (M1 ~ ) by A1;

      hence thesis by A2, MATRIX_6:def 7;

    end;

    definition

      let n be Nat, K be Field, M1,M2 be Matrix of n, K;

      :: MATRIX_8:def5

      pred M1 is_similar_to M2 means ex M be Matrix of n, K st M is invertible & M1 = (((M ~ ) * M2) * M);

      reflexivity

      proof

        let M1 be Matrix of n, K;

        take ( 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 thesis;

      end;

      symmetry

      proof

        let M1,M2 be Matrix of n, K;

        given M be Matrix of n, K such that

         A1: M is invertible and

         A2: M1 = (((M ~ ) * M2) * M);

        

         A3: (M ~ ) is_reverse_of M by A1, MATRIX_6:def 4;

        take (M ~ );

        

         A4: ( width M2) = n by MATRIX_0: 24;

        

         A5: ( len M) = n by MATRIX_0: 24;

        

         A6: ( len M2) = n & ( width (M ~ )) = n by MATRIX_0: 24;

        

         A7: ( width M) = n by MATRIX_0: 24;

        

         A8: ( len ((M ~ ) * M2)) = n & ( width ((M ~ ) * M2)) = n by MATRIX_0: 24;

        

         A9: ( len (M ~ )) = n by MATRIX_0: 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 thesis by A1;

      end;

    end

    theorem :: MATRIX_8:34

    M1 is_similar_to M2 & M2 is_similar_to M3 implies M1 is_similar_to M3

    proof

      assume that

       A1: M1 is_similar_to M2 and

       A2: M2 is_similar_to M3;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 ~ ) * M2) * M4) by A1;

      consider M5 be Matrix of n, K such that

       A5: M5 is invertible and

       A6: M2 = (((M5 ~ ) * M3) * M5) by A2;

      

       A7: ( len M5) = n by MATRIX_0: 24;

      take (M5 * M4);

      

       A8: ( width ((M5 * M4) ~ )) = n by MATRIX_0: 24;

      

       A9: ( len (M3 * M5)) = n & ( width (M3 * M5)) = n by MATRIX_0: 24;

      

       A10: ( len M4) = n by MATRIX_0: 24;

      

       A11: ( width M5) = n by MATRIX_0: 24;

      

       A12: ( len M3) = n by MATRIX_0: 24;

      

       A13: ( len (M5 * M4)) = n by MATRIX_0: 24;

      

       A14: ( width (M4 ~ )) = n by MATRIX_0: 24;

      

       A15: ( len (M5 ~ )) = n & ( width (M5 ~ )) = n by MATRIX_0: 24;

      

       A16: ( width M3) = n by MATRIX_0: 24;

      ( len ((M5 ~ ) * M3)) = n & ( width ((M5 ~ ) * M3)) = n by MATRIX_0: 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 thesis by A3, A5, MATRIX_6: 36;

    end;

    theorem :: MATRIX_8:35

    M1 is_similar_to M2 & M2 is Idempotent implies M1 is Idempotent

    proof

      assume that

       A1: M1 is_similar_to M2 and

       A2: M2 is Idempotent;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 ~ ) * M2) * M4) by A1;

      

       A5: (M4 ~ ) is_reverse_of M4 by A3, MATRIX_6:def 4;

      

       A6: ( width M4) = n by MATRIX_0: 24;

      

       A7: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

      

       A8: ( len (M2 * M4)) = n & ( width (((M4 ~ ) * M2) * M4)) = n by MATRIX_0: 24;

      

       A9: ( len (M4 ~ )) = n by MATRIX_0: 24;

      

       A10: ( width ((M4 ~ ) * M2)) = n by MATRIX_0: 24;

      

       A11: ( width (M4 ~ )) = n by MATRIX_0: 24;

      

       A12: ( len M4) = n by MATRIX_0: 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;

      hence thesis;

    end;

    theorem :: MATRIX_8:36

    M1 is_similar_to M2 & M2 is Nilpotent & n > 0 implies M1 is Nilpotent

    proof

      assume that

       A1: M1 is_similar_to M2 and

       A2: M2 is Nilpotent and

       A3: n > 0 ;

      consider M4 be Matrix of n, K such that

       A4: M4 is invertible and

       A5: M1 = (((M4 ~ ) * M2) * M4) by A1;

      

       A6: (M4 ~ ) is_reverse_of M4 by A4, MATRIX_6:def 4;

      

       A7: ( width M4) = n by MATRIX_0: 24;

      

       A8: ( width (M4 ~ )) = n by MATRIX_0: 24;

      

       A9: ( width ((M4 ~ ) * M2)) = n by MATRIX_0: 24;

      

       A10: ( len (M4 ~ )) = n by MATRIX_0: 24;

      

       A11: ( len (M2 * M4)) = n & ( width (((M4 ~ ) * M2) * M4)) = n by MATRIX_0: 24;

      

       A12: ( len M4) = n by MATRIX_0: 24;

      

       A13: ( len M2) = n & ( width M2) = n by MATRIX_0: 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

      .= (( 0. (K,n,n)) * M4) by A3, A10, A8, MATRIX_6: 2

      .= ( 0. (K,n)) by A12, A7, MATRIX_6: 1;

      hence thesis;

    end;

    theorem :: MATRIX_8:37

    M1 is_similar_to M2 & M2 is Involutory implies M1 is Involutory

    proof

      assume that

       A1: M1 is_similar_to M2 and

       A2: M2 is Involutory;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 ~ ) * M2) * M4) by A1;

      

       A5: (M4 ~ ) is_reverse_of M4 by A3, MATRIX_6:def 4;

      

       A6: ( width ((M4 ~ ) * M2)) = n by MATRIX_0: 24;

      

       A7: ( width (M4 ~ )) = n by MATRIX_0: 24;

      

       A8: ( len (M2 * M4)) = n & ( width (((M4 ~ ) * M2) * M4)) = n by MATRIX_0: 24;

      

       A9: ( len (M4 ~ )) = n by MATRIX_0: 24;

      

       A10: ( width M4) = n by MATRIX_0: 24;

      

       A11: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

      

       A12: ( len M4) = n by MATRIX_0: 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

      .= ((M4 ~ ) * M4) by MATRIX_3: 19

      .= ( 1. (K,n)) by A5, MATRIX_6:def 2;

      hence thesis;

    end;

    theorem :: MATRIX_8:38

    M1 is_similar_to M2 & n > 0 implies (M1 + ( 1. (K,n))) is_similar_to (M2 + ( 1. (K,n)))

    proof

      assume that

       A1: M1 is_similar_to M2 and

       A2: n > 0 ;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 ~ ) * M2) * M4) by A1;

      

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

      

       A7: ( width ((M4 ~ ) * M2)) = n by MATRIX_0: 24;

      

       A8: ( len M4) = n & ( len ((M4 ~ ) * M2)) = n by MATRIX_0: 24;

      take M4;

      

       A9: ( len (M4 ~ )) = n & ( width (M4 ~ )) = n by MATRIX_0: 24;

      ( len M2) = n & ( width M2) = n by MATRIX_0: 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 thesis by A3;

    end;

    theorem :: MATRIX_8:39

    M1 is_similar_to M2 & n > 0 implies (M1 + M1) is_similar_to (M2 + M2)

    proof

      assume that

       A1: M1 is_similar_to M2 and

       A2: n > 0 ;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 ~ ) * M2) * M4) by A1;

      

       A5: ( width ((M4 ~ ) * M2)) = n by MATRIX_0: 24;

      take M4;

      

       A6: ( len M4) = n & ( len ((M4 ~ ) * M2)) = n by MATRIX_0: 24;

      

       A7: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

      ( len (M4 ~ )) = n & ( width (M4 ~ )) = n by MATRIX_0: 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 thesis by A3;

    end;

    theorem :: MATRIX_8:40

    M1 is_similar_to M2 & n > 0 implies ((M1 + M1) + M1) is_similar_to ((M2 + M2) + M2)

    proof

      assume that

       A1: M1 is_similar_to M2 and

       A2: n > 0 ;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 ~ ) * M2) * M4) by A1;

      

       A5: ( len M4) = n & ( len ((M4 ~ ) * M2)) = n by MATRIX_0: 24;

      

       A6: ( width ((M4 ~ ) * M2)) = n by MATRIX_0: 24;

      

       A7: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

      

       A8: ( len (M4 ~ )) = n & ( width (M4 ~ )) = n by MATRIX_0: 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;

      

       A10: ( len ((M4 ~ ) * (M2 + M2))) = n & ( width ((M4 ~ ) * (M2 + M2))) = n by MATRIX_0: 24;

      ( len (M2 + M2)) = n & ( width (M2 + M2)) = n by MATRIX_0: 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 thesis by A3;

    end;

    theorem :: MATRIX_8:41

    M1 is invertible implies (M2 * M1) is_similar_to (M1 * M2)

    proof

      

       A1: ( len M2) = n & ( width (M1 ~ )) = n by MATRIX_0: 24;

      assume

       A2: M1 is invertible;

      then

       A3: (M1 ~ ) is_reverse_of M1 by MATRIX_6:def 4;

      take M1;

      ( len M1) = n & ( width M1) = n by MATRIX_0: 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 thesis by A2;

    end;

    theorem :: MATRIX_8:42

    M2 is invertible & M1 is_similar_to M2 implies M1 is invertible

    proof

      assume that

       A1: M2 is invertible and

       A2: M1 is_similar_to M2;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 ~ ) * M2) * M4) by A2;

      (M4 ~ ) is invertible by A3;

      then ((M4 ~ ) * M2) is invertible by A1, MATRIX_6: 36;

      hence thesis by A3, A4, MATRIX_6: 36;

    end;

    theorem :: MATRIX_8:43

    M2 is invertible & M1 is_similar_to M2 implies (M1 ~ ) is_similar_to (M2 ~ )

    proof

      assume that

       A1: M2 is invertible and

       A2: M1 is_similar_to M2;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 ~ ) * M2) * M4) by A2;

      

       A5: (M4 ~ ) is invertible & ((M4 ~ ) ~ ) = M4 by A3, MATRIX_6: 16;

      take M4;

      

       A6: ( width (M4 ~ )) = n & ( len M4) = n by MATRIX_0: 24;

      

       A7: ( len M2) = n & ( width M2) = n by MATRIX_0: 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 thesis by A3;

    end;

    definition

      let n be Nat, K be Field, M1,M2 be Matrix of n, K;

      :: MATRIX_8:def6

      pred M1 is_congruent_Matrix_of M2 means ex M be Matrix of n, K st M is invertible & M1 = (((M @ ) * M2) * M);

      reflexivity

      proof

        set M = ( 1. (K,n));

        let M1 be Matrix of n, K;

        (((M @ ) * M1) * M) = ((M * M1) * M) by MATRIX_6: 10

        .= (M1 * M) by MATRIX_3: 18

        .= M1 by MATRIX_3: 19;

        hence thesis;

      end;

    end

    theorem :: MATRIX_8:44

    M1 is_congruent_Matrix_of M2 & n > 0 implies M2 is_congruent_Matrix_of M1

    proof

      assume that

       A1: M1 is_congruent_Matrix_of M2 and

       A2: n > 0 ;

      consider M be Matrix of n, K such that

       A3: M is invertible and

       A4: M1 = (((M @ ) * M2) * M) by A1;

      

       A5: (M ~ ) is_reverse_of M by A3, MATRIX_6:def 4;

      take (M ~ );

      

       A6: ( width (M ~ )) = n by MATRIX_0: 24;

      

       A7: ( len (M @ )) = n & ( width (M @ )) = n by MATRIX_0: 24;

      

       A8: ( width M) = n by MATRIX_0: 24;

      

       A9: ( len (M ~ )) = n by MATRIX_0: 24;

      ( len M) = n & ( width ((M @ ) * M2)) = n by MATRIX_0: 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_0: 24;

      

       A12: ( width ((M ~ ) @ )) = n by MATRIX_0: 24;

      ( len M1) = n & ( width M1) = n by MATRIX_0: 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 thesis by A3;

    end;

    theorem :: MATRIX_8:45

    M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 implies M1 is_congruent_Matrix_of M3

    proof

      assume that

       A1: M1 is_congruent_Matrix_of M2 and

       A2: M2 is_congruent_Matrix_of M3 and

       A3: n > 0 ;

      

       A4: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

      consider M4 be Matrix of n, K such that

       A5: M4 is invertible and

       A6: M1 = (((M4 @ ) * M2) * M4) by A1;

      

       A7: ( len M4) = n by MATRIX_0: 24;

      consider M5 be Matrix of n, K such that

       A8: M5 is invertible and

       A9: M2 = (((M5 @ ) * M3) * M5) by A2;

      

       A10: ( len M5) = n by MATRIX_0: 24;

      

       A11: ( len M3) = n & ( len (M5 @ )) = n by MATRIX_0: 24;

      

       A12: ( width M5) = n by MATRIX_0: 24;

      take (M5 * M4);

      

       A13: ( len ((M5 @ ) * M3)) = n & ( len (M5 * M4)) = n by MATRIX_0: 24;

      

       A14: ( width (M4 @ )) = n by MATRIX_0: 24;

      

       A15: ( width (M5 @ )) = n by MATRIX_0: 24;

      

       A16: ( width ((M5 @ ) * M3)) = n by MATRIX_0: 24;

      ( width M4) = n by MATRIX_0: 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 thesis by A5, A8, MATRIX_6: 36;

    end;

    theorem :: MATRIX_8:46

    M1 is_congruent_Matrix_of M2 & n > 0 implies (M1 + M1) is_congruent_Matrix_of (M2 + M2)

    proof

      assume that

       A1: M1 is_congruent_Matrix_of M2 and

       A2: n > 0 ;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 @ ) * M2) * M4) by A1;

      

       A5: ( width ((M4 @ ) * M2)) = n by MATRIX_0: 24;

      take M4;

      

       A6: ( len M4) = n & ( len ((M4 @ ) * M2)) = n by MATRIX_0: 24;

      

       A7: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

      ( len (M4 @ )) = n & ( width (M4 @ )) = n by MATRIX_0: 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 thesis by A3;

    end;

    theorem :: MATRIX_8:47

    M1 is_congruent_Matrix_of M2 & n > 0 implies ((M1 + M1) + M1) is_congruent_Matrix_of ((M2 + M2) + M2)

    proof

      assume that

       A1: M1 is_congruent_Matrix_of M2 and

       A2: n > 0 ;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 @ ) * M2) * M4) by A1;

      

       A5: ( len M4) = n & ( len ((M4 @ ) * M2)) = n by MATRIX_0: 24;

      

       A6: ( width ((M4 @ ) * M2)) = n by MATRIX_0: 24;

      

       A7: ( len M2) = n & ( width M2) = n by MATRIX_0: 24;

      

       A8: ( len (M4 @ )) = n & ( width (M4 @ )) = n by MATRIX_0: 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;

      

       A10: ( len ((M4 @ ) * (M2 + M2))) = n & ( width ((M4 @ ) * (M2 + M2))) = n by MATRIX_0: 24;

      ( len (M2 + M2)) = n & ( width (M2 + M2)) = n by MATRIX_0: 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 thesis by A3;

    end;

    theorem :: MATRIX_8:48

    M1 is Orthogonal implies (M2 * M1) is_congruent_Matrix_of (M1 * M2)

    proof

      

       A1: ( len M2) = n & ( width (M1 ~ )) = n by MATRIX_0: 24;

      assume

       A2: M1 is Orthogonal;

      then M1 is invertible by MATRIX_6:def 7;

      then

       A3: (M1 ~ ) is_reverse_of M1 by MATRIX_6:def 4;

      take M1;

      ( len M1) = n & ( width M1) = n by MATRIX_0: 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 thesis by A2, MATRIX_6:def 7;

    end;

    theorem :: MATRIX_8:49

    M2 is invertible & M1 is_congruent_Matrix_of M2 & n > 0 implies M1 is invertible

    proof

      assume that

       A1: M2 is invertible and

       A2: M1 is_congruent_Matrix_of M2 and

       A3: n > 0 ;

      consider M4 be Matrix of n, K such that

       A4: M4 is invertible and

       A5: M1 = (((M4 @ ) * M2) * M4) by A2;

      set M6 = ((M4 ~ ) @ );

      set M5 = (M4 @ );

      

       A6: ( width M4) = n & ( width (M4 ~ )) = n by MATRIX_0: 24;

      ( len M4) = n by MATRIX_0: 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: (M5 * M6) = ( 1. (K,n)) by A7, MATRIX_6: 10;

      ( len (M4 ~ )) = n by MATRIX_0: 24;

      then ((M4 * (M4 ~ )) @ ) = (((M4 ~ ) @ ) * (M4 @ )) by A3, A6, MATRIX_3: 22;

      then (M5 * M6) = (M6 * M5) by A8, A7, MATRIX_6:def 2;

      then M5 is_reverse_of M6 by A9, MATRIX_6:def 2;

      then M5 is invertible by MATRIX_6:def 3;

      then (M5 * M2) is invertible by A1, MATRIX_6: 36;

      hence thesis by A4, A5, MATRIX_6: 36;

    end;

    theorem :: MATRIX_8:50

    M1 is_congruent_Matrix_of M2 & n > 0 implies (M1 @ ) is_congruent_Matrix_of (M2 @ )

    proof

      assume that

       A1: M1 is_congruent_Matrix_of M2 and

       A2: n > 0 ;

      consider M4 be Matrix of n, K such that

       A3: M4 is invertible and

       A4: M1 = (((M4 @ ) * M2) * M4) by A1;

      

       A5: ( width (M4 @ )) = n by MATRIX_0: 24;

      

       A6: ( width (M2 * M4)) = n & ( len (M2 * M4)) = n by MATRIX_0: 24;

      

       A7: ( len M2) = n by MATRIX_0: 24;

      

       A8: ( width M2) = n by MATRIX_0: 24;

      take M4;

      

       A9: ( len M4) = n by MATRIX_0: 24;

      

       A10: ( width M4) = n by MATRIX_0: 24;

      

      then (((M4 @ ) * (M2 @ )) * M4) = (((M4 @ ) * (M2 @ )) * ((M4 @ ) @ )) by A2, A9, MATRIX_0: 57

      .= (((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 thesis by A3;

    end;

    theorem :: MATRIX_8:51

    M4 is Orthogonal implies (((M4 @ ) * M2) * M4) is_similar_to M2

    proof

      assume

       A1: M4 is Orthogonal;

      take M4;

      thus thesis by A1, MATRIX_6:def 7;

    end;

    definition

      let n be Nat, K be Field, M be Matrix of n, K;

      :: MATRIX_8:def7

      func Trace M -> Element of K equals ( Sum ( diagonal_of_Matrix M));

      coherence ;

    end

    theorem :: MATRIX_8:52

    ( Trace M1) = ( Trace (M1 @ ))

    proof

      

       A1: for i be Nat st i in ( Seg n) holds (( diagonal_of_Matrix M1) . i) = (( diagonal_of_Matrix (M1 @ )) . i)

      proof

        let i be Nat;

        assume

         A2: i in ( Seg n);

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

        then [i, i] in ( Indices M1) by A2, ZFMISC_1: 87;

        hence thesis by A3, MATRIX_0:def 6;

      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 thesis by A1, A4, FINSEQ_1: 13;

    end;

    theorem :: MATRIX_8:53

    

     Th53: ( Trace (M1 + M2)) = (( Trace M1) + ( Trace M2))

    proof

      

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

        assume i in ( dom ( diagonal_of_Matrix M1));

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

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

    end;

    theorem :: MATRIX_8:54

    ( Trace ((M1 + M2) + M3)) = ((( Trace M1) + ( Trace M2)) + ( Trace M3))

    proof

      ( Trace ((M1 + M2) + M3)) = (( Trace (M1 + M2)) + ( Trace M3)) by Th53;

      hence thesis by Th53;

    end;

    theorem :: MATRIX_8:55

    

     Th55: ( Trace ( 0. (K,n))) = ( 0. K)

    proof

      ( 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 st i in ( dom ( diagonal_of_Matrix ( 0. (K,n)))) holds (( diagonal_of_Matrix ( 0. (K,n))) /. i) = ( 0. K)

      proof

        let i;

        assume

         A2: i in ( dom ( diagonal_of_Matrix ( 0. (K,n))));

        ( Indices ( 0. (K,n))) = [:( Seg n), ( Seg n):] by MATRIX_0: 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 thesis by A2, A3, PARTFUN1:def 6;

      end;

      hence thesis by MATRLIN: 11;

    end;

    theorem :: MATRIX_8:56

    

     Th56: ( Trace ( - M1)) = ( - ( Trace M1))

    proof

      

       A1: ( len M1) = n & ( width M1) = n by MATRIX_0: 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 thesis by RLVECT_1: 6;

    end;

    theorem :: MATRIX_8:57

    ( - ( Trace ( - M1))) = ( Trace M1)

    proof

      

       A1: ( len M1) = n & ( width M1) = n by MATRIX_0: 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 thesis by RLVECT_1: 6;

    end;

    theorem :: MATRIX_8:58

    ( Trace (M1 + ( - M1))) = ( 0. K)

    proof

      ( len M1) = n & ( width M1) = n by MATRIX_0: 24;

      

      then ( Trace (M1 + ( - M1))) = ( Trace ( 0. (K,n,n))) by MATRIX_4: 2

      .= ( Trace ( 0. (K,n)))

      .= ( 0. K) by Th55;

      hence thesis;

    end;

    theorem :: MATRIX_8:59

    

     Th59: ( Trace (M1 - M2)) = (( Trace M1) - ( Trace M2))

    proof

      ( Trace (M1 - M2)) = (( Trace M1) + ( Trace ( - M2))) by Th53

      .= (( Trace M1) + ( - ( Trace M2))) by Th56;

      hence thesis;

    end;

    theorem :: MATRIX_8:60

    ( Trace ((M1 - M2) + M3)) = ((( Trace M1) - ( Trace M2)) + ( Trace M3))

    proof

      ( Trace ((M1 - M2) + M3)) = (( Trace (M1 - M2)) + ( Trace M3)) by Th53

      .= ((( Trace M1) - ( Trace M2)) + ( Trace M3)) by Th59;

      hence thesis;

    end;

    theorem :: MATRIX_8:61

    ( Trace ((M1 + M2) - M3)) = ((( Trace M1) + ( Trace M2)) - ( Trace M3))

    proof

      ( Trace ((M1 + M2) - M3)) = (( Trace (M1 + M2)) - ( Trace M3)) by Th59

      .= ((( Trace M1) + ( Trace M2)) - ( Trace M3)) by Th53;

      hence thesis;

    end;

    theorem :: MATRIX_8:62

    ( Trace ((M1 - M2) - M3)) = ((( Trace M1) - ( Trace M2)) - ( Trace M3))

    proof

      ( Trace ((M1 - M2) - M3)) = (( Trace (M1 - M2)) - ( Trace M3)) by Th59

      .= ((( Trace M1) - ( Trace M2)) - ( Trace M3)) by Th59;

      hence thesis;

    end;