Theorem dstrvval

Description: The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017)

	Ref	Expression
Hypotheses	dstrvprob.1	|- ( ph -> P e. Prob )
	dstrvprob.2	|- ( ph -> X e. ( rRndVar ` P ) )
	dstrvprob.3	|- ( ph -> D = ( a e. BrSiga |-> ( P ` ( X oRVC _E a ) ) ) )
	dstrvval.1	|- ( ph -> A e. BrSiga )
Assertion	dstrvval	|- ( ph -> ( D ` A ) = ( P ` ( `' X " A ) ) )

Proof

Step	Hyp	Ref	Expression
1		dstrvprob.1	|- ( ph -> P e. Prob )
2		dstrvprob.2	|- ( ph -> X e. ( rRndVar ` P ) )
3		dstrvprob.3	|- ( ph -> D = ( a e. BrSiga |-> ( P ` ( X oRVC _E a ) ) ) )
4		dstrvval.1	|- ( ph -> A e. BrSiga )
5	3	fveq1d	|- ( ph -> ( D ` A ) = ( ( a e. BrSiga |-> ( P ` ( X oRVC _E a ) ) ) ` A ) )
6		oveq2	|- ( a = A -> ( X oRVC _E a ) = ( X oRVC _E A ) )
7	6	fveq2d	|- ( a = A -> ( P ` ( X oRVC _E a ) ) = ( P ` ( X oRVC _E A ) ) )
8		eqid	|- ( a e. BrSiga |-> ( P ` ( X oRVC _E a ) ) ) = ( a e. BrSiga |-> ( P ` ( X oRVC _E a ) ) )
9		fvex	|- ( P ` ( X oRVC _E A ) ) e. _V
10	7 8 9	fvmpt	|- ( A e. BrSiga -> ( ( a e. BrSiga |-> ( P ` ( X oRVC _E a ) ) ) ` A ) = ( P ` ( X oRVC _E A ) ) )
11	4 10	syl	|- ( ph -> ( ( a e. BrSiga |-> ( P ` ( X oRVC _E a ) ) ) ` A ) = ( P ` ( X oRVC _E A ) ) )
12	1 2 4	orvcelval	|- ( ph -> ( X oRVC _E A ) = ( `' X " A ) )
13	12	fveq2d	|- ( ph -> ( P ` ( X oRVC _E A ) ) = ( P ` ( `' X " A ) ) )
14	5 11 13	3eqtrd	|- ( ph -> ( D ` A ) = ( P ` ( `' X " A ) ) )