let K be Field; :: thesis: 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; :: thesis: for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @ ))
A1:
for P being FinSequence of V1 holds Sum (Sum <*P*>) = Sum (Sum (<*P*> @ ))
proof
let P be
FinSequence of
V1;
:: thesis: Sum (Sum <*P*>) = Sum (Sum (<*P*> @ ))
defpred S1[
FinSequence of
V1]
means Sum (Sum <*$1*>) = Sum (Sum (<*$1*> @ ));
A2:
S1[
<*> the
carrier of
V1]
A5:
for
P being
FinSequence of
V1 for
x being
Element of
V1 st
S1[
P] holds
S1[
P ^ <*x*>]
proof
let P be
FinSequence of
V1;
:: thesis: for x being Element of V1 st S1[P] holds
S1[P ^ <*x*>]let x be
Element of
V1;
:: thesis: ( S1[P] implies S1[P ^ <*x*>] )
assume A6:
Sum (Sum <*P*>) = Sum (Sum (<*P*> @ ))
;
:: thesis: S1[P ^ <*x*>]
Seg (len (<*P*> ^^ <*<*x*>*>)) =
dom (<*P*> ^^ <*<*x*>*>)
by FINSEQ_1:def 3
.=
(dom <*P*>) /\ (dom <*<*x*>*>)
by Def2
.=
(Seg 1) /\ (dom <*<*x*>*>)
by FINSEQ_1:55
.=
(Seg 1) /\ (Seg 1)
by FINSEQ_1:55
.=
Seg 1
;
then A7:
len (<*P*> ^^ <*<*x*>*>) =
1
by FINSEQ_1:8
.=
len <*(P ^ <*x*>)*>
by FINSEQ_1:56
;
X:
dom (<*P*> ^^ <*<*x*>*>) = Seg (len <*(P ^ <*x*>)*>)
by A7, FINSEQ_1:def 3;
A8:
now let i be
Nat;
:: thesis: ( i in dom (<*P*> ^^ <*<*x*>*>) implies (<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i )assume A9:
i in dom (<*P*> ^^ <*<*x*>*>)
;
:: thesis: (<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . ithen A10:
i in dom (<*P*> ^^ <*<*x*>*>)
;
A11:
i in Seg 1
by A9, X, FINSEQ_1:57;
i in {1}
by A9, X, FINSEQ_1:4, FINSEQ_1:57;
then A12:
i = 1
by TARSKI:def 1;
(
i in dom <*P*> &
i in dom <*<*x*>*> )
by A11, FINSEQ_1:55;
then reconsider m1 =
<*P*> . i,
m2 =
<*<*x*>*> . i as
FinSequence by Def1;
thus (<*P*> ^^ <*<*x*>*>) . i =
m1 ^ m2
by A10, Def2
.=
P ^ m2
by A12, FINSEQ_1:57
.=
P ^ <*x*>
by A12, FINSEQ_1:57
.=
<*(P ^ <*x*>)*> . i
by A12, FINSEQ_1:57
;
:: thesis: verum end;
per cases
( len P = 0 or len P <> 0 )
;
suppose
len P <> 0
;
:: thesis: S1[P ^ <*x*>]then A14:
len P > 0
;
A15:
len <*P*> = 1
by FINSEQ_1:57;
then A16:
width <*P*> = len P
by MATRIX_1:20;
A17:
len <*<*x*>*> = 1
by FINSEQ_1:57;
then A18:
width <*<*x*>*> =
len <*x*>
by MATRIX_1:20
.=
1
by FINSEQ_1:57
;
A19:
len <*(P ^ <*x*>)*> = 1
by FINSEQ_1:57;
then A20:
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
;
A21:
width (<*P*> @ ) =
len <*P*>
by A14, A16, MATRIX_2:12
.=
width (<*<*x*>*> @ )
by A15, A17, A18, MATRIX_2:12
;
A22:
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, A18, A20, MATRIX_1:def 7
;
A23:
len (<*P*> @ ) = len P
by A16, MATRIX_1:def 7;
width (<*P*> @ ) = 1
by A14, A15, A16, MATRIX_2:12;
then reconsider d1 =
<*P*> @ as
Matrix of
len P,1,the
carrier of
V1 by A14, A23, MATRIX_1:20;
A24:
len (<*<*x*>*> @ ) = 1
by A18, MATRIX_1:def 7;
width (<*<*x*>*> @ ) = 1
by A14, A15, A16, A21, MATRIX_2:12;
then reconsider d2 =
<*<*x*>*> @ as
Matrix of 1,1,the
carrier of
V1 by A24, MATRIX_1:20;
A25:
(<*<*x*>*> @ ) @ = <*<*x*>*>
by A17, A18, MATRIX_2:15;
A26:
(d1 ^ d2) @ =
((<*P*> @ ) @ ) ^^ ((<*<*x*>*> @ ) @ )
by A21, Th32
.=
<*P*> ^^ <*<*x*>*>
by A14, A15, A16, A25, MATRIX_2:15
.=
<*(P ^ <*x*>)*>
by A7, A8, FINSEQ_2:10
.=
(<*(P ^ <*x*>)*> @ ) @
by A19, A20, MATRIX_2:15
;
thus Sum (Sum <*(P ^ <*x*>)*>) =
Sum (Sum (<*P*> ^^ <*<*x*>*>))
by A7, A8, FINSEQ_2:10
.=
(Sum (Sum (<*P*> @ ))) + (Sum (Sum <*<*x*>*>))
by A6, A15, A17, 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 A22, A26, MATRIX_2:11
;
:: thesis: verum end;
end;
for
P being
FinSequence of
V1 holds
S1[
P]
from FINSEQ_2:sch 2(A2, A5);
hence
Sum (Sum <*P*>) = Sum (Sum (<*P*> @ ))
;
:: thesis: verum
end;
defpred S1[ Nat] means for M being Matrix of the carrier of V1 st len M = $1 holds
Sum (Sum M) = Sum (Sum (M @ ));
A27:
S1[ 0 ]
A30:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A31:
for
M being
Matrix of the
carrier of
V1 st
len M = n holds
Sum (Sum M) = Sum (Sum (M @ ))
;
:: thesis: 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 @ ))
:: thesis: verumproof
let M be
Matrix of the
carrier of
V1;
:: thesis: ( len M = n + 1 implies Sum (Sum M) = Sum (Sum (M @ )) )
assume A32:
len M = n + 1
;
:: thesis: Sum (Sum M) = Sum (Sum (M @ ))
A33:
dom M = Seg (len M)
by FINSEQ_1:def 3;
per cases
( n = 0 or n > 0 )
;
suppose A35:
n > 0
;
:: thesis: Sum (Sum M) = Sum (Sum (M @ ))A36:
len (Del M,(n + 1)) = n
by A32, Th3;
A37:
M . (n + 1) = Line M,
(n + 1)
by A32, A33, FINSEQ_1:6, MATRIX_2:18;
then reconsider M1 =
M . (n + 1) as
FinSequence of
V1 ;
reconsider M' =
M as
Matrix of
n + 1,
width M,the
carrier of
V1 by A32, MATRIX_1:20;
reconsider R =
<*M1*> as
Matrix of 1,
width M,the
carrier of
V1 by A37, MATRIX_1:def 8;
reconsider W =
Del M',
(n + 1) as
Matrix of
n,
width M,the
carrier of
V1 by Th5;
A38:
width W =
width M'
by A35, Th4
.=
width R
by Th4
;
A39:
len (W @ ) =
width W
by MATRIX_1:def 7
.=
len (R @ )
by A38, MATRIX_1:def 7
;
thus Sum (Sum M) =
Sum (Sum (W ^ R))
by A32, Th6
.=
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 A31, A36
.=
(Sum (Sum ((Del M,(n + 1)) @ ))) + (Sum (Sum (R @ )))
by A1
.=
Sum (Sum ((W @ ) ^^ (R @ )))
by A39, Th35
.=
Sum (Sum ((W ^ R) @ ))
by A38, Th32
.=
Sum (Sum (M @ ))
by A32, Th6
;
:: thesis: verum end;
end;
end;
let M be Matrix of the carrier of V1; :: thesis: Sum (Sum M) = Sum (Sum (M @ ))
for n being Nat holds S1[n]
from NAT_1:sch 2(A27, A30);
then
S1[ len M]
;
hence
Sum (Sum M) = Sum (Sum (M @ ))
; :: thesis: verum