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_1:def 3;
then
width <*(<*> the carrier of V1)*> = 0
by MATRIX_1:20;
then A2:
len (<*(<*> the carrier of V1)*> @ ) = 0
by MATRIX_1:def 7;
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:55
.=
(Seg 1) /\ (Seg 1)
by FINSEQ_1:55
.=
Seg 1
;
then A5:
len (<*P*> ^^ <*<*x*>*>) =
1
by FINSEQ_1:8
.=
len <*(P ^ <*x*>)*>
by FINSEQ_1:56
;
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:57;
then A13:
width <*<*x*>*> =
len <*x*>
by MATRIX_1:20
.=
1
by FINSEQ_1:57
;
then A14:
len (<*<*x*>*> @ ) = 1
by MATRIX_1:def 7;
A15:
len <*P*> = 1
by FINSEQ_1:57;
then A16:
width <*P*> = len P
by MATRIX_1:20;
then A17:
len (<*P*> @ ) = len P
by MATRIX_1:def 7;
width (<*P*> @ ) = 1
by A11, A15, A16, MATRIX_2:12;
then reconsider d1 =
<*P*> @ as
Matrix of
len P,1,the
carrier of
V1 by A11, A17, MATRIX_1:20;
A18:
len <*(P ^ <*x*>)*> = 1
by FINSEQ_1:57;
then A19:
width <*(P ^ <*x*>)*> =
len (P ^ <*x*>)
by MATRIX_1:20
.=
(len P) + (len <*x*>)
by FINSEQ_1:35
.=
(len P) + 1
by FINSEQ_1:57
;
A20:
(<*<*x*>*> @ ) @ = <*<*x*>*>
by A12, A13, MATRIX_2:15;
A21:
width (<*P*> @ ) =
len <*P*>
by A11, A16, MATRIX_2:12
.=
width (<*<*x*>*> @ )
by A15, A12, A13, MATRIX_2:12
;
then
width (<*<*x*>*> @ ) = 1
by A11, A15, A16, MATRIX_2:12;
then reconsider d2 =
<*<*x*>*> @ as
Matrix of 1,1,the
carrier of
V1 by A14, MATRIX_1:20;
A22:
(d1 ^ d2) @ =
((<*P*> @ ) @ ) ^^ ((<*<*x*>*> @ ) @ )
by A21, Th32
.=
<*P*> ^^ <*<*x*>*>
by A11, A15, A16, A20, MATRIX_2:15
.=
<*(P ^ <*x*>)*>
by A5, A7, FINSEQ_2:10
.=
(<*(P ^ <*x*>)*> @ ) @
by A18, A19, MATRIX_2:15
;
A23:
len ((<*P*> @ ) ^ (<*<*x*>*> @ )) =
(len (<*P*> @ )) + (len (<*<*x*>*> @ ))
by FINSEQ_1:35
.=
(width <*P*>) + (len (<*<*x*>*> @ ))
by MATRIX_1:def 7
.=
(width <*P*>) + (width <*<*x*>*>)
by MATRIX_1:def 7
.=
len (<*(P ^ <*x*>)*> @ )
by A16, A13, A19, MATRIX_1:def 7
;
thus Sum (Sum <*(P ^ <*x*>)*>) =
Sum (Sum (<*P*> ^^ <*<*x*>*>))
by A5, A7, FINSEQ_2:10
.=
(Sum (Sum (<*P*> @ ))) + (Sum (Sum <*<*x*>*>))
by A4, A15, A12, Th35
.=
(Sum (Sum (<*P*> @ ))) + (Sum (Sum (<*<*x*>*> @ )))
by Th19
.=
Sum ((Sum d1) ^ (Sum d2))
by RLVECT_1:58
.=
Sum (Sum (d1 ^ d2))
by Th31
.=
Sum (Sum (<*(P ^ <*x*>)*> @ ))
by A23, A22, MATRIX_2:11
;
verum 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 Th18
.=
Sum (Sum (<*(<*> the carrier of V1)*> @ ))
by A2, Th17
;
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 @ ))
A27:
M <> {}
by a27;
A28:
dom M = Seg (len M)
by FINSEQ_1:def 3;
per cases
( n = 0 or n > 0 )
;
suppose A30:
n > 0
;
Sum (Sum M) = Sum (Sum (M @ ))A31:
M . (n + 1) = Line M,
(n + 1)
by a27, A28, FINSEQ_1:6, MATRIX_2:18;
then reconsider M1 =
M . (n + 1) as
FinSequence of
V1 ;
reconsider R =
<*M1*> as
Matrix of 1,
width M,the
carrier of
V1 by A31, MATRIX_1:def 8;
reconsider M9 =
M as
Matrix of
n + 1,
width M,the
carrier of
V1 by a27, MATRIX_1:20;
reconsider W =
Del M9,
(n + 1) as
Matrix of
n,
width M,the
carrier of
V1 by Th5;
A32:
width W =
width M9
by A30, Th4
.=
width R
by Th4
;
A33:
len (W @ ) =
width W
by MATRIX_1:def 7
.=
len (R @ )
by A32, MATRIX_1:def 7
;
A34:
len (Del M,(n + 1)) = n
by a27, Th3;
thus Sum (Sum M) =
Sum (Sum (W ^ R))
by A27, Th6, a27
.=
Sum ((Sum W) ^ (Sum R))
by Th31
.=
(Sum (Sum (Del M,(n + 1)))) + (Sum (Sum R))
by RLVECT_1:58
.=
(Sum (Sum ((Del M,(n + 1)) @ ))) + (Sum (Sum R))
by A26, A34
.=
(Sum (Sum ((Del M,(n + 1)) @ ))) + (Sum (Sum (R @ )))
by A1
.=
Sum (Sum ((W @ ) ^^ (R @ )))
by A33, Th35
.=
Sum (Sum ((W ^ R) @ ))
by A32, Th32
.=
Sum (Sum (M @ ))
by A27, Th6, a27
;
verum end;
end;
end;
A35:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A35, A25);
then
S1[ len M]
;
hence
Sum (Sum M) = Sum (Sum (M @ ))
; verum