0rrv

Description: The constant function equal to zero is a random variable. (Contributed by Thierry Arnoux, 16-Jan-2017) (Revised by Thierry Arnoux, 30-Jan-2017)

		Ref	Expression
	Hypothesis	0rrv.1	$⊢ φ \to P \in Prob$
	Assertion	0rrv	$⊢ φ \to (x \in ⋃ dom P ⟼ 0) \in {RndVar}_{ℝ} (P)$

Proof

Step	Hyp	Ref	Expression
1		0rrv.1	$⊢ φ \to P \in Prob$
2		0re	$⊢ 0 \in ℝ$
3	2	rgenw	$⊢ \forall x \in ⋃ dom P 0 \in ℝ$
4		eqid	$⊢ (x \in ⋃ dom P ⟼ 0) = (x \in ⋃ dom P ⟼ 0)$
5	4	fmpt	$⊢ \forall x \in ⋃ dom P 0 \in ℝ \leftrightarrow (x \in ⋃ dom P ⟼ 0) : ⋃ dom P ⟶ ℝ$
6	3 5	mpbi	$⊢ (x \in ⋃ dom P ⟼ 0) : ⋃ dom P ⟶ ℝ$
7	6	a1i	$⊢ φ \to (x \in ⋃ dom P ⟼ 0) : ⋃ dom P ⟶ ℝ$
8		fconstmpt	$⊢ ⋃ dom P \times \{0\} = (x \in ⋃ dom P ⟼ 0)$
9	8	cnveqi	$⊢ {(⋃ dom P \times \{0\})}^{-1} = {(x \in ⋃ dom P ⟼ 0)}^{-1}$
10		cnvxp	$⊢ {(⋃ dom P \times \{0\})}^{-1} = \{0\} \times ⋃ dom P$
11	9 10	eqtr3i	$⊢ {(x \in ⋃ dom P ⟼ 0)}^{-1} = \{0\} \times ⋃ dom P$
12	11	imaeq1i	$⊢ {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] = (\{0\} \times ⋃ dom P) [y]$
13		df-ima	$⊢ (\{0\} \times ⋃ dom P) [y] = ran ({(\{0\} \times ⋃ dom P) ↾}_{y})$
14		df-rn	$⊢ ran ({(\{0\} \times ⋃ dom P) ↾}_{y}) = dom {({(\{0\} \times ⋃ dom P) ↾}_{y})}^{-1}$
15	12 13 14	3eqtri	$⊢ {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] = dom {({(\{0\} \times ⋃ dom P) ↾}_{y})}^{-1}$
16		xpres	$⊢ {(\{0\} \times ⋃ dom P) ↾}_{y} = (\{0\} \cap y) \times ⋃ dom P$
17	16	cnveqi	$⊢ {({(\{0\} \times ⋃ dom P) ↾}_{y})}^{-1} = {((\{0\} \cap y) \times ⋃ dom P)}^{-1}$
18	17	dmeqi	$⊢ dom {({(\{0\} \times ⋃ dom P) ↾}_{y})}^{-1} = dom {((\{0\} \cap y) \times ⋃ dom P)}^{-1}$
19		cnvxp	$⊢ {((\{0\} \cap y) \times ⋃ dom P)}^{-1} = ⋃ dom P \times (\{0\} \cap y)$
20	19	dmeqi	$⊢ dom {((\{0\} \cap y) \times ⋃ dom P)}^{-1} = dom (⋃ dom P \times (\{0\} \cap y))$
21	15 18 20	3eqtri	$⊢ {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] = dom (⋃ dom P \times (\{0\} \cap y))$
22		xpeq2	$⊢ \{0\} \cap y = \emptyset \to ⋃ dom P \times (\{0\} \cap y) = ⋃ dom P \times \emptyset$
23		xp0	$⊢ ⋃ dom P \times \emptyset = \emptyset$
24	22 23	eqtrdi	$⊢ \{0\} \cap y = \emptyset \to ⋃ dom P \times (\{0\} \cap y) = \emptyset$
25	24	dmeqd	$⊢ \{0\} \cap y = \emptyset \to dom (⋃ dom P \times (\{0\} \cap y)) = dom \emptyset$
26		dm0	$⊢ dom \emptyset = \emptyset$
27	25 26	eqtrdi	$⊢ \{0\} \cap y = \emptyset \to dom (⋃ dom P \times (\{0\} \cap y)) = \emptyset$
28	27	adantl	$⊢ (φ \land \{0\} \cap y = \emptyset) \to dom (⋃ dom P \times (\{0\} \cap y)) = \emptyset$
29		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
30		0elsiga	$⊢ dom P \in ⋃ ran sigAlgebra \to \emptyset \in dom P$
31	1 29 30	3syl	$⊢ φ \to \emptyset \in dom P$
32	31	adantr	$⊢ (φ \land \{0\} \cap y = \emptyset) \to \emptyset \in dom P$
33	28 32	eqeltrd	$⊢ (φ \land \{0\} \cap y = \emptyset) \to dom (⋃ dom P \times (\{0\} \cap y)) \in dom P$
34	21 33	eqeltrid	$⊢ (φ \land \{0\} \cap y = \emptyset) \to {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] \in dom P$
35		dmxp	$⊢ \{0\} \cap y \neq \emptyset \to dom (⋃ dom P \times (\{0\} \cap y)) = ⋃ dom P$
36	35	adantl	$⊢ (φ \land \{0\} \cap y \neq \emptyset) \to dom (⋃ dom P \times (\{0\} \cap y)) = ⋃ dom P$
37	1	unveldomd	$⊢ φ \to ⋃ dom P \in dom P$
38	37	adantr	$⊢ (φ \land \{0\} \cap y \neq \emptyset) \to ⋃ dom P \in dom P$
39	36 38	eqeltrd	$⊢ (φ \land \{0\} \cap y \neq \emptyset) \to dom (⋃ dom P \times (\{0\} \cap y)) \in dom P$
40	21 39	eqeltrid	$⊢ (φ \land \{0\} \cap y \neq \emptyset) \to {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] \in dom P$
41	34 40	pm2.61dane	$⊢ φ \to {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] \in dom P$
42	41	ralrimivw	$⊢ φ \to \forall y \in 𝔅_{ℝ} {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] \in dom P$
43	1	isrrvv	$⊢ φ \to ((x \in ⋃ dom P ⟼ 0) \in {RndVar}_{ℝ} (P) \leftrightarrow ((x \in ⋃ dom P ⟼ 0) : ⋃ dom P ⟶ ℝ \land \forall y \in 𝔅_{ℝ} {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] \in dom P))$
44	7 42 43	mpbir2and	$⊢ φ \to (x \in ⋃ dom P ⟼ 0) \in {RndVar}_{ℝ} (P)$

Metamath Proof Explorer

Theorem 0rrv

Proof