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 e. MblFn <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )

Proof

Step	Hyp	Ref	Expression
1		coeq2	|- ( f = F -> ( Re o. f ) = ( Re o. F ) )
2	1	cnveqd	|- ( f = F -> `' ( Re o. f ) = `' ( Re o. F ) )
3	2	imaeq1d	|- ( f = F -> ( `' ( Re o. f ) " x ) = ( `' ( Re o. F ) " x ) )
4	3	eleq1d	|- ( f = F -> ( ( `' ( Re o. f ) " x ) e. dom vol <-> ( `' ( Re o. F ) " x ) e. dom vol ) )
5		coeq2	|- ( f = F -> ( Im o. f ) = ( Im o. F ) )
6	5	cnveqd	|- ( f = F -> `' ( Im o. f ) = `' ( Im o. F ) )
7	6	imaeq1d	|- ( f = F -> ( `' ( Im o. f ) " x ) = ( `' ( Im o. F ) " x ) )
8	7	eleq1d	|- ( f = F -> ( ( `' ( Im o. f ) " x ) e. dom vol <-> ( `' ( Im o. F ) " x ) e. dom vol ) )
9	4 8	anbi12d	|- ( f = F -> ( ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol ) <-> ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
10	9	ralbidv	|- ( f = F -> ( A. x e. ran (,) ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol ) <-> A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
11		df-mbf	|- MblFn = { f e. ( CC ^pm RR ) | A. x e. ran (,) ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol ) }
12	10 11	elrab2	|- ( F e. MblFn <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )