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; ( len M > 0 implies Sum (LineSum M) = Sum (ColSum M) )
assume
len M > 0
; 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:9;
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;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
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;
( (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:19;
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 7;
assume A8:
(k + 1) + 1
= len N
;
Sum (LineSum N) = Sum (ColSum N)
then A9:
len N2 = k + 1
by FINSEQ_1:59, NAT_1:11;
A10:
len (LineSum N2) =
len N2
by Def10
.=
k1
by A8, FINSEQ_1:59, NAT_1:11
;
1
+ k >= 1
by NAT_1:11;
then A11:
len N2 >= 1
by A8, FINSEQ_1:59, NAT_1:11;
then
1
in Seg (len N2)
by FINSEQ_1:1;
then
1
in dom N2
by FINSEQ_1:def 3;
then A12:
N2 . 1
in rng N2
by FUNCT_1:3;
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 3;
len N >= 1
by A8, NAT_1:11;
then
1
in Seg (len N)
by FINSEQ_1:1;
then A14:
1
in dom N
by FINSEQ_1:def 3;
then A15:
N . 1
in rng N
by FUNCT_1:3;
A16:
ex
s2 being
FinSequence st
(
s2 = N . 1 &
len s2 = n3 )
by A6, A14, FUNCT_1:3;
then A17:
width N2 = width N
by A8, A15, A13, MATRIX_1:def 3;
len (LineSum N) = k1 + 1
by A8, Def10;
then A18:
len ((LineSum N) | k1) = len (LineSum N2)
by A10, FINSEQ_1:59, 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;
( 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)
;
((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:1;
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:112;
A26:
n <= len N2
by A18, A21, Def10;
let n1 be
Nat;
( 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))
;
(Line (N,n)) . n1 = (Line (N2,n)) . n1
A29:
n1 in Seg (len (Line (N,n)))
by A27, A28, FINSEQ_1:1;
then A30:
n1 in Seg (width N2)
by A17, MATRIX_1:def 7;
A31:
n1 in Seg (width N)
by A29, MATRIX_1:def 7;
then
n1 <= width N
by FINSEQ_1:1;
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 5;
n1 <= width N
by A31, FINSEQ_1:1;
then
n1 <= width N2
by A8, A15, A16, A13, MATRIX_1:def 3;
then A33:
[n,n1] in Indices N2
by A20, A27, A26, Th1;
n1 in Seg (width N)
by A29, MATRIX_1:def 7;
then (Line (N,n)) . n1 =
N * (
n,
n1)
by MATRIX_1:def 7
.=
N2 * (
n,
n1)
by A33, A32, A25, MATRIX_1:def 5
.=
(Line (N2,n)) . n1
by A30, MATRIX_1:def 7
;
hence
(Line (N,n)) . n1 = (Line (N2,n)) . n1
;
verum
end;
len (Line (N,n)) =
width N
by MATRIX_1:def 7
.=
width N2
by A8, A15, A16, A13, MATRIX_1:def 3
.=
len (Line (N2,n))
by MATRIX_1:def 7
;
then A34:
Line (
N,
n)
= Line (
N2,
n)
by A24, FINSEQ_1:14;
n in Seg (len ((LineSum N) | k1))
by A20, A21, FINSEQ_1:1;
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:1;
then A36:
n in Seg (len N2)
by A8, FINSEQ_1:59, NAT_1:11;
((LineSum N) | k1) . n =
((LineSum N) | (Seg k1)) . n
by FINSEQ_1:def 15
.=
(LineSum N) . n
by A35, FUNCT_1:47
.=
Sum (Line (N2,n))
by A23, A34, Def10
.=
(LineSum N2) . n
by A36, Def10
;
hence
((LineSum N) | k1) . n = (LineSum N2) . n
;
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 3
.=
len (Line (N,((k + 1) + 1)))
by MATRIX_1:def 7
;
A39:
(k + 1) + 1
in Seg (len N)
by A8, FINSEQ_1:3;
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;
( 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
;
((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 8;
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;
( 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)
;
((Col (N,j)) | k1) . n = (Col (N2,j)) . n
A49:
n <= k1
by A45, A48, FINSEQ_1:59;
then A50:
N2 . n = N . n
by FINSEQ_3:112;
n <= k1 + 1
by A49, NAT_1:13;
then
n in Seg (len N)
by A8, A47, FINSEQ_1:1;
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 5;
A53:
j <= width N2
by A8, A15, A16, A13, A44, MATRIX_1:def 3;
n in Seg k1
by A47, A49, FINSEQ_1:1;
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:1;
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:59;
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:47
.=
N * (
n,
j)
by A51, MATRIX_1:def 8
.=
N2 * (
n,
j)
by A56, A52, A50, MATRIX_1:def 5
.=
(Col (N2,j)) . n
by A54, MATRIX_1:def 8
;
hence
((Col (N,j)) | k1) . n = (Col (N2,j)) . n
;
verum
end;
A57:
(k + 1) + 1
in Seg (len N)
by A8, FINSEQ_1:4;
then A58:
(k + 1) + 1
in dom N
by FINSEQ_1:def 3;
len (Col (N2,j)) =
len N2
by MATRIX_1:def 8
.=
k1
by A8, FINSEQ_1:59, NAT_1:11
;
then A59:
Col (
N2,
j)
= (Col (N,j)) | k1
by A45, A46, FINSEQ_1:14, FINSEQ_1:59;
A60:
len (Col (N,j)) = len N
by MATRIX_1:def 8;
(k + 1) + 1
in Seg (len (Col (N,j)))
by A57, MATRIX_1:def 8;
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:1;
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 8
.=
(Sum (Col (N2,j))) + ((Col (N,j)) /. ((k + 1) + 1))
by A61, PARTFUN1:def 6
.=
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
;
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;
( 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)
;
((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j
j in Seg (len (ColSum N))
by A64, A65, FINSEQ_1:1;
then A66:
j in Seg (width N2)
by A17, Def11;
then A67:
j <= width N
by A17, FINSEQ_1:1;
j in Seg (len ((ColSum N2) + (Line (N,((k + 1) + 1)))))
by A37, A64, A65, FINSEQ_1:1;
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 7
.=
(ColSum N) . j
by A42, A64, A67
;
hence
((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j
;
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:14
.=
(Sum (LineSum N2)) + ((LineSum N) . ((k + 1) + 1))
by A40, PARTFUN1:def 6
.=
(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:14
;
hence
Sum (LineSum N) = Sum (ColSum N)
;
verum
end;
hence
S1[
k + 1]
;
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;
( 0 + 1 = len N implies Sum (LineSum N) = Sum (ColSum N) )
A68:
len (Line (N,1)) = width N
by MATRIX_1:def 7;
assume A69:
0 + 1
= len N
;
Sum (LineSum N) = Sum (ColSum N)
then A70:
1
in Seg (len N)
by FINSEQ_1:3;
A71:
1
in Seg 1
by FINSEQ_1:3;
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;
( 1 <= j & j <= width N implies (ColSum N) . j = (Line (N,1)) . j )
assume that A74:
1
<= j
and A75:
j <= width N
;
(ColSum N) . j = (Line (N,1)) . j
A76:
len (Col (N,j)) = 1
by A69, MATRIX_1:def 8;
A77:
j in Seg (width N)
by A74, A75, FINSEQ_1:1;
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 8
.=
(Line (N,1)) . j
by A77, MATRIX_1:def 7
;
hence
(ColSum N) . j = (Line (N,1)) . j
;
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:14
.=
(LineSum N) . 1
by A70, Def10
.=
Sum (LineSum N)
by A78, Th50
;
hence
Sum (LineSum N) = Sum (ColSum N)
;
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; verum