itgss3

Description: Expand the set of an integral by a nullset. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Mario Carneiro, 2-Sep-2014)

	Ref	Expression
Hypotheses	itgss3.1	$⊢ φ \to A \subseteq B$
	itgss3.2	$⊢ φ \to B \subseteq ℝ$
	itgss3.3	$⊢ φ \to {vol}^{*} (B ∖ A) = 0$
	itgss3.4	$⊢ (φ \land x \in B) \to C \in ℂ$
Assertion	itgss3	$⊢ φ \to (((x \in A ⟼ C) \in 𝐿^{1} \leftrightarrow (x \in B ⟼ C) \in 𝐿^{1}) \land \int_{A} C d x = \int_{B} C d x)$

Proof

Step	Hyp	Ref	Expression
1		itgss3.1	$⊢ φ \to A \subseteq B$
2		itgss3.2	$⊢ φ \to B \subseteq ℝ$
3		itgss3.3	$⊢ φ \to {vol}^{*} (B ∖ A) = 0$
4		itgss3.4	$⊢ (φ \land x \in B) \to C \in ℂ$
5		nfcv	$⊢ \underline{Ⅎ} y if (x \in A, C, 0)$
6		nfv	$⊢ Ⅎ x y \in A$
7		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ C$
8		nfcv	$⊢ \underline{Ⅎ} x 0$
9	6 7 8	nfif	$⊢ \underline{Ⅎ} x if (y \in A, ⦋ y / x ⦌ C, 0)$
10		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
11		csbeq1a	$⊢ x = y \to C = ⦋ y / x ⦌ C$
12	10 11	ifbieq1d	$⊢ x = y \to if (x \in A, C, 0) = if (y \in A, ⦋ y / x ⦌ C, 0)$
13	5 9 12	cbvmpt	$⊢ (x \in B ⟼ if (x \in A, C, 0)) = (y \in B ⟼ if (y \in A, ⦋ y / x ⦌ C, 0))$
14	1	adantr	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to A \subseteq B$
15		nfcv	$⊢ \underline{Ⅎ} y C$
16	15 7 11	cbvmpt	$⊢ (x \in A ⟼ C) = (y \in A ⟼ ⦋ y / x ⦌ C)$
17		iftrue	$⊢ y \in A \to if (y \in A, ⦋ y / x ⦌ C, 0) = ⦋ y / x ⦌ C$
18	17	mpteq2ia	$⊢ (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) = (y \in A ⟼ ⦋ y / x ⦌ C)$
19	16 18	eqtr4i	$⊢ (x \in A ⟼ C) = (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0))$
20		simpr	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to (x \in A ⟼ C) \in 𝐿^{1}$
21	19 20	eqeltrrid	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in 𝐿^{1}$
22		iblmbf	$⊢ (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in 𝐿^{1} \to (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in MblFn$
23	21 22	syl	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in MblFn$
24	1	sselda	$⊢ (φ \land x \in A) \to x \in B$
25	24 4	syldan	$⊢ (φ \land x \in A) \to C \in ℂ$
26	25	fmpttd	$⊢ φ \to (x \in A ⟼ C) : A ⟶ ℂ$
27	26	adantr	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to (x \in A ⟼ C) : A ⟶ ℂ$
28	19	feq1i	$⊢ (x \in A ⟼ C) : A ⟶ ℂ \leftrightarrow (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) : A ⟶ ℂ$
29	27 28	sylib	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) : A ⟶ ℂ$
30	29	fvmptelcdm	$⊢ ((φ \land (x \in A ⟼ C) \in 𝐿^{1}) \land y \in A) \to if (y \in A, ⦋ y / x ⦌ C, 0) \in ℂ$
31	23 30	mbfdm2	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to A \in dom vol$
32		undif	$⊢ A \subseteq B \leftrightarrow A \cup (B ∖ A) = B$
33	1 32	sylib	$⊢ φ \to A \cup (B ∖ A) = B$
34	33	adantr	$⊢ (φ \land A \in dom vol) \to A \cup (B ∖ A) = B$
35		id	$⊢ A \in dom vol \to A \in dom vol$
36	2	ssdifssd	$⊢ φ \to B ∖ A \subseteq ℝ$
37		nulmbl	$⊢ (B ∖ A \subseteq ℝ \land {vol}^{*} (B ∖ A) = 0) \to B ∖ A \in dom vol$
38	36 3 37	syl2anc	$⊢ φ \to B ∖ A \in dom vol$
39		unmbl	$⊢ (A \in dom vol \land B ∖ A \in dom vol) \to A \cup (B ∖ A) \in dom vol$
40	35 38 39	syl2anr	$⊢ (φ \land A \in dom vol) \to A \cup (B ∖ A) \in dom vol$
41	34 40	eqeltrrd	$⊢ (φ \land A \in dom vol) \to B \in dom vol$
42	31 41	syldan	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to B \in dom vol$
43		eldifn	$⊢ y \in (B ∖ A) \to \neg y \in A$
44	43	adantl	$⊢ ((φ \land (x \in A ⟼ C) \in 𝐿^{1}) \land y \in (B ∖ A)) \to \neg y \in A$
45	44	iffalsed	$⊢ ((φ \land (x \in A ⟼ C) \in 𝐿^{1}) \land y \in (B ∖ A)) \to if (y \in A, ⦋ y / x ⦌ C, 0) = 0$
46	14 42 30 45 21	iblss2	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to (y \in B ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in 𝐿^{1}$
47	13 46	eqeltrid	$⊢ (φ \land (x \in A ⟼ C) \in 𝐿^{1}) \to (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}$
48		iftrue	$⊢ x \in A \to if (x \in A, C, 0) = C$
49	48	mpteq2ia	$⊢ (x \in A ⟼ if (x \in A, C, 0)) = (x \in A ⟼ C)$
50	5 9 12	cbvmpt	$⊢ (x \in A ⟼ if (x \in A, C, 0)) = (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0))$
51	49 50	eqtr3i	$⊢ (x \in A ⟼ C) = (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0))$
52	1	adantr	$⊢ (φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \to A \subseteq B$
53		simpr	$⊢ (φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \to (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}$
54	13 53	eqeltrrid	$⊢ (φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \to (y \in B ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in 𝐿^{1}$
55		iblmbf	$⊢ (y \in B ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in 𝐿^{1} \to (y \in B ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in MblFn$
56	54 55	syl	$⊢ (φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \to (y \in B ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in MblFn$
57		0cn	$⊢ 0 \in ℂ$
58		ifcl	$⊢ (C \in ℂ \land 0 \in ℂ) \to if (x \in A, C, 0) \in ℂ$
59	4 57 58	sylancl	$⊢ (φ \land x \in B) \to if (x \in A, C, 0) \in ℂ$
60	59	fmpttd	$⊢ φ \to (x \in B ⟼ if (x \in A, C, 0)) : B ⟶ ℂ$
61	13	feq1i	$⊢ (x \in B ⟼ if (x \in A, C, 0)) : B ⟶ ℂ \leftrightarrow (y \in B ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) : B ⟶ ℂ$
62	60 61	sylib	$⊢ φ \to (y \in B ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) : B ⟶ ℂ$
63	62	adantr	$⊢ (φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \to (y \in B ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) : B ⟶ ℂ$
64	63	fvmptelcdm	$⊢ ((φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \land y \in B) \to if (y \in A, ⦋ y / x ⦌ C, 0) \in ℂ$
65	56 64	mbfdm2	$⊢ (φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \to B \in dom vol$
66		dfss4	$⊢ A \subseteq B \leftrightarrow B ∖ (B ∖ A) = A$
67	1 66	sylib	$⊢ φ \to B ∖ (B ∖ A) = A$
68	67	adantr	$⊢ (φ \land B \in dom vol) \to B ∖ (B ∖ A) = A$
69		id	$⊢ B \in dom vol \to B \in dom vol$
70		difmbl	$⊢ (B \in dom vol \land B ∖ A \in dom vol) \to B ∖ (B ∖ A) \in dom vol$
71	69 38 70	syl2anr	$⊢ (φ \land B \in dom vol) \to B ∖ (B ∖ A) \in dom vol$
72	68 71	eqeltrrd	$⊢ (φ \land B \in dom vol) \to A \in dom vol$
73	65 72	syldan	$⊢ (φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \to A \in dom vol$
74	52 73 64 54	iblss	$⊢ (φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \to (y \in A ⟼ if (y \in A, ⦋ y / x ⦌ C, 0)) \in 𝐿^{1}$
75	51 74	eqeltrid	$⊢ (φ \land (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1}) \to (x \in A ⟼ C) \in 𝐿^{1}$
76	47 75	impbida	$⊢ φ \to ((x \in A ⟼ C) \in 𝐿^{1} \leftrightarrow (x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1})$
77	67	eleq2d	$⊢ φ \to (x \in (B ∖ (B ∖ A)) \leftrightarrow x \in A)$
78	77	biimpa	$⊢ (φ \land x \in (B ∖ (B ∖ A))) \to x \in A$
79	78 48	syl	$⊢ (φ \land x \in (B ∖ (B ∖ A))) \to if (x \in A, C, 0) = C$
80	59 4 36 3 79	itgeqa	$⊢ φ \to (((x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1} \leftrightarrow (x \in B ⟼ C) \in 𝐿^{1}) \land \int_{B} if (x \in A, C, 0) d x = \int_{B} C d x)$
81	80	simpld	$⊢ φ \to ((x \in B ⟼ if (x \in A, C, 0)) \in 𝐿^{1} \leftrightarrow (x \in B ⟼ C) \in 𝐿^{1})$
82	76 81	bitrd	$⊢ φ \to ((x \in A ⟼ C) \in 𝐿^{1} \leftrightarrow (x \in B ⟼ C) \in 𝐿^{1})$
83		itgss2	$⊢ A \subseteq B \to \int_{A} C d x = \int_{B} if (x \in A, C, 0) d x$
84	1 83	syl	$⊢ φ \to \int_{A} C d x = \int_{B} if (x \in A, C, 0) d x$
85	80	simprd	$⊢ φ \to \int_{B} if (x \in A, C, 0) d x = \int_{B} C d x$
86	84 85	eqtrd	$⊢ φ \to \int_{A} C d x = \int_{B} C d x$
87	82 86	jca	$⊢ φ \to (((x \in A ⟼ C) \in 𝐿^{1} \leftrightarrow (x \in B ⟼ C) \in 𝐿^{1}) \land \int_{A} C d x = \int_{B} C d x)$

Metamath Proof Explorer

Theorem itgss3

Proof