let M be Matrix of REAL; SumAll M = SumAll (M @)
defpred S1[ Nat] means for M being Matrix of REAL st len M = $1 holds
SumAll M = SumAll (M @);
A1:
for p being FinSequence of REAL holds SumAll <*p*> = SumAll (<*p*> @)
proof
defpred S2[
FinSequence of
REAL ]
means SumAll <*$1*> = SumAll (<*$1*> @);
let p be
FinSequence of
REAL ;
SumAll <*p*> = SumAll (<*p*> @)
A2:
for
p being
FinSequence of
REAL for
x being
Element of
REAL st
S2[
p] holds
S2[
p ^ <*x*>]
proof
let p be
FinSequence of
REAL ;
for x being Element of REAL st S2[p] holds
S2[p ^ <*x*>]let x be
Element of
REAL ;
( S2[p] implies S2[p ^ <*x*>] )
assume A3:
SumAll <*p*> = SumAll (<*p*> @)
;
S2[p ^ <*x*>]
Seg (len (<*p*> ^^ <*<*x*>*>)) =
dom (<*p*> ^^ <*<*x*>*>)
by FINSEQ_1:def 3
.=
(dom <*p*>) /\ (dom <*<*x*>*>)
by PRE_POLY:def 4
.=
(Seg 1) /\ (dom <*<*x*>*>)
by FINSEQ_1:38
.=
(Seg 1) /\ (Seg 1)
by FINSEQ_1:38
.=
Seg 1
;
then A4:
len (<*p*> ^^ <*<*x*>*>) =
1
by FINSEQ_1:6
.=
len <*(p ^ <*x*>)*>
by FINSEQ_1:39
;
A5:
dom <*(p ^ <*x*>)*> = Seg (len <*(p ^ <*x*>)*>)
by FINSEQ_1:def 3;
per cases
( len p = 0 or len p <> 0 )
;
suppose A10:
len p <> 0
;
S2[p ^ <*x*>]A11:
len <*<*x*>*> = 1
by FINSEQ_1:40;
then A12:
width <*<*x*>*> =
len <*x*>
by MATRIX_0:20
.=
1
by FINSEQ_1:40
;
then A13:
len (<*<*x*>*> @) = 1
by MATRIX_0:def 6;
A14:
len <*p*> = 1
by FINSEQ_1:40;
then A15:
width <*p*> = len p
by MATRIX_0:20;
then A16:
len (<*p*> @) = len p
by MATRIX_0:def 6;
width (<*p*> @) = 1
by A10, A14, A15, MATRIX_0:54;
then reconsider d1 =
<*p*> @ as
Matrix of
len p,1,
REAL by A10, A16, MATRIX_0:20;
len <*(p ^ <*x*>)*> = 1
by FINSEQ_1:40;
then A17:
width <*(p ^ <*x*>)*> =
len (p ^ <*x*>)
by MATRIX_0:20
.=
(len p) + (len <*x*>)
by FINSEQ_1:22
.=
(len p) + 1
by FINSEQ_1:40
;
A18:
(<*<*x*>*> @) @ = <*<*x*>*>
by A11, A12, MATRIX_0:57;
A19:
width (<*p*> @) =
len <*p*>
by A10, A15, MATRIX_0:54
.=
width (<*<*x*>*> @)
by A14, A11, A12, MATRIX_0:54
;
then
width (<*<*x*>*> @) = 1
by A10, A14, A15, MATRIX_0:54;
then reconsider d2 =
<*<*x*>*> @ as
Matrix of 1,1,
REAL by A13, MATRIX_0:20;
A20:
(d1 ^ d2) @ =
((<*p*> @) @) ^^ ((<*<*x*>*> @) @)
by A19, MATRLIN:28
.=
<*p*> ^^ <*<*x*>*>
by A10, A14, A15, A18, MATRIX_0:57
.=
<*(p ^ <*x*>)*>
by A4, A6, FINSEQ_2:9
.=
(<*(p ^ <*x*>)*> @) @
by A17, MATRIX_0:57
;
A21:
len ((<*p*> @) ^ (<*<*x*>*> @)) =
(len (<*p*> @)) + (len (<*<*x*>*> @))
by FINSEQ_1:22
.=
(width <*p*>) + (len (<*<*x*>*> @))
by MATRIX_0:def 6
.=
(width <*p*>) + (width <*<*x*>*>)
by MATRIX_0:def 6
.=
len (<*(p ^ <*x*>)*> @)
by A15, A12, A17, MATRIX_0:def 6
;
thus SumAll <*(p ^ <*x*>)*> =
SumAll (<*p*> ^^ <*<*x*>*>)
by A4, A6, FINSEQ_2:9
.=
(SumAll (<*p*> @)) + (SumAll <*<*x*>*>)
by A3, A14, A11, Th27
.=
(SumAll (<*p*> @)) + (SumAll (<*<*x*>*> @))
by MATRLIN:15
.=
Sum ((Sum d1) ^ (Sum d2))
by RVSUM_1:75
.=
SumAll (d1 ^ d2)
by Th25
.=
SumAll (<*(p ^ <*x*>)*> @)
by A21, A20, MATRIX_0:53
;
verum end; end;
end;
A22:
S2[
<*> REAL]
for
p being
FinSequence of
REAL holds
S2[
p]
from FINSEQ_2:sch 2(A22, A2);
hence
SumAll <*p*> = SumAll (<*p*> @)
;
verum
end;
A27:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A28:
for
M being
Matrix of
REAL st
len M = n holds
SumAll M = SumAll (M @)
;
S1[n + 1]
thus
for
M being
Matrix of
REAL st
len M = n + 1 holds
SumAll M = SumAll (M @)
verumproof
let M be
Matrix of
REAL;
( len M = n + 1 implies SumAll M = SumAll (M @) )
assume A29:
len M = n + 1
;
SumAll M = SumAll (M @)
a29:
M <> {}
by A29;
A30:
dom M = Seg (len M)
by FINSEQ_1:def 3;
per cases
( n = 0 or n > 0 )
;
suppose A32:
n > 0
;
SumAll M = SumAll (M @)reconsider M9 =
M as
Matrix of
n + 1,
width M,
REAL by A29, MATRIX_0:20;
reconsider M1 =
M . (n + 1) as
FinSequence of
REAL ;
reconsider w =
Del (
M9,
(n + 1)) as
Matrix of
n,
width M,
REAL by MATRLIN:3;
M . (n + 1) = Line (
M,
(n + 1))
by A29, A30, FINSEQ_1:4, MATRIX_0:60;
then
len M1 = width M
by MATRIX_0:def 7;
then reconsider r =
<*M1*> as
Matrix of 1,
width M,
REAL ;
A33:
width w =
width M9
by A32, MATRLIN:2
.=
width r
by MATRLIN:2
;
A34:
len (w @) =
width w
by MATRIX_0:def 6
.=
len (r @)
by A33, MATRIX_0:def 6
;
A35:
len (Del (M,(n + 1))) = n
by A29, PRE_POLY:12;
thus SumAll M =
SumAll (w ^ r)
by a29, A29, PRE_POLY:13
.=
Sum ((Sum w) ^ (Sum r))
by Th25
.=
(SumAll (Del (M,(n + 1)))) + (SumAll r)
by RVSUM_1:75
.=
(SumAll ((Del (M,(n + 1))) @)) + (SumAll r)
by A28, A35
.=
(SumAll ((Del (M,(n + 1))) @)) + (SumAll (r @))
by A1
.=
SumAll ((w @) ^^ (r @))
by A34, Th27
.=
SumAll ((w ^ r) @)
by A33, MATRLIN:28
.=
SumAll (M @)
by a29, PRE_POLY:13, A29
;
verum end; end;
end;
end;
A36:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A36, A27);
then
S1[ len M]
;
hence
SumAll M = SumAll (M @)
; verum