cnmbf

Description: A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014) (Revised by Mario Carneiro, 26-Mar-2015)

		Ref	Expression
	Assertion	cnmbf	$⊢ (A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \to F \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		cncff	$⊢ F : A \underset{cn}{⟶} ℂ \to F : A ⟶ ℂ$
2		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
3		cnex	$⊢ ℂ \in V$
4		reex	$⊢ ℝ \in V$
5		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℝ)) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
6	3 4 5	mpanl12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
7	1 2 6	syl2anr	$⊢ (A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
8		simpll	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to A \in dom vol$
9		simplr	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to F : A \underset{cn}{⟶} ℂ$
10		recncf	$⊢ ℜ : ℂ \underset{cn}{⟶} ℝ$
11	10	a1i	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to ℜ : ℂ \underset{cn}{⟶} ℝ$
12	9 11	cncfco	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to (ℜ \circ F) : A \underset{cn}{⟶} ℝ$
13	2	ad2antrr	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to A \subseteq ℝ$
14		ax-resscn	$⊢ ℝ \subseteq ℂ$
15	13 14	sstrdi	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to A \subseteq ℂ$
16		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
17		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} A = TopOpen (ℂ_{fld}) ↾_{𝑡} A$
18		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
19	16 17 18	cncfcn	$⊢ (A \subseteq ℂ \land ℝ \subseteq ℂ) \to A \underset{cn}{⟶} ℝ = (TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn topGen (ran (.))$
20	15 14 19	sylancl	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to A \underset{cn}{⟶} ℝ = (TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn topGen (ran (.))$
21		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
22	16 21	rerest	$⊢ A \subseteq ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} A = topGen (ran (.)) ↾_{𝑡} A$
23	13 22	syl	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} A = topGen (ran (.)) ↾_{𝑡} A$
24	23	oveq1d	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} A) Cn topGen (ran (.)) = (topGen (ran (.)) ↾_{𝑡} A) Cn topGen (ran (.))$
25	20 24	eqtrd	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to A \underset{cn}{⟶} ℝ = (topGen (ran (.)) ↾_{𝑡} A) Cn topGen (ran (.))$
26	12 25	eleqtrd	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to ℜ \circ F \in ((topGen (ran (.)) ↾_{𝑡} A) Cn topGen (ran (.)))$
27		retopbas	$⊢ ran (.) \in TopBases$
28		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
29	27 28	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
30		simpr	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to x \in ran (.)$
31	29 30	sselid	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to x \in topGen (ran (.))$
32		cnima	$⊢ (ℜ \circ F \in ((topGen (ran (.)) ↾_{𝑡} A) Cn topGen (ran (.))) \land x \in topGen (ran (.))) \to {(ℜ \circ F)}^{-1} [x] \in (topGen (ran (.)) ↾_{𝑡} A)$
33	26 31 32	syl2anc	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to {(ℜ \circ F)}^{-1} [x] \in (topGen (ran (.)) ↾_{𝑡} A)$
34		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} A = topGen (ran (.)) ↾_{𝑡} A$
35	34	subopnmbl	$⊢ (A \in dom vol \land {(ℜ \circ F)}^{-1} [x] \in (topGen (ran (.)) ↾_{𝑡} A)) \to {(ℜ \circ F)}^{-1} [x] \in dom vol$
36	8 33 35	syl2anc	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to {(ℜ \circ F)}^{-1} [x] \in dom vol$
37		imcncf	$⊢ ℑ : ℂ \underset{cn}{⟶} ℝ$
38	37	a1i	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to ℑ : ℂ \underset{cn}{⟶} ℝ$
39	9 38	cncfco	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to (ℑ \circ F) : A \underset{cn}{⟶} ℝ$
40	39 25	eleqtrd	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to ℑ \circ F \in ((topGen (ran (.)) ↾_{𝑡} A) Cn topGen (ran (.)))$
41		cnima	$⊢ (ℑ \circ F \in ((topGen (ran (.)) ↾_{𝑡} A) Cn topGen (ran (.))) \land x \in topGen (ran (.))) \to {(ℑ \circ F)}^{-1} [x] \in (topGen (ran (.)) ↾_{𝑡} A)$
42	40 31 41	syl2anc	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to {(ℑ \circ F)}^{-1} [x] \in (topGen (ran (.)) ↾_{𝑡} A)$
43	34	subopnmbl	$⊢ (A \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in (topGen (ran (.)) ↾_{𝑡} A)) \to {(ℑ \circ F)}^{-1} [x] \in dom vol$
44	8 42 43	syl2anc	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to {(ℑ \circ F)}^{-1} [x] \in dom vol$
45	36 44	jca	$⊢ ((A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol)$
46	45	ralrimiva	$⊢ (A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \to \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol)$
47		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))$
48	7 46 47	sylanbrc	$⊢ (A \in dom vol \land F : A \underset{cn}{⟶} ℂ) \to F \in MblFn$

Metamath Proof Explorer

Theorem cnmbf

Proof