let K be Field; for V1 being finite-dimensional VectSp of K
for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))
let V1 be finite-dimensional VectSp of K; for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))
defpred S1[ Nat] means for M being Matrix of the carrier of V1 st len M = $1 holds
Sum (Sum M) = Sum (Sum (M @));
let M be Matrix of the carrier of V1; Sum (Sum M) = Sum (Sum (M @))
A1:
for P being FinSequence of V1 holds Sum (Sum <*P*>) = Sum (Sum (<*P*> @))
proof
defpred S2[
FinSequence of
V1]
means Sum (Sum <*$1*>) = Sum (Sum (<*$1*> @));
let P be
FinSequence of
V1;
Sum (Sum <*P*>) = Sum (Sum (<*P*> @))
len <*(<*> the carrier of V1)*> = 1
by MATRIX_0:def 2;
then
width <*(<*> the carrier of V1)*> = 0
by MATRIX_0:20;
then A2:
len (<*(<*> the carrier of V1)*> @) = 0
by MATRIX_0:def 6;
A3:
for
P being
FinSequence of
V1 for
x being
Element of
V1 st
S2[
P] holds
S2[
P ^ <*x*>]
proof
let P be
FinSequence of
V1;
for x being Element of V1 st S2[P] holds
S2[P ^ <*x*>]let x be
Element of
V1;
( S2[P] implies S2[P ^ <*x*>] )
assume A4:
Sum (Sum <*P*>) = Sum (Sum (<*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 A5:
len (<*P*> ^^ <*<*x*>*>) =
1
by FINSEQ_1:6
.=
len <*(P ^ <*x*>)*>
by FINSEQ_1:39
;
then A6:
dom (<*P*> ^^ <*<*x*>*>) = Seg (len <*(P ^ <*x*>)*>)
by FINSEQ_1:def 3;
per cases
( len P = 0 or len P <> 0 )
;
suppose A11:
len P <> 0
;
S2[P ^ <*x*>]A12:
len <*<*x*>*> = 1
by FINSEQ_1:40;
then A13:
width <*<*x*>*> =
len <*x*>
by MATRIX_0:20
.=
1
by FINSEQ_1:40
;
then A14:
len (<*<*x*>*> @) = 1
by MATRIX_0:def 6;
A15:
len <*P*> = 1
by FINSEQ_1:40;
then A16:
width <*P*> = len P
by MATRIX_0:20;
then A17:
len (<*P*> @) = len P
by MATRIX_0:def 6;
width (<*P*> @) = 1
by A11, A15, A16, MATRIX_0:54;
then reconsider d1 =
<*P*> @ as
Matrix of
len P,1, the
carrier of
V1 by A11, A17, MATRIX_0:20;
A18:
len <*(P ^ <*x*>)*> = 1
by FINSEQ_1:40;
then A19:
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
;
A20:
(<*<*x*>*> @) @ = <*<*x*>*>
by A12, A13, MATRIX_0:57;
A21:
width (<*P*> @) =
len <*P*>
by A11, A16, MATRIX_0:54
.=
width (<*<*x*>*> @)
by A15, A12, A13, MATRIX_0:54
;
then
width (<*<*x*>*> @) = 1
by A11, A15, A16, MATRIX_0:54;
then reconsider d2 =
<*<*x*>*> @ as
Matrix of 1,1, the
carrier of
V1 by A14, MATRIX_0:20;
A22:
(d1 ^ d2) @ =
((<*P*> @) @) ^^ ((<*<*x*>*> @) @)
by A21, Th28
.=
<*P*> ^^ <*<*x*>*>
by A11, A15, A16, A20, MATRIX_0:57
.=
<*(P ^ <*x*>)*>
by A5, A7, FINSEQ_2:9
.=
(<*(P ^ <*x*>)*> @) @
by A18, A19, MATRIX_0:57
;
A23:
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 A16, A13, A19, MATRIX_0:def 6
;
thus Sum (Sum <*(P ^ <*x*>)*>) =
Sum (Sum (<*P*> ^^ <*<*x*>*>))
by A5, A7, FINSEQ_2:9
.=
(Sum (Sum (<*P*> @))) + (Sum (Sum <*<*x*>*>))
by A4, A15, A12, Th31
.=
(Sum (Sum (<*P*> @))) + (Sum (Sum (<*<*x*>*> @)))
by Th15
.=
Sum ((Sum d1) ^ (Sum d2))
by RLVECT_1:41
.=
Sum (Sum (d1 ^ d2))
by Th27
.=
Sum (Sum (<*(P ^ <*x*>)*> @))
by A23, A22, MATRIX_0:53
;
verum end; end;
end;
<*(<*> the carrier of V1)*> is
Matrix of
0 + 1,
0 , the
carrier of
V1
;
then Sum (Sum <*(<*> the carrier of V1)*>) =
0. V1
by Th14
.=
Sum (Sum (<*(<*> the carrier of V1)*> @))
by A2, Th13
;
then A24:
S2[
<*> the
carrier of
V1]
;
for
P being
FinSequence of
V1 holds
S2[
P]
from FINSEQ_2:sch 2(A24, A3);
hence
Sum (Sum <*P*>) = Sum (Sum (<*P*> @))
;
verum
end;
A25:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A26:
for
M being
Matrix of the
carrier of
V1 st
len M = n holds
Sum (Sum M) = Sum (Sum (M @))
;
S1[n + 1]
thus
for
M being
Matrix of the
carrier of
V1 st
len M = n + 1 holds
Sum (Sum M) = Sum (Sum (M @))
verumproof
let M be
Matrix of the
carrier of
V1;
( len M = n + 1 implies Sum (Sum M) = Sum (Sum (M @)) )
assume A27:
len M = n + 1
;
Sum (Sum M) = Sum (Sum (M @))
A28:
M <> {}
by A27;
A29:
dom M = Seg (len M)
by FINSEQ_1:def 3;
per cases
( n = 0 or n > 0 )
;
suppose A31:
n > 0
;
Sum (Sum M) = Sum (Sum (M @))A32:
M . (n + 1) = Line (
M,
(n + 1))
by A27, A29, FINSEQ_1:4, MATRIX_0:60;
then reconsider M1 =
M . (n + 1) as
FinSequence of
V1 ;
len M1 = width M
by A32, MATRIX_0:def 7;
then reconsider R =
<*M1*> as
Matrix of 1,
width M, the
carrier of
V1 ;
reconsider M9 =
M as
Matrix of
n + 1,
width M, the
carrier of
V1 by A27, MATRIX_0:20;
reconsider W =
Del (
M9,
(n + 1)) as
Matrix of
n,
width M, the
carrier of
V1 by Th3;
A33:
width W =
width M9
by A31, Th2
.=
width R
by Th2
;
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 A27, Th1;
thus Sum (Sum M) =
Sum (Sum (W ^ R))
by A28, Th4, A27
.=
Sum ((Sum W) ^ (Sum R))
by Th27
.=
(Sum (Sum (Del (M,(n + 1))))) + (Sum (Sum R))
by RLVECT_1:41
.=
(Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum R))
by A26, A35
.=
(Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum (R @)))
by A1
.=
Sum (Sum ((W @) ^^ (R @)))
by A34, Th31
.=
Sum (Sum ((W ^ R) @))
by A33, Th28
.=
Sum (Sum (M @))
by A28, Th4, A27
;
verum end; end;
end;
end;
A36:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A36, A25);
then
S1[ len M]
;
hence
Sum (Sum M) = Sum (Sum (M @))
; verum