let p, q be ProbFinS FinSequence of REAL ; :: thesis: for M being Matrix of REAL st M = (ColVec2Mx p) * (LineVec2Mx q) holds
SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
let M be Matrix of REAL ; :: thesis: ( M = (ColVec2Mx p) * (LineVec2Mx q) implies SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)) )
assume A1:
M = (ColVec2Mx p) * (LineVec2Mx q)
; :: thesis: SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
reconsider M = M as Joint_Probability Matrix of REAL by A1, Th23;
set M1 = Infor_FinSeq_of M;
set L = LineSum (Infor_FinSeq_of M);
A2:
( len M = len p & width M = len q )
by A1, Th22;
A3:
( len (Infor_FinSeq_of M) = len M & width (Infor_FinSeq_of M) = width M )
by Def8;
A4:
len (LineSum (Infor_FinSeq_of M)) = len (Infor_FinSeq_of M)
by MATRPROB:def 1;
then A5:
( dom (LineSum (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of M) & dom (Infor_FinSeq_of M) = dom M & dom M = dom p )
by A2, A3, FINSEQ_3:31;
( len (FinSeq_log 2,q) = len q & len (FinSeq_log 2,p) = len p )
by Def6;
then A6:
len (mlt q,(FinSeq_log 2,q)) = len q
by MATRPROB:30;
A7:
now let k be
Element of
NAT ;
:: thesis: ( k in dom (LineSum (Infor_FinSeq_of M)) implies (LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log 2,(p . k))) + ((p . k) * (Sum (Infor_FinSeq_of q))) )assume A8:
k in dom (LineSum (Infor_FinSeq_of M))
;
:: thesis: (LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log 2,(p . k))) + ((p . k) * (Sum (Infor_FinSeq_of q)))reconsider pp =
Line M,
k as
nonnegative FinSequence of
REAL by A5, A8, Th19;
A9:
pp = (p . k) * q
by A1, A5, A8, Th22;
A10:
p . k >= 0
by A5, A8, Def1;
dom (((p . k) * (log 2,(p . k))) * q) = dom q
by VALUED_1:def 5;
then A11:
len (((p . k) * (log 2,(p . k))) * q) = len q
by FINSEQ_3:31;
dom ((p . k) * (mlt q,(FinSeq_log 2,q))) = dom (mlt q,(FinSeq_log 2,q))
by VALUED_1:def 5;
then A12:
len (((p . k) * (log 2,(p . k))) * q) = len ((p . k) * (mlt q,(FinSeq_log 2,q)))
by A6, A11, FINSEQ_3:31;
thus (LineSum (Infor_FinSeq_of M)) . k =
Sum ((Infor_FinSeq_of M) . k)
by A8, MATRPROB:def 1
.=
Sum (Line (Infor_FinSeq_of M),k)
by A5, A8, MATRIX_2:18
.=
Sum (Infor_FinSeq_of pp)
by A5, A8, Th53
.=
Sum ((((p . k) * (log 2,(p . k))) * q) + ((p . k) * (mlt q,(FinSeq_log 2,q))))
by A9, A10, Th51
.=
(Sum (((p . k) * (log 2,(p . k))) * q)) + (Sum ((p . k) * (mlt q,(FinSeq_log 2,q))))
by A12, INTEGRA5:2
.=
(((p . k) * (log 2,(p . k))) * (Sum q)) + (Sum ((p . k) * (mlt q,(FinSeq_log 2,q))))
by RVSUM_1:117
.=
(((p . k) * (log 2,(p . k))) * 1) + (Sum ((p . k) * (mlt q,(FinSeq_log 2,q))))
by MATRPROB:def 5
.=
((p . k) * (log 2,(p . k))) + ((p . k) * (Sum (Infor_FinSeq_of q)))
by RVSUM_1:117
;
:: thesis: verum end;
set p1 = Infor_FinSeq_of p;
set p2 = (Sum (Infor_FinSeq_of q)) * p;
A13:
len (Infor_FinSeq_of p) = len p
by Th47;
dom ((Sum (Infor_FinSeq_of q)) * p) = dom p
by VALUED_1:def 5;
then A14:
( len (Infor_FinSeq_of p) = len (LineSum (Infor_FinSeq_of M)) & len (Infor_FinSeq_of p) = len ((Sum (Infor_FinSeq_of q)) * p) & dom (Infor_FinSeq_of p) = dom (LineSum (Infor_FinSeq_of M)) & dom (Infor_FinSeq_of p) = dom ((Sum (Infor_FinSeq_of q)) * p) )
by A2, A3, A4, A13, FINSEQ_3:31;
then Sum (LineSum (Infor_FinSeq_of M)) =
(Sum (Infor_FinSeq_of p)) + (Sum ((Sum (Infor_FinSeq_of q)) * p))
by A14, Th7
.=
(Sum (Infor_FinSeq_of p)) + ((Sum (Infor_FinSeq_of q)) * (Sum p))
by RVSUM_1:117
.=
(Sum (Infor_FinSeq_of p)) + ((Sum (Infor_FinSeq_of q)) * 1)
by MATRPROB:def 5
.=
(Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
;
hence
SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
by MATRPROB:def 3; :: thesis: verum