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
object st
x in rng N holds
ex
p being
FinSequence of
COMPLEX st
(
x = p &
len p = n )
by MATRIX_0:9;
A5:
rng (N | k1) c= rng N
by FINSEQ_5:19;
then
for
x being
object 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_0:9;
set g1 =
LineSum N2;
consider n3 being
Nat such that A6:
for
x2 being
object st
x2 in rng N holds
ex
s being
FinSequence st
(
s = x2 &
len s = n3 )
by MATRIX_0:def 1;
set f3 =
LineSum N;
A7:
len (Line (N,((k + 1) + 1))) = width N
by MATRIX_0: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 Def9
.=
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 A12:
len N2 > 0
;
1
in Seg (len N2)
by A11, FINSEQ_1:1;
then
1
in dom N2
by FINSEQ_1:def 3;
then A13:
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 A14:
width N2 = n3
by A13, A12, MATRIX_0:def 3;
A15:
len N >= 1
by A8, NAT_1:11;
then A16:
len N > 0
;
1
in Seg (len N)
by A15, FINSEQ_1:1;
then A17:
1
in dom N
by FINSEQ_1:def 3;
then A18:
N . 1
in rng N
by FUNCT_1:3;
A19:
ex
s2 being
FinSequence st
(
s2 = N . 1 &
len s2 = n3 )
by A6, A17, FUNCT_1:3;
then A20:
width N2 = width N
by A18, A14, A16, MATRIX_0:def 3;
len (LineSum N) = k1 + 1
by A8, Def9;
then A21:
len ((LineSum N) | k1) = len (LineSum N2)
by A10, FINSEQ_1:59, NAT_1:11;
A22:
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 A23:
1
<= n
and A24:
n <= len ((LineSum N) | k1)
;
((LineSum N) | k1) . n = (LineSum N2) . n
A25:
n <= k1 + 1
by A10, A21, A24, NAT_1:13;
then A26:
n in Seg (len N)
by A8, A23, FINSEQ_1:1;
A27:
for
n1 being
Nat st 1
<= n1 &
n1 <= len (Line (N,n)) holds
(Line (N,n)) . n1 = (Line (N2,n)) . n1
proof
A28:
N2 . n = N . n
by A10, A21, A24, FINSEQ_3:112;
A29:
n <= len N2
by A21, A24, Def9;
let n1 be
Nat;
( 1 <= n1 & n1 <= len (Line (N,n)) implies (Line (N,n)) . n1 = (Line (N2,n)) . n1 )
assume that A30:
1
<= n1
and A31:
n1 <= len (Line (N,n))
;
(Line (N,n)) . n1 = (Line (N2,n)) . n1
A32:
n1 in Seg (len (Line (N,n)))
by A30, A31, FINSEQ_1:1;
then A33:
n1 in Seg (width N2)
by A20, MATRIX_0:def 7;
A34:
n1 in Seg (width N)
by A32, MATRIX_0:def 7;
then
n1 <= width N
by FINSEQ_1:1;
then
[n,n1] in Indices N
by A8, A23, A25, A30, Th1;
then A35:
ex
pn being
FinSequence of
COMPLEX st
(
pn = N . n &
N * (
n,
n1)
= pn . n1 )
by MATRIX_0:def 5;
n1 <= width N
by A34, FINSEQ_1:1;
then
n1 <= width N2
by A8, A18, A19, A14, MATRIX_0:def 3;
then A36:
[n,n1] in Indices N2
by A23, A30, A29, Th1;
n1 in Seg (width N)
by A32, MATRIX_0:def 7;
then (Line (N,n)) . n1 =
N * (
n,
n1)
by MATRIX_0:def 7
.=
N2 * (
n,
n1)
by A36, A35, A28, MATRIX_0:def 5
.=
(Line (N2,n)) . n1
by A33, MATRIX_0:def 7
;
hence
(Line (N,n)) . n1 = (Line (N2,n)) . n1
;
verum
end;
len (Line (N,n)) =
width N
by MATRIX_0:def 7
.=
width N2
by A8, A18, A19, A14, MATRIX_0:def 3
.=
len (Line (N2,n))
by MATRIX_0:def 7
;
then A37:
Line (
N,
n)
= Line (
N2,
n)
by A27, FINSEQ_1:14;
n in Seg (len ((LineSum N) | k1))
by A23, A24, FINSEQ_1:1;
then
n in dom ((LineSum N) | k1)
by FINSEQ_1:def 3;
then A38:
n in dom ((LineSum N) | (Seg k1))
by FINSEQ_1:def 15;
n in Seg k1
by A10, A21, A23, A24, FINSEQ_1:1;
then A39:
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 A38, FUNCT_1:47
.=
Sum (Line (N2,n))
by A26, A37, Def9
.=
(LineSum N2) . n
by A39, Def9
;
hence
((LineSum N) | k1) . n = (LineSum N2) . n
;
verum
end;
len (ColSum N2) = width N2
by Def10;
then A40:
len ((ColSum N2) + (Line (N,((k + 1) + 1)))) =
width N
by A20, A7, COMPLSP2:6
.=
len (ColSum N)
by Def10
;
A41:
len (ColSum N2) =
width N2
by Def10
.=
width N
by A8, A18, A19, A14, MATRIX_0:def 3
.=
len (Line (N,((k + 1) + 1)))
by MATRIX_0:def 7
;
A42:
(k + 1) + 1
in Seg (len N)
by A8, FINSEQ_1:3;
then
(k + 1) + 1
in Seg (len (LineSum N))
by Def9;
then A43:
(k + 1) + 1
in dom (LineSum N)
by FINSEQ_1:def 3;
A44:
len N >= k + 1
by A8, NAT_1:11;
A45:
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 A46:
1
<= j
and A47:
j <= width N
;
((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j
set g =
Col (
N2,
j);
set f =
Col (
N,
j);
A48:
k1 <= len (Col (N,j))
by A44, MATRIX_0:def 8;
A49:
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 A50:
1
<= n
and A51:
n <= len ((Col (N,j)) | k1)
;
((Col (N,j)) | k1) . n = (Col (N2,j)) . n
A52:
n <= k1
by A48, A51, FINSEQ_1:59;
then A53:
N2 . n = N . n
by FINSEQ_3:112;
n <= k1 + 1
by A52, NAT_1:13;
then
n in Seg (len N)
by A8, A50, FINSEQ_1:1;
then A54:
n in dom N
by FINSEQ_1:def 3;
n <= len N
by A8, A52, NAT_1:13;
then
[n,j] in Indices N
by A46, A47, A50, Th1;
then A55:
ex
pn being
FinSequence of
COMPLEX st
(
pn = N . n &
N * (
n,
j)
= pn . j )
by MATRIX_0:def 5;
A56:
j <= width N2
by A8, A18, A19, A14, A47, MATRIX_0:def 3;
n in Seg k1
by A50, A52, FINSEQ_1:1;
then A57:
n in dom N2
by A9, FINSEQ_1:def 3;
n in Seg (len ((Col (N,j)) | k1))
by A50, A51, FINSEQ_1:1;
then
n in dom ((Col (N,j)) | k1)
by FINSEQ_1:def 3;
then A58:
n in dom ((Col (N,j)) | (Seg k1))
by FINSEQ_1:def 15;
n <= len N2
by A9, A48, A51, FINSEQ_1:59;
then A59:
[n,j] in Indices N2
by A46, A50, A56, Th1;
((Col (N,j)) | k1) . n =
((Col (N,j)) | (Seg k1)) . n
by FINSEQ_1:def 15
.=
(Col (N,j)) . n
by A58, FUNCT_1:47
.=
N * (
n,
j)
by A54, MATRIX_0:def 8
.=
N2 * (
n,
j)
by A59, A55, A53, MATRIX_0:def 5
.=
(Col (N2,j)) . n
by A57, MATRIX_0:def 8
;
hence
((Col (N,j)) | k1) . n = (Col (N2,j)) . n
;
verum
end;
A60:
(k + 1) + 1
in Seg (len N)
by A8, FINSEQ_1:4;
then A61:
(k + 1) + 1
in dom N
by FINSEQ_1:def 3;
len (Col (N2,j)) =
len N2
by MATRIX_0:def 8
.=
k1
by A8, FINSEQ_1:59, NAT_1:11
;
then A62:
Col (
N2,
j)
= (Col (N,j)) | k1
by A48, A49, FINSEQ_1:14, FINSEQ_1:59;
A63:
len (Col (N,j)) = len N
by MATRIX_0:def 8;
(k + 1) + 1
in Seg (len (Col (N,j)))
by A60, MATRIX_0:def 8;
then A64:
(k + 1) + 1
in dom (Col (N,j))
by FINSEQ_1:def 3;
A65:
j in Seg (width N)
by A46, A47, FINSEQ_1:1;
then ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) =
(Sum (Col (N2,j))) + (N * (((k + 1) + 1),j))
by A20, Def10
.=
(Sum (Col (N2,j))) + ((Col (N,j)) . ((k + 1) + 1))
by A61, MATRIX_0:def 8
.=
(Sum (Col (N2,j))) + ((Col (N,j)) /. ((k + 1) + 1))
by A64, PARTFUN1:def 6
.=
Sum (Col (N,j))
by A8, A63, A62, Th46
.=
(ColSum N) . j
by A65, Def10
;
hence
((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j
;
verum
end;
A66:
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 A67:
1
<= j
and A68:
j <= len (ColSum N)
;
((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j
j in Seg (len (ColSum N))
by A67, A68, FINSEQ_1:1;
then A69:
j in Seg (width N2)
by A20, Def10;
then A70:
j <= width N
by A20, FINSEQ_1:1;
j in Seg (len ((ColSum N2) + (Line (N,((k + 1) + 1)))))
by A40, A67, A68, 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 A20, A69, MATRIX_0:def 7
.=
(ColSum N) . j
by A45, A67, A70
;
hence
((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j
;
verum
end;
len (LineSum N) = len N
by Def9;
then Sum (LineSum N) =
(Sum (LineSum N2)) + ((LineSum N) /. ((k + 1) + 1))
by A8, A21, A22, Th46, FINSEQ_1:14
.=
(Sum (LineSum N2)) + ((LineSum N) . ((k + 1) + 1))
by A43, PARTFUN1:def 6
.=
(Sum (ColSum N2)) + ((LineSum N) . ((k + 1) + 1))
by A3, A9
.=
(Sum (ColSum N2)) + (Sum (Line (N,((k + 1) + 1))))
by A42, Def9
.=
Sum ((ColSum N2) + (Line (N,((k + 1) + 1))))
by A41, Th34
.=
Sum (ColSum N)
by A40, A66, 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) )
A71:
len (Line (N,1)) = width N
by MATRIX_0:def 7;
assume A72:
0 + 1
= len N
;
Sum (LineSum N) = Sum (ColSum N)
then A73:
1
in Seg (len N)
by FINSEQ_1:3;
A74:
1
in Seg 1
by FINSEQ_1:3;
A75:
for
j being
Nat st 1
<= j &
j <= width N holds
(ColSum N) . j = (Line (N,1)) . j
proof
A76:
1
in dom N
by A72, A74, FINSEQ_1:def 3;
let j be
Nat;
( 1 <= j & j <= width N implies (ColSum N) . j = (Line (N,1)) . j )
assume that A77:
1
<= j
and A78:
j <= width N
;
(ColSum N) . j = (Line (N,1)) . j
A79:
len (Col (N,j)) = 1
by A72, MATRIX_0:def 8;
A80:
j in Seg (width N)
by A77, A78, FINSEQ_1:1;
then (ColSum N) . j =
Sum (Col (N,j))
by Def10
.=
(Col (N,j)) . 1
by A79, Th45
.=
N * (1,
j)
by A76, MATRIX_0:def 8
.=
(Line (N,1)) . j
by A80, MATRIX_0:def 7
;
hence
(ColSum N) . j = (Line (N,1)) . j
;
verum
end;
A81:
len (LineSum N) = 1
by A72, Def9;
len (ColSum N) = width N
by Def10;
then Sum (ColSum N) =
Sum (Line (N,1))
by A71, A75, FINSEQ_1:14
.=
(LineSum N) . 1
by A73, Def9
.=
Sum (LineSum N)
by A81, Th45
;
hence
Sum (LineSum N) = Sum (ColSum N)
;
verum
end;
then A82:
S1[ 0 ]
;
for i being Nat holds S1[i]
from NAT_1:sch 2(A82, 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