MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2splitlem Structured version   Visualization version   GIF version

Theorem itg2splitlem 23234
Description: Lemma for itg2split 23235. (Contributed by Mario Carneiro, 11-Aug-2014.)
Hypotheses
Ref Expression
itg2split.a (𝜑𝐴 ∈ dom vol)
itg2split.b (𝜑𝐵 ∈ dom vol)
itg2split.i (𝜑 → (vol*‘(𝐴𝐵)) = 0)
itg2split.u (𝜑𝑈 = (𝐴𝐵))
itg2split.c ((𝜑𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
itg2split.f 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
itg2split.g 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
itg2split.h 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
itg2split.sf (𝜑 → (∫2𝐹) ∈ ℝ)
itg2split.sg (𝜑 → (∫2𝐺) ∈ ℝ)
Assertion
Ref Expression
itg2splitlem (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐵   𝑥,𝑈
Allowed substitution hints:   𝐶(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝐻(𝑥)

Proof of Theorem itg2splitlem
Dummy variables 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 789 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓 ∈ dom ∫1)
2 itg1cl 23171 . . . . . 6 (𝑓 ∈ dom ∫1 → (∫1𝑓) ∈ ℝ)
31, 2syl 17 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ∈ ℝ)
4 itg2split.a . . . . . . . . 9 (𝜑𝐴 ∈ dom vol)
54adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐴 ∈ dom vol)
6 eqid 2605 . . . . . . . . 9 (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))
76i1fres 23191 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝐴 ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1)
81, 5, 7syl2anc 690 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1)
9 itg1cl 23171 . . . . . . 7 ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ∈ ℝ)
108, 9syl 17 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ∈ ℝ)
11 itg2split.b . . . . . . . . 9 (𝜑𝐵 ∈ dom vol)
1211adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐵 ∈ dom vol)
13 eqid 2605 . . . . . . . . 9 (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))
1413i1fres 23191 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝐵 ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1)
151, 12, 14syl2anc 690 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1)
16 itg1cl 23171 . . . . . . 7 ((𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ∈ ℝ)
1715, 16syl 17 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ∈ ℝ)
1810, 17readdcld 9921 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) ∈ ℝ)
19 itg2split.sf . . . . . . 7 (𝜑 → (∫2𝐹) ∈ ℝ)
20 itg2split.sg . . . . . . 7 (𝜑 → (∫2𝐺) ∈ ℝ)
2119, 20readdcld 9921 . . . . . 6 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
2221adantr 479 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
23 inss1 3790 . . . . . . . . 9 (𝐴𝐵) ⊆ 𝐴
24 mblss 23019 . . . . . . . . . 10 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
254, 24syl 17 . . . . . . . . 9 (𝜑𝐴 ⊆ ℝ)
2623, 25syl5ss 3574 . . . . . . . 8 (𝜑 → (𝐴𝐵) ⊆ ℝ)
2726adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝐴𝐵) ⊆ ℝ)
28 itg2split.i . . . . . . . 8 (𝜑 → (vol*‘(𝐴𝐵)) = 0)
2928adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (vol*‘(𝐴𝐵)) = 0)
30 reex 9879 . . . . . . . . . . 11 ℝ ∈ V
3130a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ V)
32 fvex 6094 . . . . . . . . . . . 12 (𝑓𝑥) ∈ V
33 c0ex 9886 . . . . . . . . . . . 12 0 ∈ V
3432, 33ifex 4101 . . . . . . . . . . 11 if(𝑥𝐴, (𝑓𝑥), 0) ∈ V
3534a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, (𝑓𝑥), 0) ∈ V)
3632, 33ifex 4101 . . . . . . . . . . 11 if(𝑥𝐵, (𝑓𝑥), 0) ∈ V
3736a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, (𝑓𝑥), 0) ∈ V)
38 eqidd 2606 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)))
39 eqidd 2606 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))
4031, 35, 37, 38, 39offval2 6785 . . . . . . . . 9 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))))
4140adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))))
428, 15i1fadd 23181 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ∈ dom ∫1)
4341, 42eqeltrrd 2684 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))) ∈ dom ∫1)
44 i1ff 23162 . . . . . . . . . . . . . 14 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
451, 44syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓:ℝ⟶ℝ)
46 eldifi 3689 . . . . . . . . . . . . 13 (𝑦 ∈ (ℝ ∖ (𝐴𝐵)) → 𝑦 ∈ ℝ)
47 ffvelrn 6246 . . . . . . . . . . . . 13 ((𝑓:ℝ⟶ℝ ∧ 𝑦 ∈ ℝ) → (𝑓𝑦) ∈ ℝ)
4845, 46, 47syl2an 492 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ∈ ℝ)
4948leidd 10439 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ (𝑓𝑦))
5049adantr 479 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (𝑓𝑦) ≤ (𝑓𝑦))
51 iftrue 4037 . . . . . . . . . . . . 13 (𝑦𝐴 → if(𝑦𝐴, (𝑓𝑦), 0) = (𝑓𝑦))
5251adantl 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → if(𝑦𝐴, (𝑓𝑦), 0) = (𝑓𝑦))
53 eldifn 3690 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (ℝ ∖ (𝐴𝐵)) → ¬ 𝑦 ∈ (𝐴𝐵))
5453adantl 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ 𝑦 ∈ (𝐴𝐵))
55 elin 3753 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
5654, 55sylnib 316 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ (𝑦𝐴𝑦𝐵))
57 imnan 436 . . . . . . . . . . . . . . 15 ((𝑦𝐴 → ¬ 𝑦𝐵) ↔ ¬ (𝑦𝐴𝑦𝐵))
5856, 57sylibr 222 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑦𝐴 → ¬ 𝑦𝐵))
5958imp 443 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → ¬ 𝑦𝐵)
60 iffalse 4040 . . . . . . . . . . . . 13 𝑦𝐵 → if(𝑦𝐵, (𝑓𝑦), 0) = 0)
6159, 60syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → if(𝑦𝐵, (𝑓𝑦), 0) = 0)
6252, 61oveq12d 6541 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = ((𝑓𝑦) + 0))
6348recnd 9920 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ∈ ℂ)
6463adantr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (𝑓𝑦) ∈ ℂ)
6564addid1d 10083 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → ((𝑓𝑦) + 0) = (𝑓𝑦))
6662, 65eqtrd 2639 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = (𝑓𝑦))
6750, 66breqtrrd 4601 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (𝑓𝑦) ≤ (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
6849ad2antrr 757 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ 𝑦𝐵) → (𝑓𝑦) ≤ (𝑓𝑦))
69 iftrue 4037 . . . . . . . . . . . . 13 (𝑦𝐵 → if(𝑦𝐵, (𝑓𝑦), 0) = (𝑓𝑦))
7069adantl 480 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ 𝑦𝐵) → if(𝑦𝐵, (𝑓𝑦), 0) = (𝑓𝑦))
7168, 70breqtrrd 4601 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ 𝑦𝐵) → (𝑓𝑦) ≤ if(𝑦𝐵, (𝑓𝑦), 0))
72 itg2split.u . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 = (𝐴𝐵))
7372ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → 𝑈 = (𝐴𝐵))
7473eleq2d 2668 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑦𝑈𝑦 ∈ (𝐴𝐵)))
75 elun 3710 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
7674, 75syl6bb 274 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑦𝑈 ↔ (𝑦𝐴𝑦𝐵)))
7776notbid 306 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (¬ 𝑦𝑈 ↔ ¬ (𝑦𝐴𝑦𝐵)))
78 ioran 509 . . . . . . . . . . . . . . . 16 (¬ (𝑦𝐴𝑦𝐵) ↔ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵))
7977, 78syl6bb 274 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (¬ 𝑦𝑈 ↔ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵)))
8079biimpar 500 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵)) → ¬ 𝑦𝑈)
81 simprr 791 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓𝑟𝐻)
82 ffn 5940 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:ℝ⟶ℝ → 𝑓 Fn ℝ)
8345, 82syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓 Fn ℝ)
84 itg2split.c . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
8584adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
86 0e0iccpnf 12106 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ (0[,]+∞)
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝑈) → 0 ∈ (0[,]+∞))
8885, 87ifclda 4065 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
89 itg2split.h . . . . . . . . . . . . . . . . . . . . . . 23 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
9088, 89fmptd 6273 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐻:ℝ⟶(0[,]+∞))
91 ffn 5940 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻:ℝ⟶(0[,]+∞) → 𝐻 Fn ℝ)
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐻 Fn ℝ)
9392adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐻 Fn ℝ)
9430a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ℝ ∈ V)
95 inidm 3779 . . . . . . . . . . . . . . . . . . . 20 (ℝ ∩ ℝ) = ℝ
96 eqidd 2606 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓𝑦) = (𝑓𝑦))
97 eqidd 2606 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ ℝ) → (𝐻𝑦) = (𝐻𝑦))
9883, 93, 94, 94, 95, 96, 97ofrfval 6776 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑓𝑟𝐻 ↔ ∀𝑦 ∈ ℝ (𝑓𝑦) ≤ (𝐻𝑦)))
9981, 98mpbid 220 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑦 ∈ ℝ (𝑓𝑦) ≤ (𝐻𝑦))
10099r19.21bi 2911 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓𝑦) ≤ (𝐻𝑦))
10146, 100sylan2 489 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ (𝐻𝑦))
102101adantr 479 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝑈) → (𝑓𝑦) ≤ (𝐻𝑦))
10346adantl 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → 𝑦 ∈ ℝ)
104 eldif 3545 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (ℝ ∖ 𝑈) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦𝑈))
105 nfcv 2746 . . . . . . . . . . . . . . . . . 18 𝑥𝑦
106 nfmpt1 4665 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
10789, 106nfcxfr 2744 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐻
108107, 105nffv 6091 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐻𝑦)
109108nfeq1 2759 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑦) = 0
110 fveq2 6084 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
111110eqeq1d 2607 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐻𝑥) = 0 ↔ (𝐻𝑦) = 0))
112 eldif 3545 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (ℝ ∖ 𝑈) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥𝑈))
11389fvmpt2i 6180 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → (𝐻𝑥) = ( I ‘if(𝑥𝑈, 𝐶, 0)))
114 iffalse 4040 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝑈 → if(𝑥𝑈, 𝐶, 0) = 0)
115114fveq2d 6088 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑈 → ( I ‘if(𝑥𝑈, 𝐶, 0)) = ( I ‘0))
116 0cn 9884 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
117 fvi 6146 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ ℂ → ( I ‘0) = 0)
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ( I ‘0) = 0
119115, 118syl6eq 2655 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑈 → ( I ‘if(𝑥𝑈, 𝐶, 0)) = 0)
120113, 119sylan9eq 2659 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ ∧ ¬ 𝑥𝑈) → (𝐻𝑥) = 0)
121112, 120sylbi 205 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (ℝ ∖ 𝑈) → (𝐻𝑥) = 0)
122105, 109, 111, 121vtoclgaf 3239 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (ℝ ∖ 𝑈) → (𝐻𝑦) = 0)
123104, 122sylbir 223 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ ∧ ¬ 𝑦𝑈) → (𝐻𝑦) = 0)
124103, 123sylan 486 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝑈) → (𝐻𝑦) = 0)
125102, 124breqtrd 4599 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝑈) → (𝑓𝑦) ≤ 0)
12680, 125syldan 485 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵)) → (𝑓𝑦) ≤ 0)
127126anassrs 677 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ ¬ 𝑦𝐵) → (𝑓𝑦) ≤ 0)
12860adantl 480 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ ¬ 𝑦𝐵) → if(𝑦𝐵, (𝑓𝑦), 0) = 0)
129127, 128breqtrrd 4601 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ ¬ 𝑦𝐵) → (𝑓𝑦) ≤ if(𝑦𝐵, (𝑓𝑦), 0))
13071, 129pm2.61dan 827 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (𝑓𝑦) ≤ if(𝑦𝐵, (𝑓𝑦), 0))
131 iffalse 4040 . . . . . . . . . . . . 13 𝑦𝐴 → if(𝑦𝐴, (𝑓𝑦), 0) = 0)
132131adantl 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → if(𝑦𝐴, (𝑓𝑦), 0) = 0)
133132oveq1d 6538 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = (0 + if(𝑦𝐵, (𝑓𝑦), 0)))
134 0re 9892 . . . . . . . . . . . . . . 15 0 ∈ ℝ
135 ifcl 4075 . . . . . . . . . . . . . . 15 (((𝑓𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℝ)
13648, 134, 135sylancl 692 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℝ)
137136recnd 9920 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℂ)
138137adantr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℂ)
139138addid2d 10084 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (0 + if(𝑦𝐵, (𝑓𝑦), 0)) = if(𝑦𝐵, (𝑓𝑦), 0))
140133, 139eqtrd 2639 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = if(𝑦𝐵, (𝑓𝑦), 0))
141130, 140breqtrrd 4601 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (𝑓𝑦) ≤ (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
14267, 141pm2.61dan 827 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
143 eleq1 2671 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
144 fveq2 6084 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑓𝑥) = (𝑓𝑦))
145143, 144ifbieq1d 4054 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥𝐴, (𝑓𝑥), 0) = if(𝑦𝐴, (𝑓𝑦), 0))
146 eleq1 2671 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
147146, 144ifbieq1d 4054 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥𝐵, (𝑓𝑥), 0) = if(𝑦𝐵, (𝑓𝑦), 0))
148145, 147oveq12d 6541 . . . . . . . . . 10 (𝑥 = 𝑦 → (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)) = (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
149 eqid 2605 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))
150 ovex 6551 . . . . . . . . . 10 (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) ∈ V
151148, 149, 150fvmpt 6172 . . . . . . . . 9 (𝑦 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))‘𝑦) = (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
152103, 151syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ((𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))‘𝑦) = (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
153142, 152breqtrrd 4601 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ ((𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))‘𝑦))
1541, 27, 29, 43, 153itg1lea 23198 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ≤ (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))))
15541fveq2d 6088 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))))
1568, 15itg1add 23187 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))))
157155, 156eqtr3d 2641 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))))
158154, 157breqtrd 4599 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ≤ ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))))
15919adantr 479 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫2𝐹) ∈ ℝ)
16020adantr 479 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫2𝐺) ∈ ℝ)
161 ssun1 3733 . . . . . . . . . . . . . 14 𝐴 ⊆ (𝐴𝐵)
162161, 72syl5sseqr 3612 . . . . . . . . . . . . 13 (𝜑𝐴𝑈)
163162sselda 3563 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑥𝑈)
164163adantlr 746 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥𝑈)
165164, 85syldan 485 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝐶 ∈ (0[,]+∞))
16686a1i 11 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
167165, 166ifclda 4065 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
168 itg2split.f . . . . . . . . 9 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
169167, 168fmptd 6273 . . . . . . . 8 (𝜑𝐹:ℝ⟶(0[,]+∞))
170169adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐹:ℝ⟶(0[,]+∞))
171 nfv 1828 . . . . . . . . . 10 𝑥𝜑
172 nfv 1828 . . . . . . . . . . 11 𝑥 𝑓 ∈ dom ∫1
173 nfcv 2746 . . . . . . . . . . . 12 𝑥𝑓
174 nfcv 2746 . . . . . . . . . . . 12 𝑥𝑟
175173, 174, 107nfbr 4619 . . . . . . . . . . 11 𝑥 𝑓𝑟𝐻
176172, 175nfan 1814 . . . . . . . . . 10 𝑥(𝑓 ∈ dom ∫1𝑓𝑟𝐻)
177171, 176nfan 1814 . . . . . . . . 9 𝑥(𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻))
1785, 24syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐴 ⊆ ℝ)
179178sselda 3563 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → 𝑥 ∈ ℝ)
18030a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → ℝ ∈ V)
18132a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ V)
18288adantlr 746 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
18344adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ)
184183feqmptd 6140 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
18589a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0)))
186180, 181, 182, 184, 185ofrfval2 6786 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐻 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0)))
187186biimpd 217 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐻 → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0)))
188187impr 646 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
189188r19.21bi 2911 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
190179, 189syldan 485 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
191163adantlr 746 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → 𝑥𝑈)
192191iftrued 4039 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
193190, 192breqtrd 4599 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ 𝐶)
194 iftrue 4037 . . . . . . . . . . . . 13 (𝑥𝐴 → if(𝑥𝐴, (𝑓𝑥), 0) = (𝑓𝑥))
195194adantl 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝐴, (𝑓𝑥), 0) = (𝑓𝑥))
196 iftrue 4037 . . . . . . . . . . . . 13 (𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 𝐶)
197196adantl 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 𝐶)
198193, 195, 1973brtr4d 4605 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
199 0le0 10953 . . . . . . . . . . . . . 14 0 ≤ 0
200199a1i 11 . . . . . . . . . . . . 13 𝑥𝐴 → 0 ≤ 0)
201 iffalse 4040 . . . . . . . . . . . . 13 𝑥𝐴 → if(𝑥𝐴, (𝑓𝑥), 0) = 0)
202 iffalse 4040 . . . . . . . . . . . . 13 𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 0)
203200, 201, 2023brtr4d 4605 . . . . . . . . . . . 12 𝑥𝐴 → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
204203adantl 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ ¬ 𝑥𝐴) → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
205198, 204pm2.61dan 827 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
206205a1d 25 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0)))
207177, 206ralrimi 2935 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑥 ∈ ℝ if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
208168a1i 11 . . . . . . . . . 10 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0)))
20931, 35, 167, 38, 208ofrfval2 6786 . . . . . . . . 9 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0)))
210209adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0)))
211207, 210mpbird 245 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹)
212 itg2ub 23219 . . . . . . 7 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ≤ (∫2𝐹))
213170, 8, 211, 212syl3anc 1317 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ≤ (∫2𝐹))
214 ssun2 3734 . . . . . . . . . . . . . 14 𝐵 ⊆ (𝐴𝐵)
215214, 72syl5sseqr 3612 . . . . . . . . . . . . 13 (𝜑𝐵𝑈)
216215sselda 3563 . . . . . . . . . . . 12 ((𝜑𝑥𝐵) → 𝑥𝑈)
217216adantlr 746 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥𝑈)
218217, 85syldan 485 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
21986a1i 11 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐵) → 0 ∈ (0[,]+∞))
220218, 219ifclda 4065 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
221 itg2split.g . . . . . . . . 9 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
222220, 221fmptd 6273 . . . . . . . 8 (𝜑𝐺:ℝ⟶(0[,]+∞))
223222adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐺:ℝ⟶(0[,]+∞))
224 mblss 23019 . . . . . . . . . . . . . . . 16 (𝐵 ∈ dom vol → 𝐵 ⊆ ℝ)
22512, 224syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐵 ⊆ ℝ)
226225sselda 3563 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → 𝑥 ∈ ℝ)
227226, 189syldan 485 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
228216adantlr 746 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → 𝑥𝑈)
229228iftrued 4039 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
230227, 229breqtrd 4599 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → (𝑓𝑥) ≤ 𝐶)
231 iftrue 4037 . . . . . . . . . . . . 13 (𝑥𝐵 → if(𝑥𝐵, (𝑓𝑥), 0) = (𝑓𝑥))
232231adantl 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝐵, (𝑓𝑥), 0) = (𝑓𝑥))
233 iftrue 4037 . . . . . . . . . . . . 13 (𝑥𝐵 → if(𝑥𝐵, 𝐶, 0) = 𝐶)
234233adantl 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝐵, 𝐶, 0) = 𝐶)
235230, 232, 2343brtr4d 4605 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
236199a1i 11 . . . . . . . . . . . . 13 𝑥𝐵 → 0 ≤ 0)
237 iffalse 4040 . . . . . . . . . . . . 13 𝑥𝐵 → if(𝑥𝐵, (𝑓𝑥), 0) = 0)
238 iffalse 4040 . . . . . . . . . . . . 13 𝑥𝐵 → if(𝑥𝐵, 𝐶, 0) = 0)
239236, 237, 2383brtr4d 4605 . . . . . . . . . . . 12 𝑥𝐵 → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
240239adantl 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ ¬ 𝑥𝐵) → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
241235, 240pm2.61dan 827 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
242241a1d 25 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0)))
243177, 242ralrimi 2935 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑥 ∈ ℝ if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
244221a1i 11 . . . . . . . . . 10 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0)))
24531, 37, 220, 39, 244ofrfval2 6786 . . . . . . . . 9 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0)))
246245adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0)))
247243, 246mpbird 245 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺)
248 itg2ub 23219 . . . . . . 7 ((𝐺:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ≤ (∫2𝐺))
249223, 15, 247, 248syl3anc 1317 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ≤ (∫2𝐺))
25010, 17, 159, 160, 213, 249le2addd 10491 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) ≤ ((∫2𝐹) + (∫2𝐺)))
2513, 18, 22, 158, 250letrd 10041 . . . 4 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺)))
252251expr 640 . . 3 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺))))
253252ralrimiva 2944 . 2 (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺))))
25421rexrd 9941 . . 3 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ*)
255 itg2leub 23220 . . 3 ((𝐻:ℝ⟶(0[,]+∞) ∧ ((∫2𝐹) + (∫2𝐺)) ∈ ℝ*) → ((∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺)))))
25690, 254, 255syl2anc 690 . 2 (𝜑 → ((∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺)))))
257253, 256mpbird 245 1 (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1975  wral 2891  Vcvv 3168  cdif 3532  cun 3533  cin 3534  wss 3535  ifcif 4031   class class class wbr 4573  cmpt 4633   I cid 4934  dom cdm 5024   Fn wfn 5781  wf 5782  cfv 5786  (class class class)co 6523  𝑓 cof 6766  𝑟 cofr 6767  cc 9786  cr 9787  0cc0 9788   + caddc 9791  +∞cpnf 9923  *cxr 9925  cle 9927  [,]cicc 12001  vol*covol 22951  volcvol 22952  1citg1 23103  2citg2 23104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-inf2 8394  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865  ax-pre-sup 9866  ax-addf 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-disj 4544  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-se 4984  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-isom 5795  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-of 6768  df-ofr 6769  df-om 6931  df-1st 7032  df-2nd 7033  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-2o 7421  df-oadd 7424  df-er 7602  df-map 7719  df-pm 7720  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-fi 8173  df-sup 8204  df-inf 8205  df-oi 8271  df-card 8621  df-cda 8846  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-div 10530  df-nn 10864  df-2 10922  df-3 10923  df-n0 11136  df-z 11207  df-uz 11516  df-q 11617  df-rp 11661  df-xneg 11774  df-xadd 11775  df-xmul 11776  df-ioo 12002  df-ico 12004  df-icc 12005  df-fz 12149  df-fzo 12286  df-fl 12406  df-seq 12615  df-exp 12674  df-hash 12931  df-cj 13629  df-re 13630  df-im 13631  df-sqrt 13765  df-abs 13766  df-clim 14009  df-sum 14207  df-rest 15848  df-topgen 15869  df-psmet 19501  df-xmet 19502  df-met 19503  df-bl 19504  df-mopn 19505  df-top 20459  df-bases 20460  df-topon 20461  df-cmp 20938  df-ovol 22953  df-vol 22954  df-mbf 23107  df-itg1 23108  df-itg2 23109
This theorem is referenced by:  itg2split  23235
  Copyright terms: Public domain W3C validator