Step | Hyp | Ref
| Expression |
1 | | isibl.1 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))) |
2 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
3 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥0 |
4 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥
≤ |
5 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥ℜ |
6 | | nffvmpt1 6199 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) |
7 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑥
/ |
8 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(i↑𝑘) |
9 | 6, 7, 8 | nfov 6676 |
. . . . . . . . 9
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)) |
10 | 5, 9 | nffv 6198 |
. . . . . . . 8
⊢
Ⅎ𝑥(ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))) |
11 | 3, 4, 10 | nfbr 4699 |
. . . . . . 7
⊢
Ⅎ𝑥0 ≤
(ℜ‘(((𝑥 ∈
𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))) |
12 | 2, 11 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)))) |
13 | 12, 10, 3 | nfif 4115 |
. . . . 5
⊢
Ⅎ𝑥if((𝑦 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))), 0) |
14 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑦if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘))), 0) |
15 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
16 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
17 | 16 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)) = (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘))) |
18 | 17 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))) = (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘)))) |
19 | 18 | breq2d 4665 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))) ↔ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘))))) |
20 | 15, 19 | anbi12d 747 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)))) ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘)))))) |
21 | 20, 18 | ifbieq1d 4109 |
. . . . 5
⊢ (𝑦 = 𝑥 → if((𝑦 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘))), 0)) |
22 | 13, 14, 21 | cbvmpt 4749 |
. . . 4
⊢ (𝑦 ∈ ℝ ↦
if((𝑦 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(((𝑥 ∈
𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘))), 0)) |
23 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
24 | | isibl2.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
25 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
26 | 25 | fvmpt2 6291 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
27 | 23, 24, 26 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
28 | 27 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘)) = (𝐵 / (i↑𝑘))) |
29 | 28 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘)))) |
30 | | isibl.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝑘)))) |
31 | 29, 30 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘))) = 𝑇) |
32 | 31 | ibllem 23531 |
. . . . 5
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘))), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)) |
33 | 32 | mpteq2dv 4745 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))) |
34 | 22, 33 | syl5eq 2668 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if((𝑦 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))) |
35 | 1, 34 | eqtr4d 2659 |
. 2
⊢ (𝜑 → 𝐺 = (𝑦 ∈ ℝ ↦ if((𝑦 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)))), (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))), 0))) |
36 | | eqidd 2623 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘))) = (ℜ‘(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) / (i↑𝑘)))) |
37 | 25, 24 | dmmptd 6024 |
. 2
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
38 | | eqidd 2623 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)) |
39 | 35, 36, 37, 38 | isibl 23532 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘𝐺) ∈ ℝ))) |