mbfss

Description: Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014)

	Ref	Expression
Hypotheses	mbfss.1	$⊢ φ \to A \subseteq B$
	mbfss.2	$⊢ φ \to B \in dom vol$
	mbfss.3	$⊢ (φ \land x \in A) \to C \in V$
	mbfss.4	$⊢ (φ \land x \in (B ∖ A)) \to C = 0$
	mbfss.5	$⊢ φ \to (x \in A ⟼ C) \in MblFn$
Assertion	mbfss	$⊢ φ \to (x \in B ⟼ C) \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfss.1	$⊢ φ \to A \subseteq B$
2		mbfss.2	$⊢ φ \to B \in dom vol$
3		mbfss.3	$⊢ (φ \land x \in A) \to C \in V$
4		mbfss.4	$⊢ (φ \land x \in (B ∖ A)) \to C = 0$
5		mbfss.5	$⊢ φ \to (x \in A ⟼ C) \in MblFn$
6		elun	$⊢ x \in (A \cup (B ∖ A)) \leftrightarrow (x \in A \lor x \in (B ∖ A))$
7		undif2	$⊢ A \cup (B ∖ A) = A \cup B$
8		ssequn1	$⊢ A \subseteq B \leftrightarrow A \cup B = B$
9	1 8	sylib	$⊢ φ \to A \cup B = B$
10	7 9	syl5eq	$⊢ φ \to A \cup (B ∖ A) = B$
11	10	eleq2d	$⊢ φ \to (x \in (A \cup (B ∖ A)) \leftrightarrow x \in B)$
12	6 11	bitr3id	$⊢ φ \to ((x \in A \lor x \in (B ∖ A)) \leftrightarrow x \in B)$
13	12	biimpar	$⊢ (φ \land x \in B) \to (x \in A \lor x \in (B ∖ A))$
14	5 3	mbfmptcl	$⊢ (φ \land x \in A) \to C \in ℂ$
15		0cn	$⊢ 0 \in ℂ$
16	4 15	eqeltrdi	$⊢ (φ \land x \in (B ∖ A)) \to C \in ℂ$
17	14 16	jaodan	$⊢ (φ \land (x \in A \lor x \in (B ∖ A))) \to C \in ℂ$
18	13 17	syldan	$⊢ (φ \land x \in B) \to C \in ℂ$
19	18	recld	$⊢ (φ \land x \in B) \to ℜ (C) \in ℝ$
20	19	fmpttd	$⊢ φ \to (x \in B ⟼ ℜ (C)) : B ⟶ ℝ$
21	1	resmptd	$⊢ φ \to {(x \in B ⟼ ℜ (C)) ↾}_{A} = (x \in A ⟼ ℜ (C))$
22	14	ismbfcn2	$⊢ φ \to ((x \in A ⟼ C) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (C)) \in MblFn \land (x \in A ⟼ ℑ (C)) \in MblFn))$
23	5 22	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (C)) \in MblFn \land (x \in A ⟼ ℑ (C)) \in MblFn)$
24	23	simpld	$⊢ φ \to (x \in A ⟼ ℜ (C)) \in MblFn$
25	21 24	eqeltrd	$⊢ φ \to {(x \in B ⟼ ℜ (C)) ↾}_{A} \in MblFn$
26		difss	$⊢ B ∖ A \subseteq B$
27		resmpt	$⊢ B ∖ A \subseteq B \to {(x \in B ⟼ ℜ (C)) ↾}_{(B ∖ A)} = (x \in (B ∖ A) ⟼ ℜ (C))$
28	26 27	ax-mp	$⊢ {(x \in B ⟼ ℜ (C)) ↾}_{(B ∖ A)} = (x \in (B ∖ A) ⟼ ℜ (C))$
29	4	fveq2d	$⊢ (φ \land x \in (B ∖ A)) \to ℜ (C) = ℜ (0)$
30		re0	$⊢ ℜ (0) = 0$
31	29 30	syl6eq	$⊢ (φ \land x \in (B ∖ A)) \to ℜ (C) = 0$
32	31	mpteq2dva	$⊢ φ \to (x \in (B ∖ A) ⟼ ℜ (C)) = (x \in (B ∖ A) ⟼ 0)$
33	28 32	syl5eq	$⊢ φ \to {(x \in B ⟼ ℜ (C)) ↾}_{(B ∖ A)} = (x \in (B ∖ A) ⟼ 0)$
34		fconstmpt	$⊢ (B ∖ A) \times \{0\} = (x \in (B ∖ A) ⟼ 0)$
35	5 3	mbfdm2	$⊢ φ \to A \in dom vol$
36		difmbl	$⊢ (B \in dom vol \land A \in dom vol) \to B ∖ A \in dom vol$
37	2 35 36	syl2anc	$⊢ φ \to B ∖ A \in dom vol$
38		mbfconst	$⊢ (B ∖ A \in dom vol \land 0 \in ℂ) \to (B ∖ A) \times \{0\} \in MblFn$
39	37 15 38	sylancl	$⊢ φ \to (B ∖ A) \times \{0\} \in MblFn$
40	34 39	eqeltrrid	$⊢ φ \to (x \in (B ∖ A) ⟼ 0) \in MblFn$
41	33 40	eqeltrd	$⊢ φ \to {(x \in B ⟼ ℜ (C)) ↾}_{(B ∖ A)} \in MblFn$
42	20 25 41 10	mbfres2	$⊢ φ \to (x \in B ⟼ ℜ (C)) \in MblFn$
43	18	imcld	$⊢ (φ \land x \in B) \to ℑ (C) \in ℝ$
44	43	fmpttd	$⊢ φ \to (x \in B ⟼ ℑ (C)) : B ⟶ ℝ$
45	1	resmptd	$⊢ φ \to {(x \in B ⟼ ℑ (C)) ↾}_{A} = (x \in A ⟼ ℑ (C))$
46	23	simprd	$⊢ φ \to (x \in A ⟼ ℑ (C)) \in MblFn$
47	45 46	eqeltrd	$⊢ φ \to {(x \in B ⟼ ℑ (C)) ↾}_{A} \in MblFn$
48		resmpt	$⊢ B ∖ A \subseteq B \to {(x \in B ⟼ ℑ (C)) ↾}_{(B ∖ A)} = (x \in (B ∖ A) ⟼ ℑ (C))$
49	26 48	ax-mp	$⊢ {(x \in B ⟼ ℑ (C)) ↾}_{(B ∖ A)} = (x \in (B ∖ A) ⟼ ℑ (C))$
50	4	fveq2d	$⊢ (φ \land x \in (B ∖ A)) \to ℑ (C) = ℑ (0)$
51		im0	$⊢ ℑ (0) = 0$
52	50 51	syl6eq	$⊢ (φ \land x \in (B ∖ A)) \to ℑ (C) = 0$
53	52	mpteq2dva	$⊢ φ \to (x \in (B ∖ A) ⟼ ℑ (C)) = (x \in (B ∖ A) ⟼ 0)$
54	49 53	syl5eq	$⊢ φ \to {(x \in B ⟼ ℑ (C)) ↾}_{(B ∖ A)} = (x \in (B ∖ A) ⟼ 0)$
55	54 40	eqeltrd	$⊢ φ \to {(x \in B ⟼ ℑ (C)) ↾}_{(B ∖ A)} \in MblFn$
56	44 47 55 10	mbfres2	$⊢ φ \to (x \in B ⟼ ℑ (C)) \in MblFn$
57	18	ismbfcn2	$⊢ φ \to ((x \in B ⟼ C) \in MblFn \leftrightarrow ((x \in B ⟼ ℜ (C)) \in MblFn \land (x \in B ⟼ ℑ (C)) \in MblFn))$
58	42 56 57	mpbir2and	$⊢ φ \to (x \in B ⟼ C) \in MblFn$

Metamath Proof Explorer

Theorem mbfss

Proof