let i, j be Nat; for M1, M2 being Matrix of COMPLEX st width M1 = width M2 & j in Seg (len M1) holds
Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j))
let M1, M2 be Matrix of COMPLEX; ( width M1 = width M2 & j in Seg (len M1) implies Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j)) )
assume that
A1:
width M1 = width M2
and
A2:
j in Seg (len M1)
; Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j))
len (Line (M2,j)) =
width M1
by A1, MATRIX_0:def 7
.=
len (Line (M1,j))
by MATRIX_0:def 7
;
then A3: len ((Line (M1,j)) + (Line (M2,j))) =
len (Line (M1,j))
by COMPLSP2:6
.=
width M1
by MATRIX_0:def 7
;
A4: len (Line ((M1 + M2),j)) =
width (M1 + M2)
by MATRIX_0:def 7
.=
width M1
by Th5
;
A5:
width (M1 + M2) = width M1
by Th5;
now for i being Nat st 1 <= i & i <= len (Line ((M1 + M2),j)) holds
(Line ((M1 + M2),j)) . i = ((Line (M1,j)) + (Line (M2,j))) . ilet i be
Nat;
( 1 <= i & i <= len (Line ((M1 + M2),j)) implies (Line ((M1 + M2),j)) . i = ((Line (M1,j)) + (Line (M2,j))) . i )assume that A6:
1
<= i
and A7:
i <= len (Line ((M1 + M2),j))
;
(Line ((M1 + M2),j)) . i = ((Line (M1,j)) + (Line (M2,j))) . iA8:
i in Seg (width M1)
by A4, A6, A7, FINSEQ_1:1;
i in Seg (width M1)
by A4, A6, A7, FINSEQ_1:1;
then
[j,i] in [:(Seg (len M1)),(Seg (width M1)):]
by A2, ZFMISC_1:87;
then A9:
[j,i] in Indices M1
by FINSEQ_1:def 3;
i in Seg (len ((Line (M1,j)) + (Line (M2,j))))
by A3, A4, A6, A7, FINSEQ_1:1;
then A10:
i in dom ((Line (M1,j)) + (Line (M2,j)))
by FINSEQ_1:def 3;
A11:
i in Seg (width M2)
by A1, A4, A6, A7, FINSEQ_1:1;
i in Seg (width (M1 + M2))
by A5, A4, A6, A7, FINSEQ_1:1;
hence (Line ((M1 + M2),j)) . i =
(M1 + M2) * (
j,
i)
by MATRIX_0:def 7
.=
(M1 * (j,i)) + (M2 * (j,i))
by A9, Th6
.=
(M1 * (j,i)) + ((Line (M2,j)) . i)
by A11, MATRIX_0:def 7
.=
((Line (M1,j)) . i) + ((Line (M2,j)) . i)
by A8, MATRIX_0:def 7
.=
((Line (M1,j)) + (Line (M2,j))) . i
by A10, COMPLSP2:1
;
verum end;
hence
Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j))
by A3, A4, FINSEQ_1:14; verum