Definition df-orvc 32323

Description: Define the preimage set mapping operator. In probability theory, the notation 𝑃(𝑋 = 𝐴) denotes the probability that a random variable 𝑋 takes the value 𝐴. We introduce here an operator which enables to write this in Metamath as (𝑃‘(𝑋∘_RV/𝑐 I 𝐴)), and keep a similar notation. Because with this notation (𝑋∘_RV/𝑐 I 𝐴) is a set, we can also apply it to conditional probabilities, like in (𝑃‘(𝑋∘_RV/𝑐 I 𝐴) ∣ (𝑌∘_RV/𝑐 I 𝐵))).

The oRVC operator transforms a relation 𝑅 into an operation taking a random variable 𝑋 and a constant 𝐶, and returning the preimage through 𝑋 of the equivalence class of 𝐶.

The most commonly used relations are: - equality: {𝑋 = 𝐴} as (𝑋∘_RV/𝑐 I 𝐴) cf. ideq 5750- elementhood: {𝑋 ∈ 𝐴} as (𝑋∘_RV/𝑐 E 𝐴) cf. epel 5489- less-than: {𝑋 ≤ 𝐴} as (𝑋∘_RV/𝑐 ≤ 𝐴)

Even though it is primarily designed to be used within probability theory and with random variables, this operator is defined on generic functions, and could be used in other fields, e.g., for continuous functions. (Contributed by Thierry Arnoux, 15-Jan-2017.)

Assertion

Ref	Expression
df-orvc	⊢ ∘RV/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎}))

Distinct variable group:   𝑥,𝑎,𝑦,𝑅

Detailed syntax breakdown of Definition df-orvc

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	corvc 32322	. 2 class ∘RV/𝑐𝑅
3		vx	. . 3 setvar 𝑥
4		va	. . 3 setvar 𝑎
5	3	cv 1538	. . . . 5 class 𝑥
6	5	wfun 6412	. . . 4 wff Fun 𝑥
7	6, 3	cab 2715	. . 3 class {𝑥 ∣ Fun 𝑥}
8		cvv 3422	. . 3 class V
9	5	ccnv 5579	. . . 4 class ◡𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	10	cv 1538	. . . . . 6 class 𝑦
12	4	cv 1538	. . . . . 6 class 𝑎
13	11, 12, 1	wbr 5070	. . . . 5 wff 𝑦𝑅𝑎
14	13, 10	cab 2715	. . . 4 class {𝑦 ∣ 𝑦𝑅𝑎}
15	9, 14	cima 5583	. . 3 class (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎})
16	3, 4, 7, 8, 15	cmpo 7257	. 2 class (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎}))
17	2, 16	wceq 1539	1 wff ∘RV/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎}))

This definition is referenced by:  orvcval  32324