mbfimaopn

Description: The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf , which explains why A e. dom vol is too weak a condition for this theorem.) (Contributed by Mario Carneiro, 25-Aug-2014)

		Ref	Expression
	Hypothesis	mbfimaopn.1	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	mbfimaopn	$⊢ (F \in MblFn \land A \in J) \to F^{-1} [A] \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		mbfimaopn.1	$⊢ J = TopOpen (ℂ_{fld})$
2		oveq1	$⊢ t = x \to t + i w = x + i w$
3		oveq2	$⊢ w = y \to i w = i y$
4	3	oveq2d	$⊢ w = y \to x + i w = x + i y$
5	2 4	cbvmpov	$⊢ (t \in ℝ, w \in ℝ ⟼ t + i w) = (x \in ℝ, y \in ℝ ⟼ x + i y)$
6		eqid	$⊢ (.) [ℚ \times ℚ] = (.) [ℚ \times ℚ]$
7		eqid	$⊢ ran (x \in (.) [ℚ \times ℚ], y \in (.) [ℚ \times ℚ] ⟼ x \times y) = ran (x \in (.) [ℚ \times ℚ], y \in (.) [ℚ \times ℚ] ⟼ x \times y)$
8	1 5 6 7	mbfimaopnlem	$⊢ (F \in MblFn \land A \in J) \to F^{-1} [A] \in dom vol$

Metamath Proof Explorer

Theorem mbfimaopn

Proof