cncombf

Description: The composition of a continuous function with a measurable function is measurable. (More generally, G can be a Borel-measurable function, but notably the condition that G be only measurable is too weak, the usual counterexample taking G to be the Cantor function and F the indicator function of the G -image of a nonmeasurable set, which is a subset of the Cantor set and hence null and measurable.) (Contributed by Mario Carneiro, 25-Aug-2014)

		Ref	Expression
	Assertion	cncombf	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to G \circ F \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to G : B \underset{cn}{⟶} ℂ$
2		cncff	$⊢ G : B \underset{cn}{⟶} ℂ \to G : B ⟶ ℂ$
3	1 2	syl	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to G : B ⟶ ℂ$
4		simp2	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to F : A ⟶ B$
5		fco	$⊢ (G : B ⟶ ℂ \land F : A ⟶ B) \to (G \circ F) : A ⟶ ℂ$
6	3 4 5	syl2anc	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to (G \circ F) : A ⟶ ℂ$
7	4	fdmd	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to dom F = A$
8		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
9	8	3ad2ant1	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to dom F \in dom vol$
10	7 9	eqeltrrd	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to A \in dom vol$
11		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
12	10 11	syl	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to A \subseteq ℝ$
13		cnex	$⊢ ℂ \in V$
14		reex	$⊢ ℝ \in V$
15		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land ((G \circ F) : A ⟶ ℂ \land A \subseteq ℝ)) \to G \circ F \in (ℂ ↑_{𝑝𝑚} ℝ)$
16	13 14 15	mpanl12	$⊢ ((G \circ F) : A ⟶ ℂ \land A \subseteq ℝ) \to G \circ F \in (ℂ ↑_{𝑝𝑚} ℝ)$
17	6 12 16	syl2anc	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to G \circ F \in (ℂ ↑_{𝑝𝑚} ℝ)$
18		coeq1	$⊢ g = ℜ \circ G \to g \circ F = (ℜ \circ G) \circ F$
19		coass	$⊢ (ℜ \circ G) \circ F = ℜ \circ (G \circ F)$
20	18 19	eqtrdi	$⊢ g = ℜ \circ G \to g \circ F = ℜ \circ (G \circ F)$
21	20	cnveqd	$⊢ g = ℜ \circ G \to {(g \circ F)}^{-1} = {(ℜ \circ (G \circ F))}^{-1}$
22	21	imaeq1d	$⊢ g = ℜ \circ G \to {(g \circ F)}^{-1} [x] = {(ℜ \circ (G \circ F))}^{-1} [x]$
23	22	eleq1d	$⊢ g = ℜ \circ G \to ({(g \circ F)}^{-1} [x] \in dom vol \leftrightarrow {(ℜ \circ (G \circ F))}^{-1} [x] \in dom vol)$
24		cnvco	$⊢ {(g \circ F)}^{-1} = F^{-1} \circ g^{-1}$
25	24	imaeq1i	$⊢ {(g \circ F)}^{-1} [x] = (F^{-1} \circ g^{-1}) [x]$
26		imaco	$⊢ (F^{-1} \circ g^{-1}) [x] = F^{-1} [g^{-1} [x]]$
27	25 26	eqtri	$⊢ {(g \circ F)}^{-1} [x] = F^{-1} [g^{-1} [x]]$
28		simplll	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to F \in MblFn$
29		simpllr	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to F : A ⟶ B$
30		cncfrss	$⊢ g : B \underset{cn}{⟶} ℝ \to B \subseteq ℂ$
31	30	adantl	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to B \subseteq ℂ$
32		simpr	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to g : B \underset{cn}{⟶} ℝ$
33		ax-resscn	$⊢ ℝ \subseteq ℂ$
34		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
35		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} B = TopOpen (ℂ_{fld}) ↾_{𝑡} B$
36		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
37	34 35 36	cncfcn	$⊢ (B \subseteq ℂ \land ℝ \subseteq ℂ) \to B \underset{cn}{⟶} ℝ = (TopOpen (ℂ_{fld}) ↾_{𝑡} B) Cn topGen (ran (.))$
38	31 33 37	sylancl	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to B \underset{cn}{⟶} ℝ = (TopOpen (ℂ_{fld}) ↾_{𝑡} B) Cn topGen (ran (.))$
39	32 38	eleqtrd	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to g \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} B) Cn topGen (ran (.)))$
40		retopbas	$⊢ ran (.) \in TopBases$
41		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
42	40 41	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
43		simplr	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to x \in ran (.)$
44	42 43	sselid	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to x \in topGen (ran (.))$
45		cnima	$⊢ (g \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} B) Cn topGen (ran (.))) \land x \in topGen (ran (.))) \to g^{-1} [x] \in (TopOpen (ℂ_{fld}) ↾_{𝑡} B)$
46	39 44 45	syl2anc	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to g^{-1} [x] \in (TopOpen (ℂ_{fld}) ↾_{𝑡} B)$
47	34 35	mbfimaopn2	$⊢ ((F \in MblFn \land F : A ⟶ B \land B \subseteq ℂ) \land g^{-1} [x] \in (TopOpen (ℂ_{fld}) ↾_{𝑡} B)) \to F^{-1} [g^{-1} [x]] \in dom vol$
48	28 29 31 46 47	syl31anc	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to F^{-1} [g^{-1} [x]] \in dom vol$
49	27 48	eqeltrid	$⊢ (((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \land g : B \underset{cn}{⟶} ℝ) \to {(g \circ F)}^{-1} [x] \in dom vol$
50	49	ralrimiva	$⊢ ((F \in MblFn \land F : A ⟶ B) \land x \in ran (.)) \to \forall g \in (B \underset{cn}{⟶} ℝ) {(g \circ F)}^{-1} [x] \in dom vol$
51	50	3adantl3	$⊢ ((F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to \forall g \in (B \underset{cn}{⟶} ℝ) {(g \circ F)}^{-1} [x] \in dom vol$
52		recncf	$⊢ ℜ : ℂ \underset{cn}{⟶} ℝ$
53	52	a1i	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to ℜ : ℂ \underset{cn}{⟶} ℝ$
54	1 53	cncfco	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to (ℜ \circ G) : B \underset{cn}{⟶} ℝ$
55	54	adantr	$⊢ ((F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to (ℜ \circ G) : B \underset{cn}{⟶} ℝ$
56	23 51 55	rspcdva	$⊢ ((F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to {(ℜ \circ (G \circ F))}^{-1} [x] \in dom vol$
57		coeq1	$⊢ g = ℑ \circ G \to g \circ F = (ℑ \circ G) \circ F$
58		coass	$⊢ (ℑ \circ G) \circ F = ℑ \circ (G \circ F)$
59	57 58	eqtrdi	$⊢ g = ℑ \circ G \to g \circ F = ℑ \circ (G \circ F)$
60	59	cnveqd	$⊢ g = ℑ \circ G \to {(g \circ F)}^{-1} = {(ℑ \circ (G \circ F))}^{-1}$
61	60	imaeq1d	$⊢ g = ℑ \circ G \to {(g \circ F)}^{-1} [x] = {(ℑ \circ (G \circ F))}^{-1} [x]$
62	61	eleq1d	$⊢ g = ℑ \circ G \to ({(g \circ F)}^{-1} [x] \in dom vol \leftrightarrow {(ℑ \circ (G \circ F))}^{-1} [x] \in dom vol)$
63		imcncf	$⊢ ℑ : ℂ \underset{cn}{⟶} ℝ$
64	63	a1i	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to ℑ : ℂ \underset{cn}{⟶} ℝ$
65	1 64	cncfco	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to (ℑ \circ G) : B \underset{cn}{⟶} ℝ$
66	65	adantr	$⊢ ((F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to (ℑ \circ G) : B \underset{cn}{⟶} ℝ$
67	62 51 66	rspcdva	$⊢ ((F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to {(ℑ \circ (G \circ F))}^{-1} [x] \in dom vol$
68	56 67	jca	$⊢ ((F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \land x \in ran (.)) \to ({(ℜ \circ (G \circ F))}^{-1} [x] \in dom vol \land {(ℑ \circ (G \circ F))}^{-1} [x] \in dom vol)$
69	68	ralrimiva	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to \forall x \in ran (.) ({(ℜ \circ (G \circ F))}^{-1} [x] \in dom vol \land {(ℑ \circ (G \circ F))}^{-1} [x] \in dom vol)$
70		ismbf1	$⊢ G \circ F \in MblFn \leftrightarrow (G \circ F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \forall x \in ran (.) ({(ℜ \circ (G \circ F))}^{-1} [x] \in dom vol \land {(ℑ \circ (G \circ F))}^{-1} [x] \in dom vol))$
71	17 69 70	sylanbrc	$⊢ (F \in MblFn \land F : A ⟶ B \land G : B \underset{cn}{⟶} ℂ) \to G \circ F \in MblFn$

Metamath Proof Explorer

Theorem cncombf

Proof