let M1, M2 be Matrix of COMPLEX; ( len M1 = len M2 & width M1 = width M2 implies (M1 - M2) *' = (M1 *') - (M2 *') )
assume that
A1:
len M1 = len M2
and
A2:
width M1 = width M2
; (M1 - M2) *' = (M1 *') - (M2 *')
A3:
len ((M1 - M2) *') = len (M1 - M2)
by Def1;
A4:
width ((M1 - M2) *') = width (M1 - M2)
by Def1;
A5:
width (M1 - M2) = width M1
by Th12;
A6:
width (M1 *') = width M1
by Def1;
A7:
len (M1 *') = len M1
by Def1;
A8:
width (M2 *') = width M2
by Def1;
A9:
len (M1 - M2) = len M1
by Th12;
A10:
len (M2 *') = len M2
by Def1;
A11:
now for i, j being Nat st [i,j] in Indices ((M1 - M2) *') holds
((M1 - M2) *') * (i,j) = ((M1 *') - (M2 *')) * (i,j)let i,
j be
Nat;
( [i,j] in Indices ((M1 - M2) *') implies ((M1 - M2) *') * (i,j) = ((M1 *') - (M2 *')) * (i,j) )assume A12:
[i,j] in Indices ((M1 - M2) *')
;
((M1 - M2) *') * (i,j) = ((M1 *') - (M2 *')) * (i,j)then A13:
1
<= j
by Th1;
A14:
1
<= i
by A12, Th1;
A15:
j <= width (M1 - M2)
by A4, A12, Th1;
then A16:
j <= width (M1 *')
by A5, Def1;
A17:
i <= len (M1 - M2)
by A3, A12, Th1;
then
i <= len (M1 *')
by A9, Def1;
then A18:
[i,j] in Indices (M1 *')
by A13, A14, A16, Th1;
A19:
1
<= i
by A12, Th1;
then A20:
[i,j] in Indices M1
by A9, A5, A17, A13, A15, Th1;
A21:
[i,j] in Indices M2
by A1, A2, A9, A5, A19, A17, A13, A15, Th1;
[i,j] in Indices (M1 - M2)
by A19, A17, A13, A15, Th1;
then
((M1 - M2) *') * (
i,
j)
= ((M1 - M2) * (i,j)) *'
by Def1;
hence ((M1 - M2) *') * (
i,
j) =
((M1 * (i,j)) - (M2 * (i,j))) *'
by A1, A2, A20, Th13
.=
((M1 * (i,j)) *') - ((M2 * (i,j)) *')
by COMPLEX1:34
.=
((M1 *') * (i,j)) - ((M2 * (i,j)) *')
by A20, Def1
.=
((M1 *') * (i,j)) - ((M2 *') * (i,j))
by A21, Def1
.=
((M1 *') - (M2 *')) * (
i,
j)
by A1, A2, A7, A10, A6, A8, A18, Th13
;
verum end;
A22:
width (M1 *') = width M1
by Def1;
A23:
width ((M1 *') - (M2 *')) = width (M1 *')
by Th12;
len ((M1 *') - (M2 *')) = len (M1 *')
by Th12;
hence
(M1 - M2) *' = (M1 *') - (M2 *')
by A3, A7, A9, A4, A5, A23, A22, A11, MATRIX_0:21; verum