matrix_5.miz



    begin

    theorem :: MATRIX_5:1

    1 = ( 1_ F_Complex ) by COMPLEX1:def 4, COMPLFLD: 8;

    theorem :: MATRIX_5:2

    ( 0. F_Complex ) = 0 by COMPLFLD: 7;

    definition

      let A be Matrix of COMPLEX ;

      :: MATRIX_5:def1

      func COMPLEX2Field A -> Matrix of F_Complex equals A;

      coherence by COMPLFLD:def 1;

    end

    definition

      let A be Matrix of F_Complex ;

      :: MATRIX_5:def2

      func Field2COMPLEX A -> Matrix of COMPLEX equals A;

      coherence by COMPLFLD:def 1;

    end

    theorem :: MATRIX_5:3

    for A,B be Matrix of COMPLEX st ( COMPLEX2Field A) = ( COMPLEX2Field B) holds A = B;

    theorem :: MATRIX_5:4

    for A,B be Matrix of F_Complex st ( Field2COMPLEX A) = ( Field2COMPLEX B) holds A = B;

    theorem :: MATRIX_5:5

    for A be Matrix of COMPLEX holds A = ( Field2COMPLEX ( COMPLEX2Field A));

    theorem :: MATRIX_5:6

    for A be Matrix of F_Complex holds A = ( COMPLEX2Field ( Field2COMPLEX A));

    definition

      let A,B be Matrix of COMPLEX ;

      :: MATRIX_5:def3

      func A + B -> Matrix of COMPLEX equals ( Field2COMPLEX (( COMPLEX2Field A) + ( COMPLEX2Field B)));

      coherence ;

    end

    definition

      let A be Matrix of COMPLEX ;

      :: MATRIX_5:def4

      func - A -> Matrix of COMPLEX equals ( Field2COMPLEX ( - ( COMPLEX2Field A)));

      coherence ;

    end

    definition

      let A,B be Matrix of COMPLEX ;

      :: MATRIX_5:def5

      func A - B -> Matrix of COMPLEX equals ( Field2COMPLEX (( COMPLEX2Field A) - ( COMPLEX2Field B)));

      coherence ;

      :: MATRIX_5:def6

      func A * B -> Matrix of COMPLEX equals ( Field2COMPLEX (( COMPLEX2Field A) * ( COMPLEX2Field B)));

      coherence ;

    end

    definition

      let x be Complex, A be Matrix of COMPLEX ;

      :: MATRIX_5:def7

      func x * A -> Matrix of COMPLEX means

      : Def7: for ea be Element of F_Complex st ea = x holds it = ( Field2COMPLEX (ea * ( COMPLEX2Field A)));

      existence

      proof

        x in COMPLEX by XCMPLX_0:def 2;

        then

        reconsider aa = x as Element of F_Complex by COMPLFLD:def 1;

        set C = ( Field2COMPLEX (aa * ( COMPLEX2Field A)));

        for ea be Element of F_Complex st ea = x holds C = ( Field2COMPLEX (ea * ( COMPLEX2Field A)));

        hence thesis;

      end;

      uniqueness

      proof

        x in COMPLEX by XCMPLX_0:def 2;

        then

        reconsider aa = x as Element of F_Complex by COMPLFLD:def 1;

        let C1,C2 be Matrix of COMPLEX ;

        assume that

         A1: for ea be Element of F_Complex st ea = x holds C1 = ( Field2COMPLEX (ea * ( COMPLEX2Field A))) and

         A2: for ea be Element of F_Complex st ea = x holds C2 = ( Field2COMPLEX (ea * ( COMPLEX2Field A)));

        C2 = ( Field2COMPLEX (aa * ( COMPLEX2Field A))) by A2;

        hence thesis by A1;

      end;

    end

    theorem :: MATRIX_5:7

    for A be Matrix of COMPLEX holds ( len A) = ( len ( COMPLEX2Field A)) & ( width A) = ( width ( COMPLEX2Field A));

    theorem :: MATRIX_5:8

    for A be Matrix of F_Complex holds ( len A) = ( len ( Field2COMPLEX A)) & ( width A) = ( width ( Field2COMPLEX A));

    theorem :: MATRIX_5:9

    

     Th9: for K be Field, M be Matrix of K holds (( 1_ K) * M) = M

    proof

      let K be Field, M be Matrix of K;

      

       A1: for i,j be Nat st [i, j] in ( Indices M) holds ((( 1_ K) * M) * (i,j)) = (M * (i,j))

      proof

        let i,j be Nat;

        

         A2: (( 1_ K) * (M * (i,j))) = (M * (i,j));

        assume [i, j] in ( Indices M);

        hence thesis by A2, MATRIX_3:def 5;

      end;

      ( len (( 1_ K) * M)) = ( len M) & ( width (( 1_ K) * M)) = ( width M) by MATRIX_3:def 5;

      hence thesis by A1, MATRIX_0: 21;

    end;

    theorem :: MATRIX_5:10

    for M be Matrix of COMPLEX holds (1 * M) = M

    proof

      set e = ( 1_ F_Complex );

      let M be Matrix of COMPLEX ;

      (1 * M) = ( Field2COMPLEX (e * ( COMPLEX2Field M))) by Def7, COMPLEX1:def 4, COMPLFLD: 8;

      hence thesis by Th9;

    end;

    theorem :: MATRIX_5:11

    for K be Field, a,b be Element of K, M be Matrix of K holds (a * (b * M)) = ((a * b) * M)

    proof

      let K be Field, a,b be Element of K, M be Matrix of K;

      

       A1: ( len ((a * b) * M)) = ( len M) & ( width ((a * b) * M)) = ( width M) by MATRIX_3:def 5;

      

       A2: ( len (a * (b * M))) = ( len (b * M)) by MATRIX_3:def 5;

      

       A3: ( width (a * (b * M))) = ( width (b * M)) by MATRIX_3:def 5;

      then

       A4: ( width (a * (b * M))) = ( width M) by MATRIX_3:def 5;

      

       A5: ( len (b * M)) = ( len M) & ( width (b * M)) = ( width M) by MATRIX_3:def 5;

      

       A6: for i,j be Nat st [i, j] in ( Indices (a * (b * M))) holds ((a * (b * M)) * (i,j)) = (((a * b) * M) * (i,j))

      proof

        let i,j be Nat;

        assume

         A7: [i, j] in ( Indices (a * (b * M)));

        

         A8: ( Indices (b * M)) = ( Indices M) by A5, MATRIX_4: 55;

        

         A9: ( Indices (a * (b * M))) = ( Indices (b * M)) by A2, A3, MATRIX_4: 55;

        

        then ((a * (b * M)) * (i,j)) = (a * ((b * M) * (i,j))) by A7, MATRIX_3:def 5

        .= (a * (b * (M * (i,j)))) by A7, A9, A8, MATRIX_3:def 5

        .= ((a * b) * (M * (i,j))) by GROUP_1:def 3;

        hence thesis by A7, A9, A8, MATRIX_3:def 5;

      end;

      ( len (a * (b * M))) = ( len M) by A2, MATRIX_3:def 5;

      hence thesis by A1, A4, A6, MATRIX_0: 21;

    end;

    theorem :: MATRIX_5:12

    

     Th12: for K be Field, a,b be Element of K, M be Matrix of K holds ((a + b) * M) = ((a * M) + (b * M))

    proof

      let K be Field, a,b be Element of K, M be Matrix of K;

      

       A1: ( len (a * M)) = ( len M) & ( width (a * M)) = ( width M) by MATRIX_3:def 5;

      

       A2: ( len ((a + b) * M)) = ( len M) & ( width ((a + b) * M)) = ( width M) by MATRIX_3:def 5;

      

       A3: for i,j be Nat st [i, j] in ( Indices ((a + b) * M)) holds (((a + b) * M) * (i,j)) = (((a * M) + (b * M)) * (i,j))

      proof

        let i,j be Nat;

        assume

         A4: [i, j] in ( Indices ((a + b) * M));

        

         A5: ( Indices ((a + b) * M)) = ( Indices M) by A2, MATRIX_4: 55;

        ( Indices (a * M)) = ( Indices M) by A1, MATRIX_4: 55;

        

        then (((a * M) + (b * M)) * (i,j)) = (((a * M) * (i,j)) + ((b * M) * (i,j))) by A4, A5, MATRIX_3:def 3

        .= ((a * (M * (i,j))) + ((b * M) * (i,j))) by A4, A5, MATRIX_3:def 5

        .= ((a * (M * (i,j))) + (b * (M * (i,j)))) by A4, A5, MATRIX_3:def 5

        .= ((a + b) * (M * (i,j))) by VECTSP_1:def 7;

        hence thesis by A4, A5, MATRIX_3:def 5;

      end;

      ( len ((a * M) + (b * M))) = ( len (a * M)) & ( width ((a * M) + (b * M))) = ( width (a * M)) by MATRIX_3:def 3;

      hence thesis by A2, A1, A3, MATRIX_0: 21;

    end;

    theorem :: MATRIX_5:13

    for M be Matrix of COMPLEX holds (M + M) = (2 * M)

    proof

      reconsider e2 = (( 1_ F_Complex ) + ( 1_ F_Complex )) as Element of F_Complex ;

      let M be Matrix of COMPLEX ;

      

       A1: (( 1_ F_Complex ) * ( COMPLEX2Field M)) = ( COMPLEX2Field M) by Th9;

      (2 * M) = ( Field2COMPLEX (e2 * ( COMPLEX2Field M))) by Def7, COMPLEX1:def 4, COMPLFLD: 8

      .= ( Field2COMPLEX (( COMPLEX2Field M) + ( COMPLEX2Field M))) by A1, Th12;

      hence thesis;

    end;

    theorem :: MATRIX_5:14

    for M be Matrix of COMPLEX holds ((M + M) + M) = (3 * M)

    proof

      reconsider rr = (1 + 1) as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider e3 = ((( 1_ F_Complex ) + ( 1_ F_Complex )) + ( 1_ F_Complex )) as Element of F_Complex ;

      let M be Matrix of COMPLEX ;

      

       A1: ( len M) = ( len ( COMPLEX2Field M)) & ( width M) = ( width ( COMPLEX2Field M));

      

       A2: (( 1_ F_Complex ) + ( 1_ F_Complex )) = (the addF of F_Complex . (( 1_ F_Complex ),( 1_ F_Complex ))) by RLVECT_1: 2

      .= ( addcomplex . ( 1r , 1r )) by COMPLFLD: 8, COMPLFLD:def 1

      .= (1 + 1) by BINOP_2:def 3, COMPLEX1:def 4;

      ((( 1_ F_Complex ) + ( 1_ F_Complex )) + ( 1_ F_Complex )) = (the addF of F_Complex . ((( 1_ F_Complex ) + ( 1_ F_Complex )),( 1_ F_Complex ))) by RLVECT_1: 2

      .= ( addcomplex . ((1 + 1),1)) by A2, COMPLFLD:def 1

      .= (rr + 1) by BINOP_2:def 3

      .= 3;

      

      then (3 * M) = ( Field2COMPLEX (e3 * ( COMPLEX2Field M))) by Def7

      .= ( Field2COMPLEX ((( 1_ F_Complex ) * ( COMPLEX2Field M)) + ((( 1_ F_Complex ) + ( 1_ F_Complex )) * ( COMPLEX2Field M)))) by Th12

      .= ( Field2COMPLEX (( COMPLEX2Field M) + ((( 1_ F_Complex ) + ( 1_ F_Complex )) * ( COMPLEX2Field M)))) by Th9

      .= ( Field2COMPLEX (( COMPLEX2Field M) + ((( 1_ F_Complex ) * ( COMPLEX2Field M)) + (( 1_ F_Complex ) * ( COMPLEX2Field M))))) by Th12

      .= ( Field2COMPLEX (( COMPLEX2Field M) + (( COMPLEX2Field M) + (( 1_ F_Complex ) * ( COMPLEX2Field M))))) by Th9

      .= ( Field2COMPLEX (( COMPLEX2Field M) + (( COMPLEX2Field M) + ( COMPLEX2Field M)))) by Th9

      .= ( Field2COMPLEX ((( COMPLEX2Field M) + ( COMPLEX2Field M)) + ( COMPLEX2Field M))) by A1, MATRIX_3: 3;

      hence thesis;

    end;

    definition

      let n,m be Nat;

      :: MATRIX_5:def8

      func 0_Cx (n,m) -> Matrix of COMPLEX equals ( Field2COMPLEX ( 0. ( F_Complex ,n,m)));

      coherence ;

    end

    theorem :: MATRIX_5:15

    for n,m be Nat holds ( COMPLEX2Field ( 0_Cx (n,m))) = ( 0. ( F_Complex ,n,m));

    theorem :: MATRIX_5:16

    for M1,M2 be Matrix of COMPLEX st ( len M1) = ( len M2) & ( width M1) = ( width M2) & M1 = (M1 + M2) holds M2 = ( 0_Cx (( len M1),( width M1)))

    proof

      let M1,M2 be Matrix of COMPLEX ;

      assume that

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2) and

       A2: M1 = (M1 + M2);

      ( 0_Cx (( len M1),( width M1))) = ((M1 + M2) + ( - M1)) by A2, MATRIX_4: 2

      .= ( Field2COMPLEX ((( COMPLEX2Field M2) + ( COMPLEX2Field M1)) - ( COMPLEX2Field M1))) by A1, MATRIX_3: 2

      .= M2 by A1, MATRIX_4: 21;

      hence thesis;

    end;

    theorem :: MATRIX_5:17

    for M1,M2 be Matrix of COMPLEX st ( len M1) = ( len M2) & ( width M1) = ( width M2) & (M1 + M2) = ( 0_Cx (( len M1),( width M1))) holds M2 = ( - M1)

    proof

      let M1,M2 be Matrix of COMPLEX ;

      assume that

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2) and

       A2: (M1 + M2) = ( 0_Cx (( len M1),( width M1)));

      

       A3: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;

      ( COMPLEX2Field ( 0_Cx (( len M1),( width M1)))) = (( COMPLEX2Field M1) - ( - ( COMPLEX2Field M2))) by A2, MATRIX_4: 1;

      then ( COMPLEX2Field M1) = ( - ( COMPLEX2Field M2)) by A1, A3, MATRIX_4: 7;

      hence thesis by MATRIX_4: 1;

    end;

    theorem :: MATRIX_5:18

    for M1,M2 be Matrix of COMPLEX st ( len M1) = ( len M2) & ( width M1) = ( width M2) & (M2 - M1) = M2 holds M1 = ( 0_Cx (( len M1),( width M1)))

    proof

      let M1,M2 be Matrix of COMPLEX ;

      assume that

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2) and

       A2: (M2 - M1) = M2;

      (( COMPLEX2Field M2) + ( COMPLEX2Field M1)) = ( COMPLEX2Field M2) by A1, A2, MATRIX_4: 22;

      hence thesis by A1, MATRIX_4: 6;

    end;

    theorem :: MATRIX_5:19

    for M be Matrix of COMPLEX holds (M + ( 0_Cx (( len M),( width M)))) = M

    proof

      let M be Matrix of COMPLEX ;

      

       A1: ( len M) = ( len ( COMPLEX2Field M)) & ( width M) = ( width ( COMPLEX2Field M));

      (M + ( 0_Cx (( len M),( width M)))) = (M + ( - ( 0_Cx (( len M),( width M))))) by MATRIX_4: 9

      .= ( Field2COMPLEX (( COMPLEX2Field M) - (( COMPLEX2Field M) - ( COMPLEX2Field M)))) by MATRIX_4: 3

      .= M by A1, MATRIX_4: 11;

      hence thesis;

    end;

    theorem :: MATRIX_5:20

    

     Th20: for K be Field, b be Element of K, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds (b * (M1 + M2)) = ((b * M1) + (b * M2))

    proof

      let K be Field, b be Element of K, M1,M2 be Matrix of K;

      

       A1: ( len (b * (M1 + M2))) = ( len (M1 + M2)) & ( width (b * (M1 + M2))) = ( width (M1 + M2)) by MATRIX_3:def 5;

      

       A2: ( len (M1 + M2)) = ( len M1) & ( width (M1 + M2)) = ( width M1) by MATRIX_3:def 3;

      

       A3: ( len (b * M1)) = ( len M1) & ( width (b * M1)) = ( width M1) by MATRIX_3:def 5;

      assume

       A4: ( len M1) = ( len M2) & ( width M1) = ( width M2);

      

       A5: for i,j be Nat st [i, j] in ( Indices (b * (M1 + M2))) holds ((b * (M1 + M2)) * (i,j)) = (((b * M1) + (b * M2)) * (i,j))

      proof

        let i,j be Nat;

        assume

         A6: [i, j] in ( Indices (b * (M1 + M2)));

        

         A7: ( Indices M2) = ( Indices M1) by A4, MATRIX_4: 55;

        

         A8: ( Indices (b * (M1 + M2))) = ( Indices (M1 + M2)) by A1, MATRIX_4: 55;

        

         A9: ( Indices (M1 + M2)) = ( Indices M1) by A2, MATRIX_4: 55;

        ( Indices (b * M1)) = ( Indices M1) by A3, MATRIX_4: 55;

        

        then (((b * M1) + (b * M2)) * (i,j)) = (((b * M1) * (i,j)) + ((b * M2) * (i,j))) by A6, A8, A9, MATRIX_3:def 3

        .= ((b * (M1 * (i,j))) + ((b * M2) * (i,j))) by A6, A8, A9, MATRIX_3:def 5

        .= ((b * (M1 * (i,j))) + (b * (M2 * (i,j)))) by A6, A8, A9, A7, MATRIX_3:def 5

        .= (b * ((M1 * (i,j)) + (M2 * (i,j)))) by VECTSP_1:def 7;

        

        then (((b * M1) + (b * M2)) * (i,j)) = (b * ((M1 + M2) * (i,j))) by A6, A8, A9, MATRIX_3:def 3

        .= ((b * (M1 + M2)) * (i,j)) by A6, A8, MATRIX_3:def 5;

        hence thesis;

      end;

      ( len ((b * M1) + (b * M2))) = ( len (b * M1)) & ( width ((b * M1) + (b * M2))) = ( width (b * M1)) by MATRIX_3:def 3;

      hence thesis by A1, A2, A3, A5, MATRIX_0: 21;

    end;

    theorem :: MATRIX_5:21

    for M1,M2 be Matrix of COMPLEX holds for a be Complex st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds (a * (M1 + M2)) = ((a * M1) + (a * M2))

    proof

      let M1,M2 be Matrix of COMPLEX ;

      let a be Complex;

      assume

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2);

      a in COMPLEX by XCMPLX_0:def 2;

      then

      reconsider ea = a as Element of F_Complex by COMPLFLD:def 1;

      

       A2: ((a * M1) + (a * M2)) = ( Field2COMPLEX (( COMPLEX2Field ( Field2COMPLEX (ea * ( COMPLEX2Field M1)))) + ( COMPLEX2Field (a * M2)))) by Def7

      .= ( Field2COMPLEX ((ea * ( COMPLEX2Field M1)) + ( COMPLEX2Field ( Field2COMPLEX (ea * ( COMPLEX2Field M2)))))) by Def7

      .= ( Field2COMPLEX ((ea * ( COMPLEX2Field M1)) + (ea * ( COMPLEX2Field M2))));

      (a * (M1 + M2)) = ( Field2COMPLEX (ea * ( COMPLEX2Field (M1 + M2)))) by Def7

      .= ( Field2COMPLEX ((ea * ( COMPLEX2Field M1)) + (ea * ( COMPLEX2Field M2)))) by A1, Th20;

      hence thesis by A2;

    end;

    theorem :: MATRIX_5:22

    

     Th22: for K be Field, M1,M2 be Matrix of K st ( width M1) = ( len M2) & ( len M1) > 0 & ( len M2) > 0 holds (( 0. (K,( len M1),( width M1))) * M2) = ( 0. (K,( len M1),( width M2)))

    proof

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

      assume that

       A1: ( width M1) = ( len M2) and

       A2: ( len M1) > 0 and

       A3: ( len M2) > 0 ;

      

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

      then

       A5: ( width ( 0. (K,( len M1),( width M1)))) = ( width M1) by A2, MATRIX_0: 20;

      then

       A6: ( len (( 0. (K,( len M1),( width M1))) * M2)) = ( len ( 0. (K,( len M1),( width M1)))) by A1, MATRIX_3:def 4;

      

       A7: ( width (( 0. (K,( len M1),( width M1))) * M2)) = ( width M2) by A1, A5, MATRIX_3:def 4;

      set B = (( 0. (K,( len M1),( width M1))) * M2);

      

       A8: ( width ( - (( 0. (K,( len M1),( width M1))) * M2))) = ( width (( 0. (K,( len M1),( width M1))) * M2)) by MATRIX_3:def 2;

      (( 0. (K,( len M1),( width M1))) * M2) = ((( 0. (K,( len M1),( width M1))) + ( 0. (K,( len M1),( width M1)))) * M2) by MATRIX_3: 4

      .= ((( 0. (K,( len M1),( width M1))) * M2) + (( 0. (K,( len M1),( width M1))) * M2)) by A1, A2, A3, A4, A5, MATRIX_4: 63;

      then ( len ( - (( 0. (K,( len M1),( width M1))) * M2))) = ( len (( 0. (K,( len M1),( width M1))) * M2)) & ( 0. (K,( len M1),( width M2))) = ((B + B) + ( - B)) by A4, A6, A7, MATRIX_3:def 2, MATRIX_4: 2;

      

      then ( 0. (K,( len M1),( width M2))) = (B + (B - B)) by A8, MATRIX_3: 3

      .= (( 0. (K,( len M1),( width M1))) * M2) by A6, A8, MATRIX_4: 20;

      hence thesis;

    end;

    theorem :: MATRIX_5:23

    for M1,M2 be Matrix of COMPLEX st ( width M1) = ( len M2) & ( len M1) > 0 & ( len M2) > 0 holds (( 0_Cx (( len M1),( width M1))) * M2) = ( 0_Cx (( len M1),( width M2)))

    proof

      let M1,M2 be Matrix of COMPLEX ;

      

       A1: ( len M1) = ( len ( COMPLEX2Field M1));

      assume ( width M1) = ( len M2) & ( len M1) > 0 & ( len M2) > 0 ;

      hence thesis by A1, Th22;

    end;

    theorem :: MATRIX_5:24

    

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

    proof

      let K be Field, M1 be Matrix of K;

      

       A1: ( len ( 0. (K,( len M1),( width M1)))) = ( len M1) by MATRIX_0:def 2;

      assume ( len M1) > 0 ;

      then

       A2: ( width ( 0. (K,( len M1),( width M1)))) = ( width M1) by A1, MATRIX_0: 20;

      

       A3: for i,j be Nat st [i, j] in ( Indices ( 0. (K,( len M1),( width M1)))) holds ((( 0. K) * M1) * (i,j)) = (( 0. (K,( len M1),( width M1))) * (i,j))

      proof

        let i,j be Nat;

        assume

         A4: [i, j] in ( Indices ( 0. (K,( len M1),( width M1))));

        ( Indices ( 0. (K,( len M1),( width M1)))) = ( Indices M1) by A1, A2, MATRIX_4: 55;

        then

         A5: ((( 0. K) * M1) * (i,j)) = (( 0. K) * (M1 * (i,j))) by A4, MATRIX_3:def 5;

        (( 0. (K,( len M1),( width M1))) * (i,j)) = ( 0. K) by A4, MATRIX_3: 1;

        hence thesis by A5;

      end;

      ( len (( 0. K) * M1)) = ( len M1) & ( width (( 0. K) * M1)) = ( width M1) by MATRIX_3:def 5;

      hence thesis by A1, A2, A3, MATRIX_0: 21;

    end;

    theorem :: MATRIX_5:25

    for M1 be Matrix of COMPLEX st ( len M1) > 0 holds ( 0 * M1) = ( 0_Cx (( len M1),( width M1)))

    proof

      reconsider ea = 0 as Element of F_Complex by COMPLFLD:def 1;

      let M1 be Matrix of COMPLEX ;

      assume

       A1: ( len M1) > 0 ;

      ( 0 * M1) = ( Field2COMPLEX (ea * ( COMPLEX2Field M1))) by Def7

      .= ( 0_Cx (( len M1),( width M1))) by A1, Th24, COMPLFLD: 7;

      hence thesis;

    end;

    definition

      let s be complex-valued Function, k be set;

      :: original: .

      redefine

      func s . k -> Element of COMPLEX ;

      coherence

      proof

        per cases ;

          suppose

           A1: k in ( dom s);

          

           A2: ( rng s) c= COMPLEX by VALUED_0:def 1;

          (s . k) in ( rng s) by A1, FUNCT_1:def 3;

          hence thesis by A2;

        end;

          suppose not k in ( dom s);

          then (s . k) = 0c by FUNCT_1:def 2;

          hence thesis;

        end;

      end;

    end

    theorem :: MATRIX_5:26

    for i,j be Nat, M1,M2 be Matrix of COMPLEX st ( len M2) > 0 holds ex s be FinSequence of COMPLEX st ( len s) = ( len M2) & (s . 1) = ((M1 * (i,1)) * (M2 * (1,j))) & for k be Nat st 1 <= k & k < ( len M2) holds (s . (k + 1)) = ((s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))))

    proof

      let i,j be Nat, M1,M2 be Matrix of COMPLEX ;

      defpred P[ Nat] means ex q be FinSequence of COMPLEX st 1 <= ($1 + 1) & ($1 + 1) <= ( len M2) implies (( len q) = ($1 + 1) & (q . 1) = ((M1 * (i,1)) * (M2 * (1,j))) & (for k be Nat st 1 <= k & k < ($1 + 1) holds (q . (k + 1)) = ((q . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))))));

      reconsider q0 = <*((M1 * (i,1)) * (M2 * (1,j)))*> as FinSequence of COMPLEX by RVSUM_1: 146;

      

       A1: for k be Nat st 1 <= k & k < 1 holds (q0 . (k + 1)) = ((q0 . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))));

      

       A2: for i2 be Nat st P[i2] holds P[(i2 + 1)]

      proof

        let i2 be Nat;

        set k0 = i2;

        assume P[i2];

        then

        consider q2 be FinSequence of COMPLEX such that

         A3: 1 <= (i2 + 1) & (i2 + 1) <= ( len M2) implies ( len q2) = (i2 + 1) & (q2 . 1) = ((M1 * (i,1)) * (M2 * (1,j))) & for k2 be Nat st 1 <= k2 & k2 < (i2 + 1) holds (q2 . (k2 + 1)) = ((q2 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))));

        reconsider q3 = (q2 ^ <*((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j))))*>) as FinSequence of COMPLEX by RVSUM_1: 146;

        1 <= ((i2 + 1) + 1) & ((i2 + 1) + 1) <= ( len M2) implies ( len q3) = ((i2 + 1) + 1) & (q3 . 1) = ((M1 * (i,1)) * (M2 * (1,j))) & for k be Nat st 1 <= k & k < ((i2 + 1) + 1) holds (q3 . (k + 1)) = ((q3 . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))))

        proof

          assume that 1 <= ((i2 + 1) + 1) and

           A4: ((i2 + 1) + 1) <= ( len M2);

          

           A5: 1 <= (i2 + 1) by NAT_1: 12;

          

          thus

           A6: ( len q3) = (( len q2) + ( len <*((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j))))*>)) by FINSEQ_1: 22

          .= ((i2 + 1) + 1) by A3, A4, A5, FINSEQ_1: 39, NAT_1: 13;

          

           A7: for k2 be Nat st 1 <= k2 & k2 < ((i2 + 1) + 1) holds (q3 . (k2 + 1)) = ((q3 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))))

          proof

            let k2 be Nat;

            assume that

             A8: 1 <= k2 and

             A9: k2 < ((i2 + 1) + 1);

            

             A10: k2 <= (i2 + 1) by A9, NAT_1: 13;

            per cases by A10, XXREAL_0: 1;

              suppose

               A11: k2 < (i2 + 1);

              then k2 < ( len q3) by A6, NAT_1: 13;

              then k2 < (( len q2) + ( len <*((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j))))*>)) by FINSEQ_1: 22;

              then k2 < (( len q2) + 1) by FINSEQ_1: 39;

              then k2 <= ( len q2) by NAT_1: 13;

              then k2 in ( dom q2) by A8, FINSEQ_3: 25;

              then

               A12: (q3 . k2) = (q2 . k2) by FINSEQ_1:def 7;

              (k2 + 1) < ((i2 + 1) + 1) by A11, XREAL_1: 6;

              then (k2 + 1) < (( len q2) + ( len <*((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j))))*>)) by A6, FINSEQ_1: 22;

              then (k2 + 1) < (( len q2) + 1) by FINSEQ_1: 39;

              then

               A13: (k2 + 1) <= ( len q2) by NAT_1: 13;

              1 <= (k2 + 1) by A8, NAT_1: 13;

              then (k2 + 1) in ( dom q2) by A13, FINSEQ_3: 25;

              then (q3 . (k2 + 1)) = (q2 . (k2 + 1)) by FINSEQ_1:def 7;

              hence thesis by A3, A4, A5, A8, A11, A12, NAT_1: 13;

            end;

              suppose

               A14: k2 = (i2 + 1);

              then k2 < ((i2 + 1) + 1) by NAT_1: 13;

              then k2 < (( len q2) + ( len <*((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j))))*>)) by A6, FINSEQ_1: 22;

              then k2 < (( len q2) + 1) by FINSEQ_1: 39;

              then k2 <= ( len q2) by NAT_1: 13;

              then k2 in ( dom q2) by A8, FINSEQ_3: 25;

              then

               A15: (q3 . k2) = (q2 . k2) by FINSEQ_1:def 7;

              1 in ( Seg 1) by FINSEQ_1: 3;

              then ( <*((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j))))*> . 1) = ((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j)))) & 1 in ( dom <*((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j))))*>) by FINSEQ_1:def 8;

              hence thesis by A3, A4, A5, A14, A15, FINSEQ_1:def 7, NAT_1: 13;

            end;

          end;

          1 < ( len (q2 ^ <*((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j))))*>)) by A5, A6, NAT_1: 13;

          then 1 < (( len q2) + ( len <*((q2 . (k0 + 1)) + ((M1 * (i,((k0 + 1) + 1))) * (M2 * (((k0 + 1) + 1),j))))*>)) by FINSEQ_1: 22;

          then 1 < (( len q2) + 1) by FINSEQ_1: 39;

          then 1 <= ( len q2) by NAT_1: 13;

          then 1 in ( dom q2) by FINSEQ_3: 25;

          hence thesis by A3, A4, A5, A7, FINSEQ_1:def 7, NAT_1: 13;

        end;

        hence thesis;

      end;

      ( len q0) = 1 & (q0 . 1) = ((M1 * (i,1)) * (M2 * (1,j))) by FINSEQ_1: 39, FINSEQ_1:def 8;

      then

       A16: P[ 0 ] by A1;

      

       A17: for j be Nat holds P[j] from NAT_1:sch 2( A16, A2);

      assume

       A18: ( len M2) > 0 ;

      then ( 0 + 1) <= ( len M2) by NAT_1: 8;

      then (( 0 + 1) - 1) <= (( len M2) - 1) by XREAL_1: 9;

      then

       A19: (( len M2) -' 1) = (( len M2) - 1) by XREAL_0:def 2;

      then ( 0 + 1) <= ((( len M2) -' 1) + 1) by A18, NAT_1: 8;

      hence thesis by A19, A17;

    end;