Metamath Proof Explorer


Theorem iblss2

Description: Change the domain of an integrability predicate. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses iblss2.1 φ A B
iblss2.2 φ B dom vol
iblss2.3 φ x A C V
iblss2.4 φ x B A C = 0
iblss2.5 φ x A C 𝐿 1
Assertion iblss2 φ x B C 𝐿 1

Proof

Step Hyp Ref Expression
1 iblss2.1 φ A B
2 iblss2.2 φ B dom vol
3 iblss2.3 φ x A C V
4 iblss2.4 φ x B A C = 0
5 iblss2.5 φ x A C 𝐿 1
6 iblmbf x A C 𝐿 1 x A C MblFn
7 5 6 syl φ x A C MblFn
8 1 2 3 4 7 mbfss φ x B C MblFn
9 1 adantr φ k 0 3 A B
10 9 sselda φ k 0 3 x A x B
11 10 iftrued φ k 0 3 x A if x B if 0 C i k C i k 0 0 = if 0 C i k C i k 0
12 iftrue x A if x A if 0 C i k C i k 0 0 = if 0 C i k C i k 0
13 12 adantl φ k 0 3 x A if x A if 0 C i k C i k 0 0 = if 0 C i k C i k 0
14 11 13 eqtr4d φ k 0 3 x A if x B if 0 C i k C i k 0 0 = if x A if 0 C i k C i k 0 0
15 ifid if x B 0 0 = 0
16 simplll φ k 0 3 ¬ x A x B φ
17 simpr φ k 0 3 ¬ x A x B x B
18 simplr φ k 0 3 ¬ x A x B ¬ x A
19 17 18 eldifd φ k 0 3 ¬ x A x B x B A
20 16 19 4 syl2anc φ k 0 3 ¬ x A x B C = 0
21 20 oveq1d φ k 0 3 ¬ x A x B C i k = 0 i k
22 simpllr φ k 0 3 ¬ x A x B k 0 3
23 elfzelz k 0 3 k
24 ax-icn i
25 ine0 i 0
26 expclz i i 0 k i k
27 expne0i i i 0 k i k 0
28 26 27 div0d i i 0 k 0 i k = 0
29 24 25 28 mp3an12 k 0 i k = 0
30 22 23 29 3syl φ k 0 3 ¬ x A x B 0 i k = 0
31 21 30 eqtrd φ k 0 3 ¬ x A x B C i k = 0
32 31 fveq2d φ k 0 3 ¬ x A x B C i k = 0
33 re0 0 = 0
34 32 33 eqtrdi φ k 0 3 ¬ x A x B C i k = 0
35 34 ifeq1d φ k 0 3 ¬ x A x B if 0 C i k C i k 0 = if 0 C i k 0 0
36 ifid if 0 C i k 0 0 = 0
37 35 36 eqtrdi φ k 0 3 ¬ x A x B if 0 C i k C i k 0 = 0
38 37 ifeq1da φ k 0 3 ¬ x A if x B if 0 C i k C i k 0 0 = if x B 0 0
39 iffalse ¬ x A if x A if 0 C i k C i k 0 0 = 0
40 39 adantl φ k 0 3 ¬ x A if x A if 0 C i k C i k 0 0 = 0
41 15 38 40 3eqtr4a φ k 0 3 ¬ x A if x B if 0 C i k C i k 0 0 = if x A if 0 C i k C i k 0 0
42 14 41 pm2.61dan φ k 0 3 if x B if 0 C i k C i k 0 0 = if x A if 0 C i k C i k 0 0
43 ifan if x B 0 C i k C i k 0 = if x B if 0 C i k C i k 0 0
44 ifan if x A 0 C i k C i k 0 = if x A if 0 C i k C i k 0 0
45 42 43 44 3eqtr4g φ k 0 3 if x B 0 C i k C i k 0 = if x A 0 C i k C i k 0
46 45 mpteq2dv φ k 0 3 x if x B 0 C i k C i k 0 = x if x A 0 C i k C i k 0
47 46 fveq2d φ k 0 3 2 x if x B 0 C i k C i k 0 = 2 x if x A 0 C i k C i k 0
48 eqidd φ x if x A 0 C i k C i k 0 = x if x A 0 C i k C i k 0
49 eqidd φ x A C i k = C i k
50 48 49 5 3 iblitg φ k 2 x if x A 0 C i k C i k 0
51 23 50 sylan2 φ k 0 3 2 x if x A 0 C i k C i k 0
52 47 51 eqeltrd φ k 0 3 2 x if x B 0 C i k C i k 0
53 52 ralrimiva φ k 0 3 2 x if x B 0 C i k C i k 0
54 eqidd φ x if x B 0 C i k C i k 0 = x if x B 0 C i k C i k 0
55 eqidd φ x B C i k = C i k
56 elun x A B A x A x B A
57 undif2 A B A = A B
58 ssequn1 A B A B = B
59 1 58 sylib φ A B = B
60 57 59 syl5eq φ A B A = B
61 60 eleq2d φ x A B A x B
62 56 61 bitr3id φ x A x B A x B
63 62 biimpar φ x B x A x B A
64 7 3 mbfmptcl φ x A C
65 0cn 0
66 4 65 eqeltrdi φ x B A C
67 64 66 jaodan φ x A x B A C
68 63 67 syldan φ x B C
69 54 55 68 isibl2 φ x B C 𝐿 1 x B C MblFn k 0 3 2 x if x B 0 C i k C i k 0
70 8 53 69 mpbir2and φ x B C 𝐿 1