Step | Hyp | Ref
| Expression |
1 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑦if(𝑥 ∈ 𝐴, 𝐶, 0) |
2 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
3 | | nfcsb1v 3515 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶 |
4 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥0 |
5 | 2, 3, 4 | nfif 4065 |
. . . . . 6
⊢
Ⅎ𝑥if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0) |
6 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
7 | | csbeq1a 3508 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶) |
8 | 6, 7 | ifbieq1d 4059 |
. . . . . 6
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ 𝐴, 𝐶, 0) = if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) |
9 | 1, 5, 8 | cbvmpt 4677 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) |
10 | | itgss3.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) → 𝐴 ⊆ 𝐵) |
12 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝐶 |
13 | 12, 3, 7 | cbvmpt 4677 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) |
14 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐴 → if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0) = ⦋𝑦 / 𝑥⦌𝐶) |
15 | 14 | mpteq2ia 4668 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) |
16 | 13, 15 | eqtr4i 2635 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) |
17 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) →
(𝑥 ∈ 𝐴 ↦ 𝐶) ∈
𝐿1) |
18 | 16, 17 | syl5eqelr 2693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) →
(𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈
𝐿1) |
19 | | iblmbf 23340 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈ 𝐿1 →
(𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈ MblFn) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) →
(𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈ MblFn) |
21 | 10 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
22 | | itgss3.4 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ) |
23 | 21, 22 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
24 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
25 | 23, 24 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ) |
26 | 25 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) →
(𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ) |
27 | 16 | feq1i 5949 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ ↔ (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)):𝐴⟶ℂ) |
28 | 26, 27 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) →
(𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)):𝐴⟶ℂ) |
29 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) = (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) |
30 | 29 | fmpt 6289 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐴 if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0) ∈ ℂ ↔ (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)):𝐴⟶ℂ) |
31 | 28, 30 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) →
∀𝑦 ∈ 𝐴 if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0) ∈ ℂ) |
32 | 31 | r19.21bi 2916 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) ∧ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0) ∈ ℂ) |
33 | 20, 32 | mbfdm2 23211 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) → 𝐴 ∈ dom
vol) |
34 | | undif 4001 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) |
35 | 10, 34 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) |
36 | 35 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ dom vol) → (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) |
37 | | id 22 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom vol → 𝐴 ∈ dom
vol) |
38 | | itgss3.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
39 | 38 | ssdifssd 3710 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∖ 𝐴) ⊆ ℝ) |
40 | | itgss3.3 |
. . . . . . . . . 10
⊢ (𝜑 → (vol*‘(𝐵 ∖ 𝐴)) = 0) |
41 | | nulmbl 23110 |
. . . . . . . . . 10
⊢ (((𝐵 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐵 ∖ 𝐴)) = 0) → (𝐵 ∖ 𝐴) ∈ dom vol) |
42 | 39, 40, 41 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∖ 𝐴) ∈ dom vol) |
43 | | unmbl 23112 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ (𝐵 ∖ 𝐴) ∈ dom vol) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ∈ dom vol) |
44 | 37, 42, 43 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ dom vol) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ∈ dom vol) |
45 | 36, 44 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ dom vol) → 𝐵 ∈ dom vol) |
46 | 33, 45 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) → 𝐵 ∈ dom
vol) |
47 | | eldifn 3695 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐵 ∖ 𝐴) → ¬ 𝑦 ∈ 𝐴) |
48 | 47 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) ∧ 𝑦 ∈ (𝐵 ∖ 𝐴)) → ¬ 𝑦 ∈ 𝐴) |
49 | 48 | iffalsed 4047 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) ∧ 𝑦 ∈ (𝐵 ∖ 𝐴)) → if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0) = 0) |
50 | 11, 46, 32, 49, 18 | iblss2 23378 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) →
(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈
𝐿1) |
51 | 9, 50 | syl5eqel 2692 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) →
(𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈
𝐿1) |
52 | | iftrue 4042 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
53 | 52 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
54 | 1, 5, 8 | cbvmpt 4677 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) |
55 | 53, 54 | eqtr3i 2634 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) |
56 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
𝐴 ⊆ 𝐵) |
57 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
(𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈
𝐿1) |
58 | 9, 57 | syl5eqelr 2693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈
𝐿1) |
59 | | iblmbf 23340 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈ 𝐿1 →
(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈ MblFn) |
60 | 58, 59 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈ MblFn) |
61 | | 0cn 9911 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℂ |
62 | | ifcl 4080 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ ℂ ∧ 0 ∈
ℂ) → if(𝑥 ∈
𝐴, 𝐶, 0) ∈ ℂ) |
63 | 22, 61, 62 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ ℂ) |
64 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
65 | 63, 64 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)):𝐵⟶ℂ) |
66 | 9 | feq1i 5949 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)):𝐵⟶ℂ ↔ (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)):𝐵⟶ℂ) |
67 | 65, 66 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)):𝐵⟶ℂ) |
68 | 67 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)):𝐵⟶ℂ) |
69 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) |
70 | 69 | fmpt 6289 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐵 if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0) ∈ ℂ ↔ (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)):𝐵⟶ℂ) |
71 | 68, 70 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
∀𝑦 ∈ 𝐵 if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0) ∈ ℂ) |
72 | 71 | r19.21bi 2916 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) ∧
𝑦 ∈ 𝐵) → if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0) ∈ ℂ) |
73 | 60, 72 | mbfdm2 23211 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
𝐵 ∈ dom
vol) |
74 | | dfss4 3820 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
75 | 10, 74 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
76 | 75 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ dom vol) → (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
77 | | id 22 |
. . . . . . . . 9
⊢ (𝐵 ∈ dom vol → 𝐵 ∈ dom
vol) |
78 | | difmbl 23118 |
. . . . . . . . 9
⊢ ((𝐵 ∈ dom vol ∧ (𝐵 ∖ 𝐴) ∈ dom vol) → (𝐵 ∖ (𝐵 ∖ 𝐴)) ∈ dom vol) |
79 | 77, 42, 78 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ dom vol) → (𝐵 ∖ (𝐵 ∖ 𝐴)) ∈ dom vol) |
80 | 76, 79 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ dom vol) → 𝐴 ∈ dom vol) |
81 | 73, 80 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
𝐴 ∈ dom
vol) |
82 | 56, 81, 72, 58 | iblss 23377 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
(𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, ⦋𝑦 / 𝑥⦌𝐶, 0)) ∈
𝐿1) |
83 | 55, 82 | syl5eqel 2692 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1) →
(𝑥 ∈ 𝐴 ↦ 𝐶) ∈
𝐿1) |
84 | 51, 83 | impbida 873 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔ (𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈
𝐿1)) |
85 | 75 | eleq2d 2673 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐵 ∖ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ 𝐴)) |
86 | 85 | biimpa 500 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐵 ∖ 𝐴))) → 𝑥 ∈ 𝐴) |
87 | 86, 52 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐵 ∖ 𝐴))) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
88 | 63, 22, 39, 40, 87 | itgeqa 23386 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1 ↔
(𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1) ∧
∫𝐵if(𝑥 ∈ 𝐴, 𝐶, 0) d𝑥 = ∫𝐵𝐶 d𝑥)) |
89 | 88 | simpld 474 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ 𝐿1 ↔
(𝑥 ∈ 𝐵 ↦ 𝐶) ∈
𝐿1)) |
90 | 84, 89 | bitrd 267 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔ (𝑥 ∈ 𝐵 ↦ 𝐶) ∈
𝐿1)) |
91 | | itgss2 23385 |
. . . 4
⊢ (𝐴 ⊆ 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵if(𝑥 ∈ 𝐴, 𝐶, 0) d𝑥) |
92 | 10, 91 | syl 17 |
. . 3
⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵if(𝑥 ∈ 𝐴, 𝐶, 0) d𝑥) |
93 | 88 | simprd 478 |
. . 3
⊢ (𝜑 → ∫𝐵if(𝑥 ∈ 𝐴, 𝐶, 0) d𝑥 = ∫𝐵𝐶 d𝑥) |
94 | 92, 93 | eqtrd 2644 |
. 2
⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥) |
95 | 90, 94 | jca 553 |
1
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔ (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1) ∧
∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)) |