Theorem dstrvval

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

	Ref	Expression
Hypotheses	dstrvprob.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
	dstrvprob.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
	dstrvprob.3	⊢ ( 𝜑 → 𝐷 = ( 𝑎 ∈ 𝔅ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝑎 ) ) ) )
	dstrvval.1	⊢ ( 𝜑 → 𝐴 ∈ 𝔅ℝ )
Assertion	dstrvval	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐴 ) = ( 𝑃 ‘ ( ◡ 𝑋 “ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dstrvprob.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		dstrvprob.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		dstrvprob.3	⊢ ( 𝜑 → 𝐷 = ( 𝑎 ∈ 𝔅ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝑎 ) ) ) )
4		dstrvval.1	⊢ ( 𝜑 → 𝐴 ∈ 𝔅ℝ )
5	3	fveq1d	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐴 ) = ( ( 𝑎 ∈ 𝔅ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝑎 ) ) ) ‘ 𝐴 ) )
6		oveq2	⊢ ( 𝑎 = 𝐴 → ( 𝑋 ∘RV/𝑐 E 𝑎 ) = ( 𝑋 ∘RV/𝑐 E 𝐴 ) )
7	6	fveq2d	⊢ ( 𝑎 = 𝐴 → ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝑎 ) ) = ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝐴 ) ) )
8		eqid	⊢ ( 𝑎 ∈ 𝔅ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝑎 ) ) ) = ( 𝑎 ∈ 𝔅ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝑎 ) ) )
9		fvex	⊢ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝐴 ) ) ∈ V
10	7 8 9	fvmpt	⊢ ( 𝐴 ∈ 𝔅ℝ → ( ( 𝑎 ∈ 𝔅ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝑎 ) ) ) ‘ 𝐴 ) = ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝐴 ) ) )
11	4 10	syl	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝔅ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝑎 ) ) ) ‘ 𝐴 ) = ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝐴 ) ) )
12	1 2 4	orvcelval	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 E 𝐴 ) = ( ◡ 𝑋 “ 𝐴 ) )
13	12	fveq2d	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 E 𝐴 ) ) = ( 𝑃 ‘ ( ◡ 𝑋 “ 𝐴 ) ) )
14	5 11 13	3eqtrd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐴 ) = ( 𝑃 ‘ ( ◡ 𝑋 “ 𝐴 ) ) )