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 |
⊢ ( 𝜑 → ( 𝐷 ‘ 𝐴 ) = ( 𝑃 ‘ ( ◡ 𝑋 “ 𝐴 ) ) ) |