Metamath Proof Explorer

Theorem ismbf1

Description: The predicate " F is a measurable function". This is more naturally stated for functions on the reals, see ismbf and ismbfcn for the decomposition of the real and imaginary parts. (Contributed by Mario Carneiro, 17-Jun-2014)

		Ref	Expression
	Assertion	ismbf1	$⊢ F \in MblFn \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$

Proof

Step	Hyp	Ref	Expression
1		coeq2	$⊢ f = F \to ℜ \circ f = ℜ \circ F$
2	1	cnveqd	$⊢ f = F \to {(ℜ \circ f)}^{-1} = {(ℜ \circ F)}^{-1}$
3	2	imaeq1d	$⊢ f = F \to {(ℜ \circ f)}^{-1} [x] = {(ℜ \circ F)}^{-1} [x]$
4	3	eleq1d	$⊢ f = F \to ({(ℜ \circ f)}^{-1} [x] \in dom vol \leftrightarrow {(ℜ \circ F)}^{-1} [x] \in dom vol)$
5		coeq2	$⊢ f = F \to ℑ \circ f = ℑ \circ F$
6	5	cnveqd	$⊢ f = F \to {(ℑ \circ f)}^{-1} = {(ℑ \circ F)}^{-1}$
7	6	imaeq1d	$⊢ f = F \to {(ℑ \circ f)}^{-1} [x] = {(ℑ \circ F)}^{-1} [x]$
8	7	eleq1d	$⊢ f = F \to ({(ℑ \circ f)}^{-1} [x] \in dom vol \leftrightarrow {(ℑ \circ F)}^{-1} [x] \in dom vol)$
9	4 8	anbi12d	$⊢ f = F \to (({(ℜ \circ f)}^{-1} [x] \in dom vol \land {(ℑ \circ f)}^{-1} [x] \in dom vol) \leftrightarrow ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$
10	9	ralbidv	$⊢ f = F \to (\forall x \in ran (.) ({(ℜ \circ f)}^{-1} [x] \in dom vol \land {(ℑ \circ f)}^{-1} [x] \in dom vol) \leftrightarrow \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$
11		df-mbf	$⊢ MblFn = \{f \in (ℂ ↑_{𝑝𝑚} ℝ) \| \forall x \in ran (.) ({(ℜ \circ f)}^{-1} [x] \in dom vol \land {(ℑ \circ f)}^{-1} [x] \in dom vol)\}$
12	10 11	elrab2	$⊢ F \in MblFn \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$