This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) ) )