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		df-res	$⊢ {(\{0\} \times ⋃ dom P) ↾}_{y} = (\{0\} \times ⋃ dom P) \cap (y \times V)$
17		inxp	$⊢ (\{0\} \times ⋃ dom P) \cap (y \times V) = (\{0\} \cap y) \times (⋃ dom P \cap V)$
18		inv1	$⊢ ⋃ dom P \cap V = ⋃ dom P$
19	18	xpeq2i	$⊢ (\{0\} \cap y) \times (⋃ dom P \cap V) = (\{0\} \cap y) \times ⋃ dom P$
20	16 17 19	3eqtri	$⊢ {(\{0\} \times ⋃ dom P) ↾}_{y} = (\{0\} \cap y) \times ⋃ dom P$
21	20	cnveqi	$⊢ {({(\{0\} \times ⋃ dom P) ↾}_{y})}^{-1} = {((\{0\} \cap y) \times ⋃ dom P)}^{-1}$
22	21	dmeqi	$⊢ dom {({(\{0\} \times ⋃ dom P) ↾}_{y})}^{-1} = dom {((\{0\} \cap y) \times ⋃ dom P)}^{-1}$
23		cnvxp	$⊢ {((\{0\} \cap y) \times ⋃ dom P)}^{-1} = ⋃ dom P \times (\{0\} \cap y)$
24	23	dmeqi	$⊢ dom {((\{0\} \cap y) \times ⋃ dom P)}^{-1} = dom (⋃ dom P \times (\{0\} \cap y))$
25	15 22 24	3eqtri	$⊢ {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] = dom (⋃ dom P \times (\{0\} \cap y))$
26		xpeq2	$⊢ \{0\} \cap y = \emptyset \to ⋃ dom P \times (\{0\} \cap y) = ⋃ dom P \times \emptyset$
27		xp0	$⊢ ⋃ dom P \times \emptyset = \emptyset$
28	26 27	eqtrdi	$⊢ \{0\} \cap y = \emptyset \to ⋃ dom P \times (\{0\} \cap y) = \emptyset$
29	28	dmeqd	$⊢ \{0\} \cap y = \emptyset \to dom (⋃ dom P \times (\{0\} \cap y)) = dom \emptyset$
30		dm0	$⊢ dom \emptyset = \emptyset$
31	29 30	eqtrdi	$⊢ \{0\} \cap y = \emptyset \to dom (⋃ dom P \times (\{0\} \cap y)) = \emptyset$
32	31	adantl	$⊢ (φ \land \{0\} \cap y = \emptyset) \to dom (⋃ dom P \times (\{0\} \cap y)) = \emptyset$
33		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
34		0elsiga	$⊢ dom P \in ⋃ ran sigAlgebra \to \emptyset \in dom P$
35	1 33 34	3syl	$⊢ φ \to \emptyset \in dom P$
36	35	adantr	$⊢ (φ \land \{0\} \cap y = \emptyset) \to \emptyset \in dom P$
37	32 36	eqeltrd	$⊢ (φ \land \{0\} \cap y = \emptyset) \to dom (⋃ dom P \times (\{0\} \cap y)) \in dom P$
38	25 37	eqeltrid	$⊢ (φ \land \{0\} \cap y = \emptyset) \to {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] \in dom P$
39		dmxp	$⊢ \{0\} \cap y \neq \emptyset \to dom (⋃ dom P \times (\{0\} \cap y)) = ⋃ dom P$
40	39	adantl	$⊢ (φ \land \{0\} \cap y \neq \emptyset) \to dom (⋃ dom P \times (\{0\} \cap y)) = ⋃ dom P$
41	1	unveldomd	$⊢ φ \to ⋃ dom P \in dom P$
42	41	adantr	$⊢ (φ \land \{0\} \cap y \neq \emptyset) \to ⋃ dom P \in dom P$
43	40 42	eqeltrd	$⊢ (φ \land \{0\} \cap y \neq \emptyset) \to dom (⋃ dom P \times (\{0\} \cap y)) \in dom P$
44	25 43	eqeltrid	$⊢ (φ \land \{0\} \cap y \neq \emptyset) \to {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] \in dom P$
45	38 44	pm2.61dane	$⊢ φ \to {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] \in dom P$
46	45	ralrimivw	$⊢ φ \to \forall y \in 𝔅_{ℝ} {(x \in ⋃ dom P ⟼ 0)}^{-1} [y] \in dom P$
47	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))$
48	7 46 47	mpbir2and	$⊢ φ \to (x \in ⋃ dom P ⟼ 0) \in {RndVar}_{ℝ} (P)$

Metamath Proof Explorer

Theorem 0rrv

Proof