Theorem 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	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	itgss3.2	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
	itgss3.3	⊢ ( 𝜑 → ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) = 0 )
	itgss3.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
Assertion	itgss3	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 ) ∧ ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 ) )

Proof

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