let p be ProbFinS FinSequence of REAL ; for M being V3() Conditional_Probability Matrix of REAL st len p = len M holds
(Vec2DiagMx p) * M is Joint_Probability
let M be V3() Conditional_Probability Matrix of REAL; ( len p = len M implies (Vec2DiagMx p) * M is Joint_Probability )
set M1 = (Vec2DiagMx p) * M;
assume A1:
len p = len M
; (Vec2DiagMx p) * M is Joint_Probability
then A2:
len ((Vec2DiagMx p) * M) = len p
by Th26;
A3:
LineSum ((Vec2DiagMx p) * M) = p
proof
set M2 =
LineSum ((Vec2DiagMx p) * M);
A4:
len (LineSum ((Vec2DiagMx p) * M)) = len ((Vec2DiagMx p) * M)
by MATRPROB:20;
then A5:
dom (LineSum ((Vec2DiagMx p) * M)) = dom M
by A1, A2, FINSEQ_3:29;
A6:
dom (LineSum ((Vec2DiagMx p) * M)) = dom ((Vec2DiagMx p) * M)
by A4, FINSEQ_3:29;
A7:
now for k being Nat st k in dom (LineSum ((Vec2DiagMx p) * M)) holds
(LineSum ((Vec2DiagMx p) * M)) . k = p . klet k be
Nat;
( k in dom (LineSum ((Vec2DiagMx p) * M)) implies (LineSum ((Vec2DiagMx p) * M)) . k = p . k )assume A8:
k in dom (LineSum ((Vec2DiagMx p) * M))
;
(LineSum ((Vec2DiagMx p) * M)) . k = p . k
k in Seg (len ((Vec2DiagMx p) * M))
by A4, A8, FINSEQ_1:def 3;
hence (LineSum ((Vec2DiagMx p) * M)) . k =
Sum (Line (((Vec2DiagMx p) * M),k))
by MATRPROB:20
.=
Sum ((p . k) * (Line (M,k)))
by A1, A6, A8, Th27
.=
(p . k) * (Sum (Line (M,k)))
by RVSUM_1:87
.=
(p . k) * (Sum (M . k))
by A5, A8, MATRIX_0:60
.=
(p . k) * 1
by A5, A8, MATRPROB:def 9
.=
p . k
;
verum end;
dom (LineSum ((Vec2DiagMx p) * M)) = dom p
by A2, A4, FINSEQ_3:29;
hence
LineSum ((Vec2DiagMx p) * M) = p
by A7, FINSEQ_1:13;
verum
end;
A9:
width ((Vec2DiagMx p) * M) = width M
by A1, Th26;
now for i, j being Nat st [i,j] in Indices ((Vec2DiagMx p) * M) holds
((Vec2DiagMx p) * M) * (i,j) >= 0 let i,
j be
Nat;
( [i,j] in Indices ((Vec2DiagMx p) * M) implies ((Vec2DiagMx p) * M) * (i,j) >= 0 )assume A10:
[i,j] in Indices ((Vec2DiagMx p) * M)
;
((Vec2DiagMx p) * M) * (i,j) >= 0 A11:
j in Seg (width M)
by A9, A10, MATRPROB:12;
i in Seg (len p)
by A2, A10, MATRPROB:12;
then
i in dom p
by FINSEQ_1:def 3;
then A12:
p . i >= 0
by MATRPROB:def 5;
i in Seg (len M)
by A1, A2, A10, MATRPROB:12;
then
[i,j] in Indices M
by A11, MATRPROB:12;
then A13:
M * (
i,
j)
>= 0
by MATRPROB:def 6;
((Vec2DiagMx p) * M) * (
i,
j)
= (p . i) * (M * (i,j))
by A1, A10, Th26;
hence
((Vec2DiagMx p) * M) * (
i,
j)
>= 0
by A12, A13;
verum end;
then A14:
(Vec2DiagMx p) * M is m-nonnegative
by MATRPROB:def 6;
SumAll ((Vec2DiagMx p) * M) =
Sum (LineSum ((Vec2DiagMx p) * M))
by MATRPROB:def 3
.=
1
by A3, MATRPROB:def 5
;
then
(Vec2DiagMx p) * M is with_sum=1
by MATRPROB:def 7;
hence
(Vec2DiagMx p) * M is Joint_Probability
by A14; verum