defpred S1[ Nat] means for N being Matrix of COMPLEX st $1 + 1 = len N holds
Sum (LineSum N) = Sum (ColSum N);
let M be Matrix of COMPLEX; :: thesis: ( len M > 0 implies Sum (LineSum M) = Sum (ColSum M) )
assume len M > 0 ; :: thesis: Sum (LineSum M) = Sum (ColSum M)
then 0 + 1 <= len M by NAT_1:8;
then (0 + 1) - 1 <= (len M) - 1 by XREAL_1:11;
then A1: (len M) -' 1 = (len M) - 1 by XREAL_0:def 2;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
for N being Matrix of COMPLEX st (k + 1) + 1 = len N holds
Sum (LineSum N) = Sum (ColSum N)
proof
reconsider k1 = k + 1 as Element of NAT ;
let N be Matrix of COMPLEX; :: thesis: ( (k + 1) + 1 = len N implies Sum (LineSum N) = Sum (ColSum N) )
consider n being Nat such that
A4: for x being set st x in rng N holds
ex p being FinSequence of COMPLEX st
( x = p & len p = n ) by MATRIX_1:9;
A5: rng (N | k1) c= rng N by FINSEQ_5:21;
then for x being set st x in rng (N | k1) holds
ex p being FinSequence of COMPLEX st
( x = p & len p = n ) by A4;
then reconsider N2 = N | k1 as Matrix of COMPLEX by MATRIX_1:9;
set g1 = LineSum N2;
consider n3 being Nat such that
A6: for x2 being set st x2 in rng N holds
ex s being FinSequence st
( s = x2 & len s = n3 ) by MATRIX_1:def 1;
set f3 = LineSum N;
A7: len (Line (N,((k + 1) + 1))) = width N by MATRIX_1:def 8;
assume A8: (k + 1) + 1 = len N ; :: thesis: Sum (LineSum N) = Sum (ColSum N)
then A9: len N2 = k + 1 by FINSEQ_1:80, NAT_1:11;
A10: len (LineSum N2) = len N2 by Def10
.= k1 by A8, FINSEQ_1:80, NAT_1:11 ;
1 + k >= 1 by NAT_1:11;
then A11: len N2 >= 1 by A8, FINSEQ_1:80, NAT_1:11;
then 1 in Seg (len N2) by FINSEQ_1:3;
then 1 in dom N2 by FINSEQ_1:def 3;
then A12: N2 . 1 in rng N2 by FUNCT_1:12;
then ex s3 being FinSequence st
( s3 = N2 . 1 & len s3 = n3 ) by A5, A6;
then A13: width N2 = n3 by A11, A12, MATRIX_1:def 4;
len N >= 1 by A8, NAT_1:11;
then 1 in Seg (len N) by FINSEQ_1:3;
then A14: 1 in dom N by FINSEQ_1:def 3;
then A15: N . 1 in rng N by FUNCT_1:12;
A16: ex s2 being FinSequence st
( s2 = N . 1 & len s2 = n3 ) by A6, A14, FUNCT_1:12;
then A17: width N2 = width N by A8, A15, A13, MATRIX_1:def 4;
len (LineSum N) = k1 + 1 by A8, Def10;
then A18: len ((LineSum N) | k1) = len (LineSum N2) by A10, FINSEQ_1:80, NAT_1:11;
A19: for n being Nat st 1 <= n & n <= len ((LineSum N) | k1) holds
((LineSum N) | k1) . n = (LineSum N2) . n
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len ((LineSum N) | k1) implies ((LineSum N) | k1) . n = (LineSum N2) . n )
assume that
A20: 1 <= n and
A21: n <= len ((LineSum N) | k1) ; :: thesis: ((LineSum N) | k1) . n = (LineSum N2) . n
A22: n <= k1 + 1 by A10, A18, A21, NAT_1:13;
then A23: n in Seg (len N) by A8, A20, FINSEQ_1:3;
A24: for n1 being Nat st 1 <= n1 & n1 <= len (Line (N,n)) holds
(Line (N,n)) . n1 = (Line (N2,n)) . n1
proof
A25: N2 . n = N . n by A10, A18, A21, FINSEQ_3:121;
A26: n <= len N2 by A18, A21, Def10;
let n1 be Nat; :: thesis: ( 1 <= n1 & n1 <= len (Line (N,n)) implies (Line (N,n)) . n1 = (Line (N2,n)) . n1 )
assume that
A27: 1 <= n1 and
A28: n1 <= len (Line (N,n)) ; :: thesis: (Line (N,n)) . n1 = (Line (N2,n)) . n1
A29: n1 in Seg (len (Line (N,n))) by A27, A28, FINSEQ_1:3;
then A30: n1 in Seg (width N2) by A17, MATRIX_1:def 8;
A31: n1 in Seg (width N) by A29, MATRIX_1:def 8;
then n1 <= width N by FINSEQ_1:3;
then [n,n1] in Indices N by A8, A20, A22, A27, Th1;
then A32: ex pn being FinSequence of COMPLEX st
( pn = N . n & N * (n,n1) = pn . n1 ) by MATRIX_1:def 6;
n1 <= width N by A31, FINSEQ_1:3;
then n1 <= width N2 by A8, A15, A16, A13, MATRIX_1:def 4;
then A33: [n,n1] in Indices N2 by A20, A27, A26, Th1;
n1 in Seg (width N) by A29, MATRIX_1:def 8;
then (Line (N,n)) . n1 = N * (n,n1) by MATRIX_1:def 8
.= N2 * (n,n1) by A33, A32, A25, MATRIX_1:def 6
.= (Line (N2,n)) . n1 by A30, MATRIX_1:def 8 ;
hence (Line (N,n)) . n1 = (Line (N2,n)) . n1 ; :: thesis: verum
end;
len (Line (N,n)) = width N by MATRIX_1:def 8
.= width N2 by A8, A15, A16, A13, MATRIX_1:def 4
.= len (Line (N2,n)) by MATRIX_1:def 8 ;
then A34: Line (N,n) = Line (N2,n) by A24, FINSEQ_1:18;
n in Seg (len ((LineSum N) | k1)) by A20, A21, FINSEQ_1:3;
then n in dom ((LineSum N) | k1) by FINSEQ_1:def 3;
then A35: n in dom ((LineSum N) | (Seg k1)) by FINSEQ_1:def 15;
n in Seg k1 by A10, A18, A20, A21, FINSEQ_1:3;
then A36: n in Seg (len N2) by A8, FINSEQ_1:80, NAT_1:11;
((LineSum N) | k1) . n = ((LineSum N) | (Seg k1)) . n by FINSEQ_1:def 15
.= (LineSum N) . n by A35, FUNCT_1:70
.= Sum (Line (N2,n)) by A23, A34, Def10
.= (LineSum N2) . n by A36, Def10 ;
hence ((LineSum N) | k1) . n = (LineSum N2) . n ; :: thesis: verum
end;
len (ColSum N2) = width N2 by Def11;
then A37: len ((ColSum N2) + (Line (N,((k + 1) + 1)))) = width N by A17, A7, COMPLSP2:6
.= len (ColSum N) by Def11 ;
A38: len (ColSum N2) = width N2 by Def11
.= width N by A8, A15, A16, A13, MATRIX_1:def 4
.= len (Line (N,((k + 1) + 1))) by MATRIX_1:def 8 ;
A39: (k + 1) + 1 in Seg (len N) by A8, FINSEQ_1:5;
then (k + 1) + 1 in Seg (len (LineSum N)) by Def10;
then A40: (k + 1) + 1 in dom (LineSum N) by FINSEQ_1:def 3;
A41: len N >= k + 1 by A8, NAT_1:11;
A42: for j being Nat st 1 <= j & j <= width N holds
((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= width N implies ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j )
assume that
A43: 1 <= j and
A44: j <= width N ; :: thesis: ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j
set g = Col (N2,j);
set f = Col (N,j);
A45: k1 <= len (Col (N,j)) by A41, MATRIX_1:def 9;
A46: for n being Nat st 1 <= n & n <= len ((Col (N,j)) | k1) holds
((Col (N,j)) | k1) . n = (Col (N2,j)) . n
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len ((Col (N,j)) | k1) implies ((Col (N,j)) | k1) . n = (Col (N2,j)) . n )
assume that
A47: 1 <= n and
A48: n <= len ((Col (N,j)) | k1) ; :: thesis: ((Col (N,j)) | k1) . n = (Col (N2,j)) . n
A49: n <= k1 by A45, A48, FINSEQ_1:80;
then A50: N2 . n = N . n by FINSEQ_3:121;
n <= k1 + 1 by A49, NAT_1:13;
then n in Seg (len N) by A8, A47, FINSEQ_1:3;
then A51: n in dom N by FINSEQ_1:def 3;
n <= len N by A8, A49, NAT_1:13;
then [n,j] in Indices N by A43, A44, A47, Th1;
then A52: ex pn being FinSequence of COMPLEX st
( pn = N . n & N * (n,j) = pn . j ) by MATRIX_1:def 6;
A53: j <= width N2 by A8, A15, A16, A13, A44, MATRIX_1:def 4;
n in Seg k1 by A47, A49, FINSEQ_1:3;
then A54: n in dom N2 by A9, FINSEQ_1:def 3;
n in Seg (len ((Col (N,j)) | k1)) by A47, A48, FINSEQ_1:3;
then n in dom ((Col (N,j)) | k1) by FINSEQ_1:def 3;
then A55: n in dom ((Col (N,j)) | (Seg k1)) by FINSEQ_1:def 15;
n <= len N2 by A9, A45, A48, FINSEQ_1:80;
then A56: [n,j] in Indices N2 by A43, A47, A53, Th1;
((Col (N,j)) | k1) . n = ((Col (N,j)) | (Seg k1)) . n by FINSEQ_1:def 15
.= (Col (N,j)) . n by A55, FUNCT_1:70
.= N * (n,j) by A51, MATRIX_1:def 9
.= N2 * (n,j) by A56, A52, A50, MATRIX_1:def 6
.= (Col (N2,j)) . n by A54, MATRIX_1:def 9 ;
hence ((Col (N,j)) | k1) . n = (Col (N2,j)) . n ; :: thesis: verum
end;
A57: (k + 1) + 1 in Seg (len N) by A8, FINSEQ_1:6;
then A58: (k + 1) + 1 in dom N by FINSEQ_1:def 3;
len (Col (N2,j)) = len N2 by MATRIX_1:def 9
.= k1 by A8, FINSEQ_1:80, NAT_1:11 ;
then A59: Col (N2,j) = (Col (N,j)) | k1 by A45, A46, FINSEQ_1:18, FINSEQ_1:80;
A60: len (Col (N,j)) = len N by MATRIX_1:def 9;
(k + 1) + 1 in Seg (len (Col (N,j))) by A57, MATRIX_1:def 9;
then A61: (k + 1) + 1 in dom (Col (N,j)) by FINSEQ_1:def 3;
A62: j in Seg (width N) by A43, A44, FINSEQ_1:3;
then ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (Sum (Col (N2,j))) + (N * (((k + 1) + 1),j)) by A17, Def11
.= (Sum (Col (N2,j))) + ((Col (N,j)) . ((k + 1) + 1)) by A58, MATRIX_1:def 9
.= (Sum (Col (N2,j))) + ((Col (N,j)) /. ((k + 1) + 1)) by A61, PARTFUN1:def 8
.= Sum (Col (N,j)) by A8, A60, A59, Th51
.= (ColSum N) . j by A62, Def11 ;
hence ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j ; :: thesis: verum
end;
A63: for j being Nat st 1 <= j & j <= len (ColSum N) holds
((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= len (ColSum N) implies ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j )
assume that
A64: 1 <= j and
A65: j <= len (ColSum N) ; :: thesis: ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j
j in Seg (len (ColSum N)) by A64, A65, FINSEQ_1:3;
then A66: j in Seg (width N2) by A17, Def11;
then A67: j <= width N by A17, FINSEQ_1:3;
j in Seg (len ((ColSum N2) + (Line (N,((k + 1) + 1))))) by A37, A64, A65, FINSEQ_1:3;
then j in dom ((ColSum N2) + (Line (N,((k + 1) + 1)))) by FINSEQ_1:def 3;
then ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = ((ColSum N2) . j) + ((Line (N,((k + 1) + 1))) . j) by COMPLSP2:1
.= ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) by A17, A66, MATRIX_1:def 8
.= (ColSum N) . j by A42, A64, A67 ;
hence ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j ; :: thesis: verum
end;
len (LineSum N) = len N by Def10;
then Sum (LineSum N) = (Sum (LineSum N2)) + ((LineSum N) /. ((k + 1) + 1)) by A8, A18, A19, Th51, FINSEQ_1:18
.= (Sum (LineSum N2)) + ((LineSum N) . ((k + 1) + 1)) by A40, PARTFUN1:def 8
.= (Sum (ColSum N2)) + ((LineSum N) . ((k + 1) + 1)) by A3, A9
.= (Sum (ColSum N2)) + (Sum (Line (N,((k + 1) + 1)))) by A39, Def10
.= Sum ((ColSum N2) + (Line (N,((k + 1) + 1)))) by A38, Th37
.= Sum (ColSum N) by A37, A63, FINSEQ_1:18 ;
hence Sum (LineSum N) = Sum (ColSum N) ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
for N being Matrix of COMPLEX st 0 + 1 = len N holds
Sum (LineSum N) = Sum (ColSum N)
proof
let N be Matrix of COMPLEX; :: thesis: ( 0 + 1 = len N implies Sum (LineSum N) = Sum (ColSum N) )
A68: len (Line (N,1)) = width N by MATRIX_1:def 8;
assume A69: 0 + 1 = len N ; :: thesis: Sum (LineSum N) = Sum (ColSum N)
then A70: 1 in Seg (len N) by FINSEQ_1:5;
A71: 1 in Seg 1 by FINSEQ_1:5;
A72: for j being Nat st 1 <= j & j <= width N holds
(ColSum N) . j = (Line (N,1)) . j
proof
A73: 1 in dom N by A69, A71, FINSEQ_1:def 3;
let j be Nat; :: thesis: ( 1 <= j & j <= width N implies (ColSum N) . j = (Line (N,1)) . j )
assume that
A74: 1 <= j and
A75: j <= width N ; :: thesis: (ColSum N) . j = (Line (N,1)) . j
A76: len (Col (N,j)) = 1 by A69, MATRIX_1:def 9;
A77: j in Seg (width N) by A74, A75, FINSEQ_1:3;
then (ColSum N) . j = Sum (Col (N,j)) by Def11
.= (Col (N,j)) . 1 by A76, Th50
.= N * (1,j) by A73, MATRIX_1:def 9
.= (Line (N,1)) . j by A77, MATRIX_1:def 8 ;
hence (ColSum N) . j = (Line (N,1)) . j ; :: thesis: verum
end;
A78: len (LineSum N) = 1 by A69, Def10;
len (ColSum N) = width N by Def11;
then Sum (ColSum N) = Sum (Line (N,1)) by A68, A72, FINSEQ_1:18
.= (LineSum N) . 1 by A70, Def10
.= Sum (LineSum N) by A78, Th50 ;
hence Sum (LineSum N) = Sum (ColSum N) ; :: thesis: verum
end;
then A79: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch 2(A79, A2);
 then ( ((len M) -' 1) + 1 = len M implies Sum (LineSum M) = Sum (ColSum M) ) ;
hence Sum (LineSum M) = Sum (ColSum M) by A1; :: thesis: verum