let M1, M2 be Matrix of COMPLEX ; :: thesis: ( len M1 = len M2 & width M1 = width M2 implies (M1 - M2) *' = (M1 *' ) - (M2 *' ) )
assume A1:
( len M1 = len M2 & width M1 = width M2 )
; :: thesis: (M1 - M2) *' = (M1 *' ) - (M2 *' )
A2:
len ((M1 - M2) *' ) = len (M1 - M2)
by Def1;
A3:
len (M1 *' ) = len M1
by Def1;
A4:
len (M2 *' ) = len M2
by Def1;
A5:
width (M1 *' ) = width M1
by Def1;
A6:
width (M2 *' ) = width M2
by Def1;
A7:
len (M1 - M2) = len M1
by Th13;
A8:
len ((M1 *' ) - (M2 *' )) = len (M1 *' )
by Th13;
A9:
width ((M1 - M2) *' ) = width (M1 - M2)
by Def1;
A10:
width (M1 - M2) = width M1
by Th13;
A11:
width ((M1 *' ) - (M2 *' )) = width (M1 *' )
by Th13;
A12:
width (M1 *' ) = width M1
by Def1;
now let i,
j be
Nat;
:: thesis: ( [i,j] in Indices ((M1 - M2) *' ) implies ((M1 - M2) *' ) * i,j = ((M1 *' ) - (M2 *' )) * i,j )assume
[i,j] in Indices ((M1 - M2) *' )
;
:: thesis: ((M1 - M2) *' ) * i,j = ((M1 *' ) - (M2 *' )) * i,jthen A13:
( 1
<= i &
i <= len (M1 - M2) & 1
<= j &
j <= width (M1 - M2) )
by A2, A9, Th1;
then A14:
[i,j] in Indices (M1 - M2)
by Th1;
A15:
[i,j] in Indices M1
by A7, A10, A13, Th1;
( 1
<= i &
i <= len (M1 *' ) & 1
<= j &
j <= width (M1 *' ) )
by A7, A10, A13, Def1;
then A16:
[i,j] in Indices (M1 *' )
by Th1;
A17:
[i,j] in Indices M2
by A1, A7, A10, A13, Th1;
((M1 - M2) *' ) * i,
j = ((M1 - M2) * i,j) *'
by A14, Def1;
hence ((M1 - M2) *' ) * i,
j =
((M1 * i,j) - (M2 * i,j)) *'
by A1, A15, Th14
.=
((M1 * i,j) *' ) - ((M2 * i,j) *' )
by COMPLEX1:120
.=
((M1 *' ) * i,j) - ((M2 * i,j) *' )
by A15, Def1
.=
((M1 *' ) * i,j) - ((M2 *' ) * i,j)
by A17, Def1
.=
((M1 *' ) - (M2 *' )) * i,
j
by A1, A3, A4, A5, A6, A16, Th14
;
:: thesis: verum end;
hence
(M1 - M2) *' = (M1 *' ) - (M2 *' )
by A2, A3, A7, A8, A9, A10, A11, A12, MATRIX_1:21; :: thesis: verum