smfco

Description: The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfco.s	$⊢ φ \to S \in SAlg$
	smfco.f	$⊢ φ \to F \in SMblFn (S)$
	smfco.j	$⊢ J = topGen (ran (.))$
	smfco.b	$⊢ B = SalGen (J)$
	smfco.h	$⊢ φ \to H \in SMblFn (B)$
Assertion	smfco	$⊢ φ \to H \circ F \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfco.s	$⊢ φ \to S \in SAlg$
2		smfco.f	$⊢ φ \to F \in SMblFn (S)$
3		smfco.j	$⊢ J = topGen (ran (.))$
4		smfco.b	$⊢ B = SalGen (J)$
5		smfco.h	$⊢ φ \to H \in SMblFn (B)$
6		nfv	$⊢ Ⅎ a φ$
7		cnvimass	$⊢ F^{-1} [dom H] \subseteq dom F$
8	7	a1i	$⊢ φ \to F^{-1} [dom H] \subseteq dom F$
9		eqid	$⊢ dom F = dom F$
10	1 2 9	smfdmss	$⊢ φ \to dom F \subseteq ⋃ S$
11	8 10	sstrd	$⊢ φ \to F^{-1} [dom H] \subseteq ⋃ S$
12		retop	$⊢ topGen (ran (.)) \in Top$
13	3 12	eqeltri	$⊢ J \in Top$
14	13	a1i	$⊢ φ \to J \in Top$
15	14 4	salgencld	$⊢ φ \to B \in SAlg$
16		eqid	$⊢ dom H = dom H$
17	15 5 16	smff	$⊢ φ \to H : dom H ⟶ ℝ$
18	17	ffund	$⊢ φ \to Fun H$
19	1 2 9	smff	$⊢ φ \to F : dom F ⟶ ℝ$
20	19	ffund	$⊢ φ \to Fun F$
21	18 20	fco3	$⊢ φ \to (H \circ F) : F^{-1} [dom H] ⟶ ran H$
22	17	frnd	$⊢ φ \to ran H \subseteq ℝ$
23	21 22	fssd	$⊢ φ \to (H \circ F) : F^{-1} [dom H] ⟶ ℝ$
24	23	adantr	$⊢ (φ \land a \in ℝ) \to (H \circ F) : F^{-1} [dom H] ⟶ ℝ$
25		rexr	$⊢ a \in ℝ \to a \in ℝ^{*}$
26	25	adantl	$⊢ (φ \land a \in ℝ) \to a \in ℝ^{*}$
27	24 26	preimaioomnf	$⊢ (φ \land a \in ℝ) \to {(H \circ F)}^{-1} [(−∞, a)] = \{x \in F^{-1} [dom H] \| (H \circ F) (x) < a\}$
28	27	eqcomd	$⊢ (φ \land a \in ℝ) \to \{x \in F^{-1} [dom H] \| (H \circ F) (x) < a\} = {(H \circ F)}^{-1} [(−∞, a)]$
29		cnvco	$⊢ {(H \circ F)}^{-1} = F^{-1} \circ H^{-1}$
30	29	imaeq1i	$⊢ {(H \circ F)}^{-1} [(−∞, a)] = (F^{-1} \circ H^{-1}) [(−∞, a)]$
31	30	a1i	$⊢ (φ \land a \in ℝ) \to {(H \circ F)}^{-1} [(−∞, a)] = (F^{-1} \circ H^{-1}) [(−∞, a)]$
32		imaco	$⊢ (F^{-1} \circ H^{-1}) [(−∞, a)] = F^{-1} [H^{-1} [(−∞, a)]]$
33	32	a1i	$⊢ (φ \land a \in ℝ) \to (F^{-1} \circ H^{-1}) [(−∞, a)] = F^{-1} [H^{-1} [(−∞, a)]]$
34	28 31 33	3eqtrd	$⊢ (φ \land a \in ℝ) \to \{x \in F^{-1} [dom H] \| (H \circ F) (x) < a\} = F^{-1} [H^{-1} [(−∞, a)]]$
35	17	adantr	$⊢ (φ \land a \in ℝ) \to H : dom H ⟶ ℝ$
36	35 26	preimaioomnf	$⊢ (φ \land a \in ℝ) \to H^{-1} [(−∞, a)] = \{x \in dom H \| H (x) < a\}$
37	36	eqcomd	$⊢ (φ \land a \in ℝ) \to \{x \in dom H \| H (x) < a\} = H^{-1} [(−∞, a)]$
38	37	eqcomd	$⊢ (φ \land a \in ℝ) \to H^{-1} [(−∞, a)] = \{x \in dom H \| H (x) < a\}$
39	15	adantr	$⊢ (φ \land a \in ℝ) \to B \in SAlg$
40	5	adantr	$⊢ (φ \land a \in ℝ) \to H \in SMblFn (B)$
41		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
42	39 40 16 41	smfpreimalt	$⊢ (φ \land a \in ℝ) \to \{x \in dom H \| H (x) < a\} \in (B ↾_{𝑡} dom H)$
43	38 42	eqeltrd	$⊢ (φ \land a \in ℝ) \to H^{-1} [(−∞, a)] \in (B ↾_{𝑡} dom H)$
44	15	elexd	$⊢ φ \to B \in V$
45	5	dmexd	$⊢ φ \to dom H \in V$
46		elrest	$⊢ (B \in V \land dom H \in V) \to (H^{-1} [(−∞, a)] \in (B ↾_{𝑡} dom H) \leftrightarrow \exists e \in B H^{-1} [(−∞, a)] = e \cap dom H)$
47	44 45 46	syl2anc	$⊢ φ \to (H^{-1} [(−∞, a)] \in (B ↾_{𝑡} dom H) \leftrightarrow \exists e \in B H^{-1} [(−∞, a)] = e \cap dom H)$
48	47	adantr	$⊢ (φ \land a \in ℝ) \to (H^{-1} [(−∞, a)] \in (B ↾_{𝑡} dom H) \leftrightarrow \exists e \in B H^{-1} [(−∞, a)] = e \cap dom H)$
49	43 48	mpbid	$⊢ (φ \land a \in ℝ) \to \exists e \in B H^{-1} [(−∞, a)] = e \cap dom H$
50		imaeq2	$⊢ H^{-1} [(−∞, a)] = e \cap dom H \to F^{-1} [H^{-1} [(−∞, a)]] = F^{-1} [e \cap dom H]$
51	50	3ad2ant3	$⊢ (φ \land e \in B \land H^{-1} [(−∞, a)] = e \cap dom H) \to F^{-1} [H^{-1} [(−∞, a)]] = F^{-1} [e \cap dom H]$
52		ovexd	$⊢ (φ \land e \in B) \to S ↾_{𝑡} dom F \in V$
53	2	elexd	$⊢ φ \to F \in V$
54		cnvexg	$⊢ F \in V \to F^{-1} \in V$
55	53 54	syl	$⊢ φ \to F^{-1} \in V$
56		imaexg	$⊢ F^{-1} \in V \to F^{-1} [dom H] \in V$
57	55 56	syl	$⊢ φ \to F^{-1} [dom H] \in V$
58	57	adantr	$⊢ (φ \land e \in B) \to F^{-1} [dom H] \in V$
59	1	adantr	$⊢ (φ \land e \in B) \to S \in SAlg$
60	2	adantr	$⊢ (φ \land e \in B) \to F \in SMblFn (S)$
61		simpr	$⊢ (φ \land e \in B) \to e \in B$
62		eqid	$⊢ F^{-1} [e] = F^{-1} [e]$
63	59 60 9 3 4 61 62	smfpimbor1	$⊢ (φ \land e \in B) \to F^{-1} [e] \in (S ↾_{𝑡} dom F)$
64		eqid	$⊢ F^{-1} [e] \cap F^{-1} [dom H] = F^{-1} [e] \cap F^{-1} [dom H]$
65	52 58 63 64	elrestd	$⊢ (φ \land e \in B) \to F^{-1} [e] \cap F^{-1} [dom H] \in ((S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H])$
66		inpreima	$⊢ Fun F \to F^{-1} [e \cap dom H] = F^{-1} [e] \cap F^{-1} [dom H]$
67	20 66	syl	$⊢ φ \to F^{-1} [e \cap dom H] = F^{-1} [e] \cap F^{-1} [dom H]$
68	67	adantr	$⊢ (φ \land e \in B) \to F^{-1} [e \cap dom H] = F^{-1} [e] \cap F^{-1} [dom H]$
69	2	dmexd	$⊢ φ \to dom F \in V$
70		restabs	$⊢ (S \in SAlg \land F^{-1} [dom H] \subseteq dom F \land dom F \in V) \to (S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H] = S ↾_{𝑡} F^{-1} [dom H]$
71	1 8 69 70	syl3anc	$⊢ φ \to (S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H] = S ↾_{𝑡} F^{-1} [dom H]$
72	71	eqcomd	$⊢ φ \to S ↾_{𝑡} F^{-1} [dom H] = (S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H]$
73	72	adantr	$⊢ (φ \land e \in B) \to S ↾_{𝑡} F^{-1} [dom H] = (S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H]$
74	68 73	eleq12d	$⊢ (φ \land e \in B) \to (F^{-1} [e \cap dom H] \in (S ↾_{𝑡} F^{-1} [dom H]) \leftrightarrow F^{-1} [e] \cap F^{-1} [dom H] \in ((S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H]))$
75	65 74	mpbird	$⊢ (φ \land e \in B) \to F^{-1} [e \cap dom H] \in (S ↾_{𝑡} F^{-1} [dom H])$
76	75	3adant3	$⊢ (φ \land e \in B \land H^{-1} [(−∞, a)] = e \cap dom H) \to F^{-1} [e \cap dom H] \in (S ↾_{𝑡} F^{-1} [dom H])$
77	51 76	eqeltrd	$⊢ (φ \land e \in B \land H^{-1} [(−∞, a)] = e \cap dom H) \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H])$
78	77	3exp	$⊢ φ \to (e \in B \to (H^{-1} [(−∞, a)] = e \cap dom H \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H])))$
79	78	adantr	$⊢ (φ \land a \in ℝ) \to (e \in B \to (H^{-1} [(−∞, a)] = e \cap dom H \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H])))$
80	79	rexlimdv	$⊢ (φ \land a \in ℝ) \to (\exists e \in B H^{-1} [(−∞, a)] = e \cap dom H \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H]))$
81	49 80	mpd	$⊢ (φ \land a \in ℝ) \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H])$
82	34 81	eqeltrd	$⊢ (φ \land a \in ℝ) \to \{x \in F^{-1} [dom H] \| (H \circ F) (x) < a\} \in (S ↾_{𝑡} F^{-1} [dom H])$
83	6 1 11 23 82	issmfd	$⊢ φ \to H \circ F \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfco

Proof