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