matrix_6.miz

    begin

    reserve i,j,n for Nat,

K for Field,

a for Element of K,

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

    reserve A for Matrix of K;

    definition

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

      :: MATRIX_6:def1

      pred M1 commutes_with M2 means (M1 * M2) = (M2 * M1);

      reflexivity ;

      symmetry ;

    end

    definition

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

      :: MATRIX_6:def2

      pred M1 is_reverse_of M2 means (M1 * M2) = (M2 * M1) & (M1 * M2) = ( 1. (K,n));

      symmetry ;

    end

    definition

      let n be Nat, K be Field;

      let M1 be Matrix of n, K;

      :: MATRIX_6:def3

      attr M1 is invertible means ex M2 be Matrix of n, K st M1 is_reverse_of M2;

    end

    registration

      let n;

      let K be Ring;

      let M1 be Matrix of n, K;

      cluster ( - M1) -> n, n -size;

      coherence

      proof

        ( len M1) = n by MATRIX_0: 24;

        then

         A1: ( len ( - M1)) = n by MATRIX_3:def 2;

        ( width M1) = n by MATRIX_0: 24;

        then ( width ( - M1)) = n by MATRIX_3:def 2;

        hence thesis by A1, MATRIX_0: 51;

      end;

    end

    registration

      let n;

      let K be Ring;

      let M1,M2 be Matrix of n, K;

      cluster (M1 + M2) -> n, n -size;

      coherence

      proof



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

        ( width M1) = n by MATRIX_0: 24;

        then ( len (M1 + M2)) = ( len M1) & ( width (M1 + M2)) = ( width M2) by A1, MATRIX_3:def 3;

        hence thesis by A1, MATRIX_0: 24, MATRIX_0: 51;

      end;

    end

    registration

      let n;

      let K be Field;

      let M1,M2 be Matrix of n, K;

      cluster (M1 - M2) -> n, n -size;

      coherence ;

    end

    registration

      let n;

      let K be Ring;

      let M1,M2 be Matrix of n, K;

      cluster (M1 * M2) -> n, n -size;

      coherence

      proof

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

        then

         A1: ( len (M1 * M2)) = ( len M1) & ( width (M1 * M2)) = ( width M2) by MATRIX_3:def 4;

        ( width M2) = n by MATRIX_0: 24;

        hence thesis by A1, MATRIX_0: 24, MATRIX_0: 51;

      end;

    end

    theorem :: MATRIX_6:1



     Th1: for K be Field, A be Matrix of K holds (( 0. (K,( len A),( len A))) * A) = ( 0. (K,( len A),( width A)))

    proof

      let K, A;

      per cases by NAT_1: 3;

        suppose

         A1: ( len A) > 0 ;

        set B = (( 0. (K,( len A),( len A))) * A);



         A2: ( width ( - (( 0. (K,( len A),( len A))) * A))) = ( width (( 0. (K,( len A),( len A))) * A)) by MATRIX_3:def 2;



         A3: ( len ( 0. (K,( len A),( len A)))) = ( len A) by MATRIX_0:def 2;

        then

         A4: ( width ( 0. (K,( len A),( len A)))) = ( len A) by A1, MATRIX_0: 20;

        then

         A5: ( len (( 0. (K,( len A),( len A))) * A)) = ( len A) by A3, MATRIX_3:def 4;



         A6: ( width (( 0. (K,( len A),( len A))) * A)) = ( width A) by A4, MATRIX_3:def 4;

        (( 0. (K,( len A),( len A))) * A) = ((( 0. (K,( len A),( len A))) + ( 0. (K,( len A),( len A)))) * A) by MATRIX_3: 4

        .= ((( 0. (K,( len A),( len A))) * A) + (( 0. (K,( len A),( len A))) * A)) by A1, A3, A4, MATRIX_4: 63;

        then ( len ( - (( 0. (K,( len A),( len A))) * A))) = ( len (( 0. (K,( len A),( len A))) * A)) & ( 0. (K,( len A),( width A))) = ((B + B) + ( - B)) by A5, A6, MATRIX_3:def 2, MATRIX_4: 2;



        then ( 0. (K,( len A),( width A))) = (B + (B - B)) by A2, MATRIX_3: 3

        .= (( 0. (K,( len A),( len A))) * A) by A5, A2, MATRIX_4: 20;

        hence thesis;

      end;

        suppose

         A7: ( len A) = 0 ;

        then ( len ( 0. (K,( len A),( len A)))) = 0 by MATRIX_0:def 2;

        then ( width ( 0. (K,( len A),( len A)))) = ( len A) by A7, MATRIX_0:def 3;

        then

         A8: ( len (( 0. (K,( len A),( len A))) * A)) = ( len ( 0. (K,( len A),( len A)))) by MATRIX_3:def 4;

        ( len ( 0. (K,( len A),( len A)))) = ( len A) & ( len ( 0. (K,( len A),( width A)))) = ( len A) by MATRIX_0:def 2;

        hence thesis by A7, A8, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_6:2



     Th2: for K be Field, A be Matrix of K st ( width A) > 0 holds (A * ( 0. (K,( width A),( width A)))) = ( 0. (K,( len A),( width A)))

    proof

      let K, A;



       A1: ( width ( - (A * ( 0. (K,( width A),( width A)))))) = ( width (A * ( 0. (K,( width A),( width A))))) by MATRIX_3:def 2;

      set B = (A * ( 0. (K,( width A),( width A))));

      assume

       A2: ( width A) > 0 ;

      then

       A3: ( len A) > 0 by MATRIX_0:def 3;



       A4: ( len ( 0. (K,( width A),( width A)))) = ( width A) by MATRIX_0:def 2;

      then

       A5: ( len (A * ( 0. (K,( width A),( width A))))) = ( len A) by MATRIX_3:def 4;



       A6: ( width ( 0. (K,( width A),( width A)))) = ( width A) by A2, A4, MATRIX_0: 20;

      then

       A7: ( width (A * ( 0. (K,( width A),( width A))))) = ( width A) by A4, MATRIX_3:def 4;

      (A * ( 0. (K,( width A),( width A)))) = (A * (( 0. (K,( width A),( width A))) + ( 0. (K,( width A),( width A))))) by MATRIX_3: 4

      .= ((A * ( 0. (K,( width A),( width A)))) + (A * ( 0. (K,( width A),( width A))))) by A2, A3, A4, A6, MATRIX_4: 62;

      then ( len ( - (A * ( 0. (K,( width A),( width A)))))) = ( len (A * ( 0. (K,( width A),( width A))))) & ( 0. (K,( len A),( width A))) = ((B + B) + ( - B)) by A5, A7, MATRIX_3:def 2, MATRIX_4: 2;



      then ( 0. (K,( len A),( width A))) = (B + (B - B)) by A1, MATRIX_3: 3

      .= (A * ( 0. (K,( width A),( width A)))) by A5, A1, MATRIX_4: 20;

      hence thesis;

    end;

    theorem :: MATRIX_6:3



     Th3: M1 commutes_with ( 0. (K,n,n))

    proof

      per cases by NAT_1: 3;

        suppose

         A1: n > 0 ;



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

        then

         A3: (( 0. (K,n,n)) * M1) = ( 0. (K,n,n)) by Th1;

        (M1 * ( 0. (K,n,n))) = ( 0. (K,n,n)) by A1, A2, Th2;

        hence thesis by A3;

      end;

        suppose n = 0 ;

        then ( len M1) = 0 & ( len ( 0. (K,n,n))) = 0 by MATRIX_0:def 2;

        hence thesis by CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_6:4

    M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 implies M1 commutes_with (M2 * M3)

    proof



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



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



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



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



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

      assume that

       A6: M1 commutes_with M2 and

       A7: M2 commutes_with M3 and

       A8: M1 commutes_with M3;

      ((M2 * M3) * M1) = ((M3 * M2) * M1) by A7

      .= (M3 * (M2 * M1)) by A2, A3, A5, MATRIX_3: 33

      .= (M3 * (M1 * M2)) by A6

      .= ((M3 * M1) * M2) by A1, A3, A5, MATRIX_3: 33

      .= ((M1 * M3) * M2) by A8

      .= (M1 * (M3 * M2)) by A1, A5, A4, MATRIX_3: 33

      .= (M1 * (M2 * M3)) by A7;

      hence thesis;

    end;

    theorem :: MATRIX_6:5

    M1 commutes_with M2 & M1 commutes_with M3 & n > 0 implies M1 commutes_with (M2 + M3)

    proof



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



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



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

      assume that

       A4: M1 commutes_with M2 and

       A5: M1 commutes_with M3 and

       A6: n > 0 ;



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



      then ((M2 + M3) * M1) = ((M2 * M1) + (M3 * M1)) by A2, A3, A6, MATRIX_4: 63

      .= ((M1 * M2) + (M3 * M1)) by A4

      .= ((M1 * M2) + (M1 * M3)) by A5

      .= (M1 * (M2 + M3)) by A1, A7, A2, A3, A6, MATRIX_4: 62;

      hence thesis;

    end;

    theorem :: MATRIX_6:6



     Th6: M1 commutes_with ( 1. (K,n))

    proof

      M1 = (M1 * ( 1. (K,n))) & M1 = (( 1. (K,n)) * M1) by MATRIX_3: 18, MATRIX_3: 19;

      hence thesis;

    end;

    theorem :: MATRIX_6:7



     Th7: M2 is_reverse_of M3 & M1 is_reverse_of M3 implies M1 = M2

    proof



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



       A2: ( len M2) = n & ( len M3) = n by MATRIX_0: 24;

      assume that

       A3: M2 is_reverse_of M3 and

       A4: M1 is_reverse_of M3;

      M1 = (M1 * ( 1. (K,n))) by MATRIX_3: 19

      .= (M1 * (M3 * M2)) by A3

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

      .= (( 1. (K,n)) * M2) by A4

      .= M2 by MATRIX_3: 18;

      hence thesis;

    end;

    definition

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

      assume

       A1: M1 is invertible;

      :: MATRIX_6:def4

      func M1 ~ -> Matrix of n, K means

      : Def4: it is_reverse_of M1;

      existence by A1;

      uniqueness by Th7;

    end

    theorem :: MATRIX_6:8



     Th8: (( 1. (K,n)) ~ ) = ( 1. (K,n)) & ( 1. (K,n)) is invertible

    proof

      (( 1. (K,n)) * ( 1. (K,n))) = ( 1. (K,n)) by MATRIX_3: 18;

      then

       A1: ( 1. (K,n)) is_reverse_of ( 1. (K,n));

      then ( 1. (K,n)) is invertible;

      hence thesis by A1, Def4;

    end;

    registration

      let K be Field, n be Nat;

      cluster ( 1. (K,n)) -> invertible;

      coherence by Th8;

    end

    registration

      let K be Field, n be Nat;

      cluster invertible for Matrix of n, K;

      existence

      proof

        take ( 1. (K,n));

        thus thesis;

      end;

    end

    theorem :: MATRIX_6:9

    ((( 1. (K,n)) ~ ) ~ ) = ( 1. (K,n))

    proof

      (( 1. (K,n)) ~ ) = ( 1. (K,n)) by Th8;

      hence thesis;

    end;

    theorem :: MATRIX_6:10



     Th10: (( 1. (K,n)) @ ) = ( 1. (K,n))

    proof

      per cases by NAT_1: 3;

        suppose

         A1: n > 0 ;



         A2: ( len ( 1. (K,n))) = n by MATRIX_0: 24;



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



         A4: for i, j st [i, j] in ( Indices ( 1. (K,n))) holds (( 1. (K,n)) * (i,j)) = ((( 1. (K,n)) @ ) * (i,j))

        proof

          let i, j;

          assume

           A5: [i, j] in ( Indices ( 1. (K,n)));

          then i in ( Seg n) & j in ( Seg n) by A3, ZFMISC_1: 87;

          then

           A6: [j, i] in ( Indices ( 1. (K,n))) by A3, ZFMISC_1: 87;

          per cases ;

            suppose i = j;

            hence thesis by A5, MATRIX_0:def 6;

          end;

            suppose i <> j;

            then (( 1. (K,n)) * (i,j)) = ( 0. K) & (( 1. (K,n)) * (j,i)) = ( 0. K) by A5, A6, MATRIX_1:def 3;

            hence thesis by A6, MATRIX_0:def 6;

          end;

        end;



         A7: ( width ( 1. (K,n))) = n by MATRIX_0: 24;

        then ( len (( 1. (K,n)) @ )) = ( width ( 1. (K,n))) & ( width (( 1. (K,n)) @ )) = ( len ( 1. (K,n))) by A1, MATRIX_0: 54;

        hence thesis by A7, A2, A4, MATRIX_0: 21;

      end;

        suppose n = 0 ;

        hence thesis by MATRIX_0: 45;

      end;

    end;

    theorem :: MATRIX_6:11

    for K be Field, n be Nat holds ((( 1. (K,n)) @ ) ~ ) = ( 1. (K,n))

    proof

      let K, n;

      (( 1. (K,n)) @ ) = ( 1. (K,n)) by Th10;

      hence thesis by Th8;

    end;

    theorem :: MATRIX_6:12

    M3 is_reverse_of M1 & n > 0 implies (M1 @ ) is_reverse_of (M3 @ )

    proof



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

      assume that

       A2: M3 is_reverse_of M1 and

       A3: n > 0 ;

      ( len M1) = n & (M3 * M1) = (M1 * M3) by A2, MATRIX_0: 24;

      then

       A4: ((M1 * M3) @ ) = ((M1 @ ) * (M3 @ )) by A1, A3, MATRIX_3: 22;

      then

       A5: ((M1 @ ) * (M3 @ )) = ( 1. (K,n)) by Th10, A2;

      ( len M3) = n by MATRIX_0: 24;

      then ((M3 @ ) * (M1 @ )) = ((M1 @ ) * (M3 @ )) by A1, A3, A4, MATRIX_3: 22;

      hence thesis by A5;

    end;

    theorem :: MATRIX_6:13



     Th13: M is invertible implies (M @ ) is invertible & ((M @ ) ~ ) = ((M ~ ) @ )

    proof

      assume

       A1: M is invertible;

      set M1 = (M @ ), M2 = ((M ~ ) @ );

      per cases by NAT_1: 3;

        suppose

         A2: n > 0 ;



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

        ( len M) = n by MATRIX_0: 24;

        then

         A4: (((M ~ ) * M) @ ) = ((M @ ) * ((M ~ ) @ )) by A2, A3, MATRIX_3: 22;



         A5: (M ~ ) is_reverse_of M by A1, Def4;

        then

         A6: (M1 * M2) = ( 1. (K,n)) by A4, Th10;

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

        then ((M * (M ~ )) @ ) = (((M ~ ) @ ) * (M @ )) by A2, A3, MATRIX_3: 22;

        then (M1 * M2) = (M2 * M1) by A5, A4;

        then

         A7: M1 is_reverse_of M2 by A6;

        then M1 is invertible;

        hence thesis by A7, Def4;

      end;

        suppose n = 0 ;

        then

         B1: M = ( 1. (K,n)) by MATRIX_0: 45;

        then

         B2: M1 = ( 1. (K,n)) by Th10;

        then ((M @ ) ~ ) = ( 1. (K,n)) by Th8;

        hence thesis by B1, B2;

      end;

    end;

    registration

      let K, n;

      let M be invertible Matrix of n, K;

      cluster (M @ ) -> invertible;

      coherence by Th13;

    end

    theorem :: MATRIX_6:14

    for K be Field, n be Nat, M1,M2,M3,M4 be Matrix of n, K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds (M3 * M4) is_reverse_of (M2 * M1)

    proof

      let K, n, M1, M2, M3, M4;



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



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



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



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

      assume that

       A5: M3 is_reverse_of M1 and

       A6: M4 is_reverse_of M2;

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



      then

       A7: ((M2 * M1) * (M3 * M4)) = (((M2 * M1) * M3) * M4) by A3, A4, MATRIX_3: 33

      .= ((M2 * (M1 * M3)) * M4) by A1, A2, A3, MATRIX_3: 33

      .= ((M2 * ( 1. (K,n))) * M4) by A5

      .= (M2 * M4) by MATRIX_3: 19

      .= ( 1. (K,n)) by A6;



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



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

      ( width (M3 * M4)) = n by MATRIX_0: 24;



      then ((M3 * M4) * (M2 * M1)) = (((M3 * M4) * M2) * M1) by A2, A9, MATRIX_3: 33

      .= ((M3 * (M4 * M2)) * M1) by A9, A8, A4, MATRIX_3: 33

      .= ((M3 * ( 1. (K,n))) * M1) by A6

      .= (M3 * M1) by MATRIX_3: 19

      .= ( 1. (K,n)) by A5;

      hence thesis by A7;

    end;

    theorem :: MATRIX_6:15

    for K be Field, n be Nat, M1,M2 be Matrix of n, K st M2 is_reverse_of M1 holds M1 commutes_with M2;

    theorem :: MATRIX_6:16



     Th16: M is invertible implies (M ~ ) is invertible & ((M ~ ) ~ ) = M

    proof

      assume M is invertible;

      then

       A1: (M ~ ) is_reverse_of M by Def4;

      then (M ~ ) is invertible;

      hence thesis by A1, Def4;

    end;

    registration

      let K, n;

      let M be invertible Matrix of n, K;

      cluster (M ~ ) -> invertible;

      coherence by Th16;

    end

    theorem :: MATRIX_6:17

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

    proof

      assume that

       A1: n > 0 and

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

       A3: M1 is invertible;



       A4: (M1 ~ ) is_reverse_of M1 by A3, Def4;



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



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



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



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

      M2 = (( 1. (K,n)) * M2) by MATRIX_3: 18

      .= (((M1 ~ ) * M1) * M2) by A4

      .= ((M1 ~ ) * ( 0. (K,n,n))) by A2, A6, A5, A8, MATRIX_3: 33

      .= ( 0. (K,n,n)) by A1, A7, A8, Th2;

      hence thesis by Th3;

    end;

    theorem :: MATRIX_6:18

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

    proof

      assume that

       A1: M1 = (M1 * M2) and

       A2: M1 is invertible;



       A3: (M1 ~ ) is_reverse_of M1 by A2, Def4;



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



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

      M2 = (( 1. (K,n)) * M2) by MATRIX_3: 18

      .= (((M1 ~ ) * M1) * M2) by A3

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

      .= ( 1. (K,n)) by A3;

      hence thesis by Th6;

    end;

    theorem :: MATRIX_6:19

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

    proof

      assume that

       A1: M1 = (M2 * M1) and

       A2: M1 is invertible;



       A3: (M1 ~ ) is_reverse_of M1 by A2, Def4;



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



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

      M2 = (M2 * ( 1. (K,n))) by MATRIX_3: 19

      .= (M2 * (M1 * (M1 ~ ))) by A3

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

      .= ( 1. (K,n)) by A3;

      hence thesis by Th6;

    end;

    definition

      let n be Nat, K be Field;

      let M1 be Matrix of n, K;

      :: MATRIX_6:def5

      attr M1 is symmetric means (M1 @ ) = M1;

    end

    registration

      let n be Nat, K be Field;

      cluster ( 1. (K,n)) -> symmetric;

      coherence by Th10;

    end

    theorem :: MATRIX_6:20



     Th20: (((n,n) --> a) @ ) = ((n,n) --> a)

    proof

      ( len ((n,n) --> a)) = n by MATRIX_0: 24;

      then

       A1: ( len (((n,n) --> a) @ )) = ( len ((n,n) --> a)) by MATRIX_0: 24;



       A2: ( Indices ((n,n) --> a)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



       A3: for i, j st [i, j] in ( Indices (((n,n) --> a) @ )) holds ((((n,n) --> a) @ ) * (i,j)) = (((n,n) --> a) * (i,j))

      proof

        let i, j;

        assume [i, j] in ( Indices (((n,n) --> a) @ ));

        then

         A4: [i, j] in ( Indices ((n,n) --> a)) by MATRIX_0: 26;

        then i in ( Seg n) & j in ( Seg n) by A2, ZFMISC_1: 87;

        then [j, i] in ( Indices ((n,n) --> a)) by A2, ZFMISC_1: 87;

        then ((((n,n) --> a) @ ) * (i,j)) = (((n,n) --> a) * (j,i)) & (((n,n) --> a) * (j,i)) = a by MATRIX_0: 46, MATRIX_0:def 6;

        hence thesis by A4, MATRIX_0: 46;

      end;

      ( width ((n,n) --> a)) = n by MATRIX_0: 24;

      then ( width (((n,n) --> a) @ )) = ( width ((n,n) --> a)) by MATRIX_0: 24;

      hence thesis by A1, A3, MATRIX_0: 21;

    end;

    theorem :: MATRIX_6:21

    ((n,n) --> a) is symmetric by Th20;

    theorem :: MATRIX_6:22

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

    proof

      assume that

       A1: n > 0 and

       A2: M1 is symmetric & M2 is symmetric;



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



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



       A5: (M1 @ ) = M1 & (M2 @ ) = M2 by A2;

      thus M1 commutes_with M2 implies (M1 * M2) is symmetric by A1, A5, A3, A4, MATRIX_3: 22;

      assume

       A6: (M1 * M2) is symmetric;

      (M2 * M1) = ((M1 * M2) @ ) by A1, A5, A3, A4, MATRIX_3: 22

      .= (M1 * M2) by A6;

      hence thesis;

    end;

    theorem :: MATRIX_6:23



     Th23: ((M1 + M2) @ ) = ((M1 @ ) + (M2 @ ))

    proof

      for i, j st [i, j] in ( Indices ((M1 + M2) @ )) holds (((M1 + M2) @ ) * (i,j)) = (((M1 @ ) + (M2 @ )) * (i,j))

      proof

        let i, j;

        assume [i, j] in ( Indices ((M1 + M2) @ ));

        then

         A1: [i, j] in [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then

         A2: [i, j] in ( Indices (M1 @ )) by MATRIX_0: 24;

        i in ( Seg n) & j in ( Seg n) by A1, ZFMISC_1: 87;

        then

         A3: [j, i] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        then

         A4: [j, i] in ( Indices M1) by MATRIX_0: 24;



         A5: [j, i] in ( Indices M2) by A3, MATRIX_0: 24;

         [j, i] in ( Indices (M1 + M2)) by A3, MATRIX_0: 24;



        then (((M1 + M2) @ ) * (i,j)) = ((M1 + M2) * (j,i)) by MATRIX_0:def 6

        .= ((M1 * (j,i)) + (M2 * (j,i))) by A4, MATRIX_3:def 3

        .= (((M1 @ ) * (i,j)) + (M2 * (j,i))) by A4, MATRIX_0:def 6

        .= (((M1 @ ) * (i,j)) + ((M2 @ ) * (i,j))) by A5, MATRIX_0:def 6

        .= (((M1 @ ) + (M2 @ )) * (i,j)) by A2, MATRIX_3:def 3;

        hence thesis;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIX_6:24

    M1 is symmetric & M2 is symmetric implies (M1 + M2) is symmetric by Th23;

    theorem :: MATRIX_6:25

    M1 is upper_triangular Matrix of n, K & M1 is lower_triangular Matrix of n, K implies M1 is symmetric

    proof

      assume

       A1: M1 is upper_triangular Matrix of n, K & M1 is lower_triangular Matrix of n, K;



       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices M1) holds ((M1 @ ) * (i,j)) = (M1 * (i,j))

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices M1);

        then [i, j] in [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then i in ( Seg n) & j in ( Seg n) by ZFMISC_1: 87;

        then

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

        per cases ;

          suppose i = j;

          hence thesis by A4, MATRIX_0:def 6;

        end;

          suppose

           A5: i <> j;

          per cases by A5, XXREAL_0: 1;

            suppose i < j;

            then (M1 * (i,j)) = ( 0. K) & (M1 * (j,i)) = ( 0. K) by A1, A3, A4, MATRIX_1:def 9, MATRIX_1:def 8;

            hence thesis by A4, MATRIX_0:def 6;

          end;

            suppose i > j;

            then (M1 * (i,j)) = ( 0. K) & (M1 * (j,i)) = ( 0. K) by A1, A3, A4, MATRIX_1:def 8, MATRIX_1:def 9;

            hence thesis by A4, MATRIX_0:def 6;

          end;

        end;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIX_6:26



     Th26: for K be Field, n be Nat, M1 be Matrix of n, K holds (( - M1) @ ) = ( - (M1 @ ))

    proof

      let K, n, M1;

      for i, j st [i, j] in ( Indices (( - M1) @ )) holds ((( - M1) @ ) * (i,j)) = (( - (M1 @ )) * (i,j))

      proof

        let i, j;

        assume

         A1: [i, j] in ( Indices (( - M1) @ ));

        then

         A2: [i, j] in ( Indices (M1 @ )) by MATRIX_0: 26;

         [i, j] in [:( Seg n), ( Seg n):] by A1, MATRIX_0: 24;

        then i in ( Seg n) & j in ( Seg n) by ZFMISC_1: 87;

        then

         A3: [j, i] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        then

         A4: [j, i] in ( Indices M1) by MATRIX_0: 24;

         [j, i] in ( Indices ( - M1)) by A3, MATRIX_0: 24;



        then ((( - M1) @ ) * (i,j)) = (( - M1) * (j,i)) by MATRIX_0:def 6

        .= ( - (M1 * (j,i))) by A4, MATRIX_3:def 2

        .= ( - ((M1 @ ) * (i,j))) by A4, MATRIX_0:def 6

        .= (( - (M1 @ )) * (i,j)) by A2, MATRIX_3:def 2;

        hence thesis;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIX_6:27

    for K be Field, n be Nat, M1 be Matrix of n, K st M1 is symmetric holds ( - M1) is symmetric by Th26;

    theorem :: MATRIX_6:28

    for K be Field, n be Nat, M1,M2 be Matrix of n, K st M1 is symmetric & M2 is symmetric holds (M1 - M2) is symmetric

    proof

      let K, n, M1, M2;

      assume that

       A1: M1 is symmetric and

       A2: M2 is symmetric;

      ((M1 - M2) @ ) = ((M1 @ ) + (( - M2) @ )) by Th23

      .= (M1 + (( - M2) @ )) by A1

      .= (M1 + ( - (M2 @ ))) by Th26

      .= (M1 - M2) by A2;

      hence thesis;

    end;

    definition

      let n be Nat, K be Field;

      let M1 be Matrix of n, K;

      :: MATRIX_6:def6

      attr M1 is antisymmetric means (M1 @ ) = ( - M1);

    end

    theorem :: MATRIX_6:29

    for K be Fanoian Field, n be Nat, M1 be Matrix of n, K st M1 is symmetric antisymmetric holds M1 = ( 0. (K,n,n))

    proof

      let K be Fanoian Field;

      let n;

      let M1 be Matrix of n, K;

      assume M1 is symmetric antisymmetric;

      then

       A1: (M1 @ ) = M1 & (M1 @ ) = ( - M1);

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (( 0. (K,n,n)) * (i,j))

      proof

        let i, j;

        assume

         A2: [i, j] in ( Indices M1);

        then (M1 * (i,j)) = ( - (M1 * (i,j))) by A1, MATRIX_3:def 2;

        then ((M1 * (i,j)) + (M1 * (i,j))) = ( 0. K) by RLVECT_1: 5;

        then ((( 1_ K) * (M1 * (i,j))) + (( 1_ K) * (M1 * (i,j)))) = ( 0. K);

        then (( 1_ K) + ( 1_ K)) <> ( 0. K) & ((( 1_ K) + ( 1_ K)) * (M1 * (i,j))) = ( 0. K) by VECTSP_1:def 7, VECTSP_1:def 19;

        then

         A3: (M1 * (i,j)) = ( 0. K) by VECTSP_1: 12;

         [i, j] in ( Indices ( 0. (K,n,n))) by A2, MATRIX_0: 26;

        hence thesis by A3, MATRIX_3: 1;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIX_6:30

    for K be Fanoian Field, n,i be Nat, M1 be Matrix of n, K st M1 is antisymmetric & i in ( Seg n) holds (M1 * (i,i)) = ( 0. K)

    proof

      let K be Fanoian Field;

      let n, i;

      let M1 be Matrix of n, K;

      assume that

       A1: M1 is antisymmetric and

       A2: i in ( Seg n);



       A3: (M1 @ ) = ( - M1) by A1;

      ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      then

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

      then ((M1 @ ) * (i,i)) = (M1 * (i,i)) by MATRIX_0:def 6;

      then (M1 * (i,i)) = ( - (M1 * (i,i))) by A4, A3, MATRIX_3:def 2;

      then ((M1 * (i,i)) + (M1 * (i,i))) = ( 0. K) by RLVECT_1: 5;

      then ((( 1_ K) * (M1 * (i,i))) + (( 1_ K) * (M1 * (i,i)))) = ( 0. K);

      then (( 1_ K) + ( 1_ K)) <> ( 0. K) & ((( 1_ K) + ( 1_ K)) * (M1 * (i,i))) = ( 0. K) by VECTSP_1:def 7, VECTSP_1:def 19;

      hence thesis by VECTSP_1: 12;

    end;

    theorem :: MATRIX_6:31

    for K be Field, n be Nat, M1,M2 be Matrix of n, K st M1 is antisymmetric & M2 is antisymmetric holds (M1 + M2) is antisymmetric

    proof

      let K, n, M1, M2;

      assume that

       A1: M1 is antisymmetric and

       A2: M2 is antisymmetric;



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



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

      ((M1 + M2) @ ) = ((M1 @ ) + (M2 @ )) by Th23

      .= (( - M1) + (M2 @ )) by A1

      .= (( - M1) + ( - M2)) by A2

      .= ( - (M1 + M2)) by A3, A4, MATRIX_4: 12;

      hence thesis;

    end;

    theorem :: MATRIX_6:32

    for K be Field, n be Nat, M1 be Matrix of n, K st M1 is antisymmetric holds ( - M1) is antisymmetric by Th26;

    theorem :: MATRIX_6:33

    for K be Field, n be Nat, M1,M2 be Matrix of n, K st M1 is antisymmetric & M2 is antisymmetric holds (M1 - M2) is antisymmetric

    proof

      let K, n, M1, M2;

      assume that

       A1: M1 is antisymmetric and

       A2: M2 is antisymmetric;



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



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

      ((M1 - M2) @ ) = ((M1 @ ) + (( - M2) @ )) by Th23

      .= (( - M1) + (( - M2) @ )) by A1

      .= (( - M1) + ( - (M2 @ ))) by Th26

      .= (( - M1) + ( - ( - M2))) by A2

      .= ( - (M1 - M2)) by A3, A4, MATRIX_4: 12;

      hence thesis;

    end;

    theorem :: MATRIX_6:34

    n > 0 implies (M1 - (M1 @ )) is antisymmetric

    proof

      assume

       A1: n > 0 ;

      set M2 = (M1 - (M1 @ ));



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



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

      (M2 @ ) = ((M1 @ ) + (( - (M1 @ )) @ )) by Th23

      .= ((M1 @ ) + ( - ((M1 @ ) @ ))) by Th26

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

      .= ( - (M1 - (M1 @ ))) by A2, A3, MATRIX_4: 43;

      hence thesis;

    end;

    theorem :: MATRIX_6:35

    n > 0 implies (M1 commutes_with M2 iff ((M1 + M2) * (M1 + M2)) = ((((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2)))

    proof

      assume

       A1: n > 0 ;



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



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



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



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



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

      thus M1 commutes_with M2 implies ((M1 + M2) * (M1 + M2)) = ((((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2))

      proof

        assume

         A10: M1 commutes_with M2;

        ((M1 + M2) * (M1 + M2)) = (((M1 + M2) * M1) + ((M1 + M2) * M2)) by A1, A6, A8, A9, MATRIX_4: 62

        .= (((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2)) by A1, A6, A8, MATRIX_4: 63

        .= (((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2))) by A1, A6, A8, MATRIX_4: 63

        .= ((((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2)) by A2, A7, MATRIX_3: 3;

        hence thesis by A10;

      end;

      assume

       A11: ((M1 + M2) * (M1 + M2)) = ((((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2));



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

      ((M1 + M2) * (M1 + M2)) = (((M1 + M2) * M1) + ((M1 + M2) * M2)) by A1, A6, A8, A9, MATRIX_4: 62

      .= (((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2)) by A1, A6, A8, MATRIX_4: 63

      .= (((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2))) by A1, A6, A8, MATRIX_4: 63

      .= ((((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2)) by A2, A7, MATRIX_3: 3;

      then (((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2))) = ((((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2)) by A2, A7, A11, MATRIX_3: 3;

      then (((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2))) = (((M1 * M1) + (M1 * M2)) + ((M1 * M2) + (M2 * M2))) by A2, A3, MATRIX_3: 3;

      then ((M1 * M1) + (M2 * M1)) = ((M1 * M1) + (M1 * M2)) by A7, A4, A3, MATRIX_4: 4;

      then ((M2 * M1) + (M1 * M1)) = ((M1 * M1) + (M1 * M2)) by A5, A12, MATRIX_3: 2;

      then ((M2 * M1) + (M1 * M1)) = ((M1 * M2) + (M1 * M1)) by A5, A2, MATRIX_3: 2;

      hence thesis by A5, A2, A12, MATRIX_4: 4;

    end;

    theorem :: MATRIX_6:36



     Th36: M1 is invertible & M2 is invertible implies (M1 * M2) is invertible & ((M1 * M2) ~ ) = ((M2 ~ ) * (M1 ~ ))

    proof

      assume that

       A1: M1 is invertible and

       A2: M2 is invertible;



       A3: (M2 ~ ) is_reverse_of M2 by A2, Def4;



       A4: (M1 ~ ) is_reverse_of M1 by A1, Def4;



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



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



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



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



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



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

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



      then

       A11: ((M1 * M2) * ((M2 ~ ) * (M1 ~ ))) = (((M1 * M2) * (M2 ~ )) * (M1 ~ )) by A5, A10, MATRIX_3: 33

      .= ((M1 * (M2 * (M2 ~ ))) * (M1 ~ )) by A9, A8, A5, MATRIX_3: 33

      .= ((M1 * ( 1. (K,n))) * (M1 ~ )) by A3

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

      .= ( 1. (K,n)) by A4;

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



      then (((M2 ~ ) * (M1 ~ )) * (M1 * M2)) = ((((M2 ~ ) * (M1 ~ )) * M1) * M2) by A9, A7, MATRIX_3: 33

      .= (((M2 ~ ) * ((M1 ~ ) * M1)) * M2) by A7, A6, A10, MATRIX_3: 33

      .= (((M2 ~ ) * ( 1. (K,n))) * M2) by A4

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

      .= ( 1. (K,n)) by A3;

      then

       A12: ((M2 ~ ) * (M1 ~ )) is_reverse_of (M1 * M2) by A11;

      then (M1 * M2) is invertible;

      hence thesis by A12, Def4;

    end;

    theorem :: MATRIX_6:37

    M1 is invertible & M2 is invertible & M1 commutes_with M2 implies (M1 * M2) is invertible & ((M1 * M2) ~ ) = ((M1 ~ ) * (M2 ~ ))

    proof

      assume that

       A1: M1 is invertible and

       A2: M2 is invertible and

       A3: M1 commutes_with M2;



       A4: (M2 ~ ) is_reverse_of M2 by A2, Def4;



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



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



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



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



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



       A10: (M1 ~ ) is_reverse_of M1 by A1, Def4;



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



       A12: ( len (M1 ~ )) = n by MATRIX_0: 24;

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



      then

       A13: ((M1 * M2) * ((M1 ~ ) * (M2 ~ ))) = (((M1 * M2) * (M1 ~ )) * (M2 ~ )) by A11, A12, MATRIX_3: 33

      .= (((M2 * M1) * (M1 ~ )) * (M2 ~ )) by A3

      .= ((M2 * (M1 * (M1 ~ ))) * (M2 ~ )) by A8, A9, A12, MATRIX_3: 33

      .= ((M2 * ( 1. (K,n))) * (M2 ~ )) by A10

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

      .= ( 1. (K,n)) by A4;

      (((M1 ~ ) * (M2 ~ )) * (M1 * M2)) = (((M1 ~ ) * (M2 ~ )) * (M2 * M1)) by A3

      .= ((((M1 ~ ) * (M2 ~ )) * M2) * M1) by A7, A9, A5, MATRIX_3: 33

      .= (((M1 ~ ) * ((M2 ~ ) * M2)) * M1) by A7, A11, A6, MATRIX_3: 33

      .= (((M1 ~ ) * ( 1. (K,n))) * M1) by A4

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

      .= ( 1. (K,n)) by A10;

      then

       A14: ((M1 ~ ) * (M2 ~ )) is_reverse_of (M1 * M2) by A13;

      then (M1 * M2) is invertible;

      hence thesis by A14, Def4;

    end;

    theorem :: MATRIX_6:38

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

    proof



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



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

      assume that

       A3: M1 is invertible and

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



       A5: (M1 ~ ) is_reverse_of M1 by A3, Def4;

      ((M1 ~ ) * (M1 * M2)) = (M1 ~ ) by A4, MATRIX_3: 19;

      then (((M1 ~ ) * M1) * M2) = (M1 ~ ) by A1, A2, MATRIX_3: 33;

      then (( 1. (K,n)) * M2) = (M1 ~ ) by A5;

      then M2 = (M1 ~ ) by MATRIX_3: 18;

      hence thesis by A3, Def4;

    end;

    theorem :: MATRIX_6:39

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

    proof



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



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

      assume that

       A3: M2 is invertible and

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



       A5: (M2 ~ ) is_reverse_of M2 by A3, Def4;

      ((M2 ~ ) * (M2 * M1)) = (M2 ~ ) by A4, MATRIX_3: 19;

      then (((M2 ~ ) * M2) * M1) = (M2 ~ ) by A1, A2, MATRIX_3: 33;

      then (( 1. (K,n)) * M1) = (M2 ~ ) by A5;

      then M1 = (M2 ~ ) by MATRIX_3: 18;

      hence thesis by A3, Def4;

    end;

    theorem :: MATRIX_6:40



     Th40: M1 is invertible & M1 commutes_with M2 implies (M1 ~ ) commutes_with M2

    proof

      assume that

       A1: M1 is invertible and

       A2: M1 commutes_with M2;



       A3: (M1 ~ ) is_reverse_of M1 by A1, Def4;



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



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



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



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



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



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

      M2 = (( 1. (K,n)) * M2) by MATRIX_3: 18

      .= (((M1 ~ ) * M1) * M2) by A3

      .= ((M1 ~ ) * (M1 * M2)) by A5, A8, A9, MATRIX_3: 33

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



      then (M2 * (M1 ~ )) = ((M1 ~ ) * ((M2 * M1) * (M1 ~ ))) by A9, A7, A6, MATRIX_3: 33

      .= ((M1 ~ ) * (M2 * (M1 * (M1 ~ )))) by A5, A4, A7, MATRIX_3: 33

      .= ((M1 ~ ) * (M2 * ( 1. (K,n)))) by A3

      .= ((M1 ~ ) * M2) by MATRIX_3: 19;

      hence thesis;

    end;

    definition

      let n be Nat, K be Field;

      let M1 be Matrix of n, K;

      :: MATRIX_6:def7

      attr M1 is Orthogonal means M1 is invertible & (M1 @ ) = (M1 ~ );

    end

    theorem :: MATRIX_6:41



     Th41: (M1 * (M1 @ )) = ( 1. (K,n)) & M1 is invertible iff M1 is Orthogonal

    proof



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



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



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



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

      thus (M1 * (M1 @ )) = ( 1. (K,n)) & M1 is invertible implies M1 is Orthogonal

      proof

        assume that

         A5: (M1 * (M1 @ )) = ( 1. (K,n)) and

         A6: M1 is invertible;



         A7: (M1 ~ ) is_reverse_of M1 by A6, Def4;

        then ((M1 ~ ) * (M1 * (M1 ~ ))) = ((M1 ~ ) * (M1 * (M1 @ ))) by A5;

        then (((M1 ~ ) * M1) * (M1 ~ )) = ((M1 ~ ) * (M1 * (M1 @ ))) by A1, A3, A4, MATRIX_3: 33;

        then (((M1 ~ ) * M1) * (M1 ~ )) = (((M1 ~ ) * M1) * (M1 @ )) by A1, A3, A2, MATRIX_3: 33;

        then (( 1. (K,n)) * (M1 ~ )) = (((M1 ~ ) * M1) * (M1 @ )) by A7;

        then (( 1. (K,n)) * (M1 ~ )) = (( 1. (K,n)) * (M1 @ )) by A7;

        then (M1 ~ ) = (( 1. (K,n)) * (M1 @ )) by MATRIX_3: 18;

        then (M1 ~ ) = (M1 @ ) by MATRIX_3: 18;

        hence thesis by A6;

      end;

      assume

       A8: M1 is Orthogonal;

      then

       A9: (M1 ~ ) is_reverse_of M1 by Def4;

      (M1 * (M1 @ )) = (M1 * (M1 ~ )) by A8;

      hence thesis by A9;

    end;

    theorem :: MATRIX_6:42



     Th42: M1 is invertible & ((M1 @ ) * M1) = ( 1. (K,n)) iff M1 is Orthogonal

    proof



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



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



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



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

      thus M1 is invertible & ((M1 @ ) * M1) = ( 1. (K,n)) implies M1 is Orthogonal

      proof

        assume that

         A5: M1 is invertible and

         A6: ((M1 @ ) * M1) = ( 1. (K,n));



         A7: (M1 ~ ) is_reverse_of M1 by A5, Def4;

        then (((M1 ~ ) * M1) * (M1 ~ )) = (((M1 @ ) * M1) * (M1 ~ )) by A6;

        then ((M1 ~ ) * (M1 * (M1 ~ ))) = (((M1 @ ) * M1) * (M1 ~ )) by A1, A4, A3, MATRIX_3: 33;

        then ((M1 ~ ) * (M1 * (M1 ~ ))) = ((M1 @ ) * (M1 * (M1 ~ ))) by A1, A3, A2, MATRIX_3: 33;

        then ((M1 ~ ) * ( 1. (K,n))) = ((M1 @ ) * (M1 * (M1 ~ ))) by A7;

        then ((M1 ~ ) * ( 1. (K,n))) = ((M1 @ ) * ( 1. (K,n))) by A7;

        then (M1 ~ ) = ((M1 @ ) * ( 1. (K,n))) by MATRIX_3: 19;

        then (M1 ~ ) = (M1 @ ) by MATRIX_3: 19;

        hence thesis by A5;

      end;

      assume

       A8: M1 is Orthogonal;

      then

       A9: (M1 ~ ) is_reverse_of M1 by Def4;

      ((M1 @ ) * M1) = ((M1 ~ ) * M1) by A8;

      hence thesis by A9;

    end;

    theorem :: MATRIX_6:43

    M1 is Orthogonal implies ((M1 @ ) * M1) = (M1 * (M1 @ ))

    proof

      assume

       A1: M1 is Orthogonal;

      then ((M1 @ ) * M1) = ( 1. (K,n)) by Th42;

      hence thesis by A1, Th41;

    end;

    theorem :: MATRIX_6:44

    M1 is Orthogonal & M1 commutes_with M2 implies (M1 @ ) commutes_with M2 by Th40;

    theorem :: MATRIX_6:45



     Th45: M1 is invertible & M2 is invertible implies (M1 * M2) is invertible & ((M1 * M2) ~ ) = ((M2 ~ ) * (M1 ~ ))

    proof

      assume that

       A1: M1 is invertible and

       A2: M2 is invertible;



       A3: (M1 ~ ) is_reverse_of M1 by A1, Def4;



       A4: (M2 ~ ) is_reverse_of M2 by A2, Def4;



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



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



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



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



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



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

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



      then

       A11: (((M2 ~ ) * (M1 ~ )) * (M1 * M2)) = ((((M2 ~ ) * (M1 ~ )) * M1) * M2) by A7, A5, MATRIX_3: 33

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

      .= (((M2 ~ ) * ( 1. (K,n))) * M2) by A3

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

      .= ( 1. (K,n)) by A4;

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



      then ((M1 * M2) * ((M2 ~ ) * (M1 ~ ))) = (((M1 * M2) * (M2 ~ )) * (M1 ~ )) by A9, A10, MATRIX_3: 33

      .= ((M1 * (M2 * (M2 ~ ))) * (M1 ~ )) by A7, A8, A9, MATRIX_3: 33

      .= ((M1 * ( 1. (K,n))) * (M1 ~ )) by A4

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

      .= ( 1. (K,n)) by A3;

      then

       A12: ((M2 ~ ) * (M1 ~ )) is_reverse_of (M1 * M2) by A11;

      then (M1 * M2) is invertible;

      hence thesis by A12, Def4;

    end;

    theorem :: MATRIX_6:46

    n > 0 & M1 is Orthogonal & M2 is Orthogonal implies (M1 * M2) is Orthogonal

    proof

      assume that

       A1: n > 0 and

       A2: M1 is Orthogonal & M2 is Orthogonal;

      M1 is invertible & M2 is invertible by A2;

      then

       A3: (M1 * M2) is invertible & ((M1 * M2) ~ ) = ((M2 ~ ) * (M1 ~ )) by Th45;



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



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

      (M1 @ ) = (M1 ~ ) & (M2 @ ) = (M2 ~ ) by A2;

      then ((M1 * M2) @ ) = ((M2 ~ ) * (M1 ~ )) by A1, A5, A4, MATRIX_3: 22;

      hence thesis by A3;

    end;

    theorem :: MATRIX_6:47

    M1 is Orthogonal & M1 commutes_with M2 implies (M1 @ ) commutes_with M2

    proof

      set M3 = (M1 @ );

      assume that

       A1: M1 is Orthogonal and

       A2: M1 commutes_with M2;

      M1 is invertible by A1;

      then

       A3: (M1 ~ ) is_reverse_of M1 by Def4;



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



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



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



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



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

      (M2 * M3) = ((( 1. (K,n)) * M2) * (M1 @ )) by MATRIX_3: 18

      .= ((((M1 ~ ) * M1) * M2) * (M1 @ )) by A3

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

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

      .= (((M1 ~ ) * (M2 * M1)) * (M1 ~ )) by A1

      .= ((((M1 ~ ) * M2) * M1) * (M1 ~ )) by A4, A8, A6, MATRIX_3: 33

      .= (((M1 ~ ) * M2) * (M1 * (M1 ~ ))) by A5, A8, A7, MATRIX_3: 33

      .= (((M1 ~ ) * M2) * ( 1. (K,n))) by A3

      .= ((M1 ~ ) * M2) by MATRIX_3: 19

      .= (M3 * M2) by A1;

      hence thesis;

    end;

    theorem :: MATRIX_6:48

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

    proof

      assume that

       A1: n > 0 and

       A2: M1 commutes_with M2;



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



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



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



      then ((M1 + M1) * M2) = ((M1 * M2) + (M1 * M2)) by A1, A4, MATRIX_4: 63

      .= ((M2 * M1) + (M1 * M2)) by A2

      .= ((M2 * M1) + (M2 * M1)) by A2

      .= (M2 * (M1 + M1)) by A1, A5, A3, A4, MATRIX_4: 62;

      hence thesis;

    end;

    theorem :: MATRIX_6:49

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

    proof

      assume that

       A1: n > 0 and

       A2: M1 commutes_with M2;



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



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



      then ((M1 + M2) * M2) = ((M1 * M2) + (M2 * M2)) by A1, A3, MATRIX_4: 63

      .= ((M2 * M1) + (M2 * M2)) by A2

      .= (M2 * (M1 + M2)) by A1, A4, A3, MATRIX_4: 62;

      hence thesis;

    end;

    theorem :: MATRIX_6:50

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

    proof

      assume that

       A1: n > 0 and

       A2: M1 commutes_with M2;



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



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



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



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

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



      then ((M1 + M1) * (M2 + M2)) = (((M1 + M1) * M2) + ((M1 + M1) * M2)) by A1, A3, A5, A4, MATRIX_4: 62

      .= (((M1 * M2) + (M1 * M2)) + ((M1 + M1) * M2)) by A1, A3, A6, MATRIX_4: 63

      .= (((M1 * M2) + (M1 * M2)) + ((M1 * M2) + (M1 * M2))) by A1, A3, A6, MATRIX_4: 63

      .= (((M2 * M1) + (M1 * M2)) + ((M1 * M2) + (M1 * M2))) by A2

      .= (((M2 * M1) + (M2 * M1)) + ((M1 * M2) + (M1 * M2))) by A2

      .= (((M2 * M1) + (M2 * M1)) + ((M2 * M1) + (M2 * M1))) by A2

      .= ((M2 * (M1 + M1)) + ((M2 * M1) + (M2 * M1))) by A1, A3, A5, A6, MATRIX_4: 62

      .= ((M2 * (M1 + M1)) + (M2 * (M1 + M1))) by A1, A3, A5, A6, MATRIX_4: 62

      .= ((M2 + M2) * (M1 + M1)) by A1, A3, A5, A4, MATRIX_4: 63;

      hence thesis;

    end;

    theorem :: MATRIX_6:51

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

    proof

      assume that

       A1: n > 0 and

       A2: M1 commutes_with M2;



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



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



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

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



      then ((M1 + M2) * (M2 + M2)) = (((M1 + M2) * M2) + ((M1 + M2) * M2)) by A1, A3, A4, MATRIX_4: 62

      .= (((M1 * M2) + (M2 * M2)) + ((M1 + M2) * M2)) by A1, A3, A5, MATRIX_4: 63

      .= (((M1 * M2) + (M2 * M2)) + ((M1 * M2) + (M2 * M2))) by A1, A3, A5, MATRIX_4: 63

      .= (((M2 * M1) + (M2 * M2)) + ((M1 * M2) + (M2 * M2))) by A2

      .= (((M2 * M1) + (M2 * M2)) + ((M2 * M1) + (M2 * M2))) by A2

      .= ((M2 * (M1 + M2)) + ((M2 * M1) + (M2 * M2))) by A1, A3, A5, MATRIX_4: 62

      .= ((M2 * (M1 + M2)) + (M2 * (M1 + M2))) by A1, A3, A5, MATRIX_4: 62

      .= ((M2 + M2) * (M1 + M2)) by A1, A3, A4, MATRIX_4: 63;

      hence thesis;

    end;

    theorem :: MATRIX_6:52

    M1 commutes_with M2 implies (M1 * M2) commutes_with M2

    proof



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



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

      assume M1 commutes_with M2;

      then ((M1 * M2) * M2) = (M2 * (M1 * M2)) by A1, A2, MATRIX_3: 33;

      hence thesis;

    end;

    theorem :: MATRIX_6:53

    M1 commutes_with M2 implies (M1 * M1) commutes_with M2

    proof



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



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

      assume

       A3: M1 commutes_with M2;



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



      then ((M1 * M1) * M2) = (M1 * (M1 * M2)) by A2, MATRIX_3: 33

      .= (M1 * (M2 * M1)) by A3

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

      .= ((M2 * M1) * M1) by A3

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

      hence thesis;

    end;

    theorem :: MATRIX_6:54

    M1 commutes_with M2 implies (M1 * M1) commutes_with (M2 * M2)

    proof



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



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



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

      assume

       A4: M1 commutes_with M2;



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



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



      then ((M1 * M1) * (M2 * M2)) = (((M1 * M1) * M2) * M2) by A1, A5, MATRIX_3: 33

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

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

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

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

      .= ((M2 * (M1 * M1)) * M2) by A1, A3, MATRIX_3: 33

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

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

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

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

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

      .= (M2 * (M2 * (M1 * M1))) by A1, A3, MATRIX_3: 33

      .= ((M2 * M2) * (M1 * M1)) by A1, A5, A2, MATRIX_3: 33;

      hence thesis;

    end;

    theorem :: MATRIX_6:55

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

    proof



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

      set M3 = (M1 @ ), M4 = (M2 @ );



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

      assume that

       A3: n > 0 and

       A4: M1 commutes_with M2;

      ( len M1) = n by MATRIX_0: 24;



      then (M3 * M4) = ((M2 * M1) @ ) by A1, A3, MATRIX_3: 22

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

      .= (M4 * M3) by A1, A2, A3, MATRIX_3: 22;

      hence thesis;

    end;

    theorem :: MATRIX_6:56



     Th56: M1 is invertible & M2 is invertible & M3 is invertible implies ((M1 * M2) * M3) is invertible & (((M1 * M2) * M3) ~ ) = (((M3 ~ ) * (M2 ~ )) * (M1 ~ ))

    proof

      assume that

       A1: M1 is invertible and

       A2: M2 is invertible and

       A3: M3 is invertible;



       A4: (M1 ~ ) is_reverse_of M1 by A1, Def4;



       A5: (M2 ~ ) is_reverse_of M2 by A2, Def4;



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



       A7: (M3 ~ ) is_reverse_of M3 by A3, Def4;



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



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



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



       A11: ( len (M1 ~ )) = n by MATRIX_0: 24;

      set M5 = (((M3 ~ ) * (M2 ~ )) * (M1 ~ ));

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



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



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



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



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



       A16: ( len (M3 ~ )) = n by MATRIX_0: 24;



       A17: ( width ((M3 ~ ) * (M2 ~ ))) = n by MATRIX_0: 24;



       A18: ( width (M3 ~ )) = n by MATRIX_0: 24;



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



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



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



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



      then

       A23: (M5 * M4) = ((((M3 ~ ) * (M2 ~ )) * (M1 ~ )) * (M1 * (M2 * M3))) by A12, A14, A6, MATRIX_3: 33

      .= (((((M3 ~ ) * (M2 ~ )) * (M1 ~ )) * M1) * (M2 * M3)) by A22, A20, A13, MATRIX_3: 33

      .= ((((M3 ~ ) * (M2 ~ )) * ((M1 ~ ) * M1)) * (M2 * M3)) by A20, A19, A11, A17, MATRIX_3: 33

      .= ((((M3 ~ ) * (M2 ~ )) * ( 1. (K,n))) * (M2 * M3)) by A4

      .= (((M3 ~ ) * (M2 ~ )) * (M2 * M3)) by MATRIX_3: 19

      .= ((((M3 ~ ) * (M2 ~ )) * M2) * M3) by A12, A14, A6, A17, MATRIX_3: 33

      .= (((M3 ~ ) * ((M2 ~ ) * M2)) * M3) by A14, A8, A18, A21, MATRIX_3: 33

      .= (((M3 ~ ) * ( 1. (K,n))) * M3) by A5

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

      .= ( 1. (K,n)) by A7;

      (M4 * M5) = (((M1 * M2) * M3) * ((M3 ~ ) * ((M2 ~ ) * (M1 ~ )))) by A8, A18, A11, A21, MATRIX_3: 33

      .= ((((M1 * M2) * M3) * (M3 ~ )) * ((M2 ~ ) * (M1 ~ ))) by A18, A16, A15, MATRIX_3: 33

      .= (((M1 * M2) * (M3 * (M3 ~ ))) * ((M2 ~ ) * (M1 ~ ))) by A9, A6, A10, A16, MATRIX_3: 33

      .= (((M1 * M2) * ( 1. (K,n))) * ((M2 ~ ) * (M1 ~ ))) by A7

      .= ((M1 * M2) * ((M2 ~ ) * (M1 ~ ))) by MATRIX_3: 19

      .= (((M1 * M2) * (M2 ~ )) * (M1 ~ )) by A10, A8, A11, A21, MATRIX_3: 33

      .= ((M1 * (M2 * (M2 ~ ))) * (M1 ~ )) by A22, A12, A14, A21, MATRIX_3: 33

      .= ((M1 * ( 1. (K,n))) * (M1 ~ )) by A5

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

      .= ( 1. (K,n)) by A4;

      then

       A24: M5 is_reverse_of M4 by A23;

      then M4 is invertible;

      hence thesis by A24, Def4;

    end;

    theorem :: MATRIX_6:57

    n > 0 & M1 is Orthogonal & M2 is Orthogonal & M3 is Orthogonal implies ((M1 * M2) * M3) is Orthogonal

    proof

      assume that

       A1: n > 0 and

       A2: M1 is Orthogonal & M2 is Orthogonal and

       A3: M3 is Orthogonal;



       A4: M3 is invertible by A3;

      set M5 = (((M3 ~ ) * (M2 ~ )) * (M1 ~ ));

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



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

      M1 is invertible & M2 is invertible by A2;

      then

       A6: (M4 ~ ) = M5 & M4 is invertible by A4, Th56;



       A7: ( width M2) = n & (M3 @ ) = (M3 ~ ) by A3, MATRIX_0: 24;



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



       A9: (M1 @ ) = (M1 ~ ) & (M2 @ ) = (M2 ~ ) by A2;



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



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

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



      then (((M1 * M2) * M3) @ ) = ((M3 @ ) * ((M1 * M2) @ )) by A1, A10, MATRIX_3: 22

      .= ((M3 ~ ) * ((M2 ~ ) * (M1 ~ ))) by A1, A5, A9, A7, MATRIX_3: 22

      .= M5 by A8, A11, MATRIX_3: 33;

      hence thesis by A6;

    end;

    theorem :: MATRIX_6:58

    ( 1. (K,n)) is Orthogonal

    proof



       A1: (( 1. (K,n)) @ ) = ( 1. (K,n)) by Th10;

      (( 1. (K,n)) ~ ) = ( 1. (K,n)) & ( 1. (K,n)) is invertible by Th8;

      hence thesis by A1;

    end;

    theorem :: MATRIX_6:59

    n > 0 & M1 is Orthogonal & M2 is Orthogonal implies ((M1 ~ ) * M2) is Orthogonal

    proof

      assume that

       A1: n > 0 and

       A2: M1 is Orthogonal and

       A3: M2 is Orthogonal;



       A4: M1 is invertible by A2;

      then

       A5: (M1 ~ ) is invertible;



       A6: M2 is invertible by A3;

      then

       A7: ((M1 ~ ) * M2) is invertible by A5, Th36;

      (((M1 ~ ) * M2) ~ ) = ((M2 ~ ) * ((M1 ~ ) ~ )) by A6, A5, Th36;

      then

       A8: (((M1 ~ ) * M2) ~ ) = ((M2 ~ ) * M1) by A4, Th16;



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



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



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

      (M1 @ ) = (M1 ~ ) & (M2 @ ) = (M2 ~ ) by A2, A3;



      then (((M1 ~ ) * M2) @ ) = ((M2 ~ ) * ((M1 @ ) @ )) by A1, A10, A9, MATRIX_3: 22

      .= ((M2 ~ ) * M1) by A1, A11, MATRIX_0: 57;

      hence thesis by A7, A8;

    end;