This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑥 ) )