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

Theorem itg2splitlem 23321
 Description: Lemma for itg2split 23322. (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 790 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓 ∈ dom ∫1)
2 itg1cl 23258 . . . . . 6 (𝑓 ∈ dom ∫1 → (∫1𝑓) ∈ ℝ)
31, 2syl 17 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ∈ ℝ)
4 itg2split.a . . . . . . . . 9 (𝜑𝐴 ∈ dom vol)
54adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐴 ∈ dom vol)
6 eqid 2610 . . . . . . . . 9 (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))
76i1fres 23278 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝐴 ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1)
81, 5, 7syl2anc 691 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1)
9 itg1cl 23258 . . . . . . 7 ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ∈ ℝ)
108, 9syl 17 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ∈ ℝ)
11 itg2split.b . . . . . . . . 9 (𝜑𝐵 ∈ dom vol)
1211adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐵 ∈ dom vol)
13 eqid 2610 . . . . . . . . 9 (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))
1413i1fres 23278 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝐵 ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1)
151, 12, 14syl2anc 691 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1)
16 itg1cl 23258 . . . . . . 7 ((𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ∈ ℝ)
1715, 16syl 17 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ∈ ℝ)
1810, 17readdcld 9948 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) ∈ ℝ)
19 itg2split.sf . . . . . . 7 (𝜑 → (∫2𝐹) ∈ ℝ)
20 itg2split.sg . . . . . . 7 (𝜑 → (∫2𝐺) ∈ ℝ)
2119, 20readdcld 9948 . . . . . 6 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
2221adantr 480 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ)
23 inss1 3795 . . . . . . . . 9 (𝐴𝐵) ⊆ 𝐴
24 mblss 23106 . . . . . . . . . 10 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
254, 24syl 17 . . . . . . . . 9 (𝜑𝐴 ⊆ ℝ)
2623, 25syl5ss 3579 . . . . . . . 8 (𝜑 → (𝐴𝐵) ⊆ ℝ)
2726adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝐴𝐵) ⊆ ℝ)
28 itg2split.i . . . . . . . 8 (𝜑 → (vol*‘(𝐴𝐵)) = 0)
2928adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (vol*‘(𝐴𝐵)) = 0)
30 reex 9906 . . . . . . . . . . 11 ℝ ∈ V
3130a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ V)
32 fvex 6113 . . . . . . . . . . . 12 (𝑓𝑥) ∈ V
33 c0ex 9913 . . . . . . . . . . . 12 0 ∈ V
3432, 33ifex 4106 . . . . . . . . . . 11 if(𝑥𝐴, (𝑓𝑥), 0) ∈ V
3534a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, (𝑓𝑥), 0) ∈ V)
3632, 33ifex 4106 . . . . . . . . . . 11 if(𝑥𝐵, (𝑓𝑥), 0) ∈ V
3736a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, (𝑓𝑥), 0) ∈ V)
38 eqidd 2611 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)))
39 eqidd 2611 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))
4031, 35, 37, 38, 39offval2 6812 . . . . . . . . 9 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))))
4140adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))))
428, 15i1fadd 23268 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ∈ dom ∫1)
4341, 42eqeltrrd 2689 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))) ∈ dom ∫1)
44 i1ff 23249 . . . . . . . . . . . . . 14 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
451, 44syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓:ℝ⟶ℝ)
46 eldifi 3694 . . . . . . . . . . . . 13 (𝑦 ∈ (ℝ ∖ (𝐴𝐵)) → 𝑦 ∈ ℝ)
47 ffvelrn 6265 . . . . . . . . . . . . 13 ((𝑓:ℝ⟶ℝ ∧ 𝑦 ∈ ℝ) → (𝑓𝑦) ∈ ℝ)
4845, 46, 47syl2an 493 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ∈ ℝ)
4948leidd 10473 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ (𝑓𝑦))
5049adantr 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (𝑓𝑦) ≤ (𝑓𝑦))
51 iftrue 4042 . . . . . . . . . . . . 13 (𝑦𝐴 → if(𝑦𝐴, (𝑓𝑦), 0) = (𝑓𝑦))
5251adantl 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → if(𝑦𝐴, (𝑓𝑦), 0) = (𝑓𝑦))
53 eldifn 3695 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (ℝ ∖ (𝐴𝐵)) → ¬ 𝑦 ∈ (𝐴𝐵))
5453adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ 𝑦 ∈ (𝐴𝐵))
55 elin 3758 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
5654, 55sylnib 317 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → ¬ (𝑦𝐴𝑦𝐵))
57 imnan 437 . . . . . . . . . . . . . . 15 ((𝑦𝐴 → ¬ 𝑦𝐵) ↔ ¬ (𝑦𝐴𝑦𝐵))
5856, 57sylibr 223 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑦𝐴 → ¬ 𝑦𝐵))
5958imp 444 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → ¬ 𝑦𝐵)
60 iffalse 4045 . . . . . . . . . . . . 13 𝑦𝐵 → if(𝑦𝐵, (𝑓𝑦), 0) = 0)
6159, 60syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → if(𝑦𝐵, (𝑓𝑦), 0) = 0)
6252, 61oveq12d 6567 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = ((𝑓𝑦) + 0))
6348recnd 9947 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ∈ ℂ)
6463adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (𝑓𝑦) ∈ ℂ)
6564addid1d 10115 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → ((𝑓𝑦) + 0) = (𝑓𝑦))
6662, 65eqtrd 2644 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = (𝑓𝑦))
6750, 66breqtrrd 4611 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ 𝑦𝐴) → (𝑓𝑦) ≤ (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
6849ad2antrr 758 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ 𝑦𝐵) → (𝑓𝑦) ≤ (𝑓𝑦))
69 iftrue 4042 . . . . . . . . . . . . 13 (𝑦𝐵 → if(𝑦𝐵, (𝑓𝑦), 0) = (𝑓𝑦))
7069adantl 481 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ 𝑦𝐵) → if(𝑦𝐵, (𝑓𝑦), 0) = (𝑓𝑦))
7168, 70breqtrrd 4611 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ 𝑦𝐵) → (𝑓𝑦) ≤ if(𝑦𝐵, (𝑓𝑦), 0))
72 itg2split.u . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 = (𝐴𝐵))
7372ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → 𝑈 = (𝐴𝐵))
7473eleq2d 2673 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑦𝑈𝑦 ∈ (𝐴𝐵)))
75 elun 3715 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
7674, 75syl6bb 275 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑦𝑈 ↔ (𝑦𝐴𝑦𝐵)))
7776notbid 307 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (¬ 𝑦𝑈 ↔ ¬ (𝑦𝐴𝑦𝐵)))
78 ioran 510 . . . . . . . . . . . . . . . 16 (¬ (𝑦𝐴𝑦𝐵) ↔ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵))
7977, 78syl6bb 275 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (¬ 𝑦𝑈 ↔ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵)))
8079biimpar 501 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵)) → ¬ 𝑦𝑈)
81 simprr 792 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓𝑟𝐻)
82 ffn 5958 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:ℝ⟶ℝ → 𝑓 Fn ℝ)
8345, 82syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝑓 Fn ℝ)
84 itg2split.c . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
8584adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝑈) → 𝐶 ∈ (0[,]+∞))
86 0e0iccpnf 12154 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ (0[,]+∞)
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝑈) → 0 ∈ (0[,]+∞))
8885, 87ifclda 4070 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
89 itg2split.h . . . . . . . . . . . . . . . . . . . . . . 23 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
9088, 89fmptd 6292 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐻:ℝ⟶(0[,]+∞))
91 ffn 5958 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻:ℝ⟶(0[,]+∞) → 𝐻 Fn ℝ)
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐻 Fn ℝ)
9392adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐻 Fn ℝ)
9430a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ℝ ∈ V)
95 inidm 3784 . . . . . . . . . . . . . . . . . . . 20 (ℝ ∩ ℝ) = ℝ
96 eqidd 2611 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓𝑦) = (𝑓𝑦))
97 eqidd 2611 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ ℝ) → (𝐻𝑦) = (𝐻𝑦))
9883, 93, 94, 94, 95, 96, 97ofrfval 6803 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑓𝑟𝐻 ↔ ∀𝑦 ∈ ℝ (𝑓𝑦) ≤ (𝐻𝑦)))
9981, 98mpbid 221 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑦 ∈ ℝ (𝑓𝑦) ≤ (𝐻𝑦))
10099r19.21bi 2916 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ ℝ) → (𝑓𝑦) ≤ (𝐻𝑦))
10146, 100sylan2 490 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ (𝐻𝑦))
102101adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝑈) → (𝑓𝑦) ≤ (𝐻𝑦))
10346adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → 𝑦 ∈ ℝ)
104 eldif 3550 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (ℝ ∖ 𝑈) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦𝑈))
105 nfcv 2751 . . . . . . . . . . . . . . . . . 18 𝑥𝑦
106 nfmpt1 4675 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0))
10789, 106nfcxfr 2749 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐻
108107, 105nffv 6110 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐻𝑦)
109108nfeq1 2764 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑦) = 0
110 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
111110eqeq1d 2612 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐻𝑥) = 0 ↔ (𝐻𝑦) = 0))
112 eldif 3550 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (ℝ ∖ 𝑈) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥𝑈))
11389fvmpt2i 6199 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → (𝐻𝑥) = ( I ‘if(𝑥𝑈, 𝐶, 0)))
114 iffalse 4045 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝑈 → if(𝑥𝑈, 𝐶, 0) = 0)
115114fveq2d 6107 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑈 → ( I ‘if(𝑥𝑈, 𝐶, 0)) = ( I ‘0))
116 0cn 9911 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
117 fvi 6165 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ ℂ → ( I ‘0) = 0)
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ( I ‘0) = 0
119115, 118syl6eq 2660 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑈 → ( I ‘if(𝑥𝑈, 𝐶, 0)) = 0)
120113, 119sylan9eq 2664 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ ∧ ¬ 𝑥𝑈) → (𝐻𝑥) = 0)
121112, 120sylbi 206 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (ℝ ∖ 𝑈) → (𝐻𝑥) = 0)
122105, 109, 111, 121vtoclgaf 3244 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (ℝ ∖ 𝑈) → (𝐻𝑦) = 0)
123104, 122sylbir 224 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ ∧ ¬ 𝑦𝑈) → (𝐻𝑦) = 0)
124103, 123sylan 487 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝑈) → (𝐻𝑦) = 0)
125102, 124breqtrd 4609 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝑈) → (𝑓𝑦) ≤ 0)
12680, 125syldan 486 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ (¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵)) → (𝑓𝑦) ≤ 0)
127126anassrs 678 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ ¬ 𝑦𝐵) → (𝑓𝑦) ≤ 0)
12860adantl 481 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ ¬ 𝑦𝐵) → if(𝑦𝐵, (𝑓𝑦), 0) = 0)
129127, 128breqtrrd 4611 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) ∧ ¬ 𝑦𝐵) → (𝑓𝑦) ≤ if(𝑦𝐵, (𝑓𝑦), 0))
13071, 129pm2.61dan 828 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (𝑓𝑦) ≤ if(𝑦𝐵, (𝑓𝑦), 0))
131 iffalse 4045 . . . . . . . . . . . . 13 𝑦𝐴 → if(𝑦𝐴, (𝑓𝑦), 0) = 0)
132131adantl 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → if(𝑦𝐴, (𝑓𝑦), 0) = 0)
133132oveq1d 6564 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = (0 + if(𝑦𝐵, (𝑓𝑦), 0)))
134 0re 9919 . . . . . . . . . . . . . . 15 0 ∈ ℝ
135 ifcl 4080 . . . . . . . . . . . . . . 15 (((𝑓𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℝ)
13648, 134, 135sylancl 693 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℝ)
137136recnd 9947 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℂ)
138137adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → if(𝑦𝐵, (𝑓𝑦), 0) ∈ ℂ)
139138addid2d 10116 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (0 + if(𝑦𝐵, (𝑓𝑦), 0)) = if(𝑦𝐵, (𝑓𝑦), 0))
140133, 139eqtrd 2644 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) = if(𝑦𝐵, (𝑓𝑦), 0))
141130, 140breqtrrd 4611 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) ∧ ¬ 𝑦𝐴) → (𝑓𝑦) ≤ (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
14267, 141pm2.61dan 828 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
143 eleq1 2676 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
144 fveq2 6103 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑓𝑥) = (𝑓𝑦))
145143, 144ifbieq1d 4059 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥𝐴, (𝑓𝑥), 0) = if(𝑦𝐴, (𝑓𝑦), 0))
146 eleq1 2676 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
147146, 144ifbieq1d 4059 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥𝐵, (𝑓𝑥), 0) = if(𝑦𝐵, (𝑓𝑦), 0))
148145, 147oveq12d 6567 . . . . . . . . . 10 (𝑥 = 𝑦 → (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)) = (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)))
149 eqid 2610 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))
150 ovex 6577 . . . . . . . . . 10 (if(𝑦𝐴, (𝑓𝑦), 0) + if(𝑦𝐵, (𝑓𝑦), 0)) ∈ V
151148, 149, 150fvmpt 6191 . . . . . . . . 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 4611 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑦 ∈ (ℝ ∖ (𝐴𝐵))) → (𝑓𝑦) ≤ ((𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))‘𝑦))
1541, 27, 29, 43, 153itg1lea 23285 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ≤ (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))))
15541fveq2d 6107 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))))
1568, 15itg1add 23274 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))))
157155, 156eqtr3d 2646 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ (if(𝑥𝐴, (𝑓𝑥), 0) + if(𝑥𝐵, (𝑓𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))))
158154, 157breqtrd 4609 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ≤ ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))))
15919adantr 480 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫2𝐹) ∈ ℝ)
16020adantr 480 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫2𝐺) ∈ ℝ)
161 ssun1 3738 . . . . . . . . . . . . . 14 𝐴 ⊆ (𝐴𝐵)
162161, 72syl5sseqr 3617 . . . . . . . . . . . . 13 (𝜑𝐴𝑈)
163162sselda 3568 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑥𝑈)
164163adantlr 747 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥𝑈)
165164, 85syldan 486 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐴) → 𝐶 ∈ (0[,]+∞))
16686a1i 11 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
167165, 166ifclda 4070 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, 𝐶, 0) ∈ (0[,]+∞))
168 itg2split.f . . . . . . . . 9 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0))
169167, 168fmptd 6292 . . . . . . . 8 (𝜑𝐹:ℝ⟶(0[,]+∞))
170169adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐹:ℝ⟶(0[,]+∞))
171 nfv 1830 . . . . . . . . . 10 𝑥𝜑
172 nfv 1830 . . . . . . . . . . 11 𝑥 𝑓 ∈ dom ∫1
173 nfcv 2751 . . . . . . . . . . . 12 𝑥𝑓
174 nfcv 2751 . . . . . . . . . . . 12 𝑥𝑟
175173, 174, 107nfbr 4629 . . . . . . . . . . 11 𝑥 𝑓𝑟𝐻
176172, 175nfan 1816 . . . . . . . . . 10 𝑥(𝑓 ∈ dom ∫1𝑓𝑟𝐻)
177171, 176nfan 1816 . . . . . . . . 9 𝑥(𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻))
1785, 24syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐴 ⊆ ℝ)
179178sselda 3568 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → 𝑥 ∈ ℝ)
18030a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → ℝ ∈ V)
18132a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ V)
18288adantlr 747 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑈, 𝐶, 0) ∈ (0[,]+∞))
18344adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ)
184183feqmptd 6159 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
18589a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥𝑈, 𝐶, 0)))
186180, 181, 182, 184, 185ofrfval2 6813 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐻 ↔ ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0)))
187186biimpd 218 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐻 → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0)))
188187impr 647 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑥 ∈ ℝ (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
189188r19.21bi 2916 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
190179, 189syldan 486 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
191163adantlr 747 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → 𝑥𝑈)
192191iftrued 4044 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
193190, 192breqtrd 4609 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → (𝑓𝑥) ≤ 𝐶)
194 iftrue 4042 . . . . . . . . . . . . 13 (𝑥𝐴 → if(𝑥𝐴, (𝑓𝑥), 0) = (𝑓𝑥))
195194adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝐴, (𝑓𝑥), 0) = (𝑓𝑥))
196 iftrue 4042 . . . . . . . . . . . . 13 (𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 𝐶)
197196adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝐴, 𝐶, 0) = 𝐶)
198193, 195, 1973brtr4d 4615 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐴) → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
199 0le0 10987 . . . . . . . . . . . . . 14 0 ≤ 0
200199a1i 11 . . . . . . . . . . . . 13 𝑥𝐴 → 0 ≤ 0)
201 iffalse 4045 . . . . . . . . . . . . 13 𝑥𝐴 → if(𝑥𝐴, (𝑓𝑥), 0) = 0)
202 iffalse 4045 . . . . . . . . . . . . 13 𝑥𝐴 → if(𝑥𝐴, 𝐶, 0) = 0)
203200, 201, 2023brtr4d 4615 . . . . . . . . . . . 12 𝑥𝐴 → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
204203adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ ¬ 𝑥𝐴) → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
205198, 204pm2.61dan 828 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
206205a1d 25 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ → if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0)))
207177, 206ralrimi 2940 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑥 ∈ ℝ if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0))
208168a1i 11 . . . . . . . . . 10 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 𝐶, 0)))
20931, 35, 167, 38, 208ofrfval2 6813 . . . . . . . . 9 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0)))
210209adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐴, (𝑓𝑥), 0) ≤ if(𝑥𝐴, 𝐶, 0)))
211207, 210mpbird 246 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹)
212 itg2ub 23306 . . . . . . 7 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0)) ∘𝑟𝐹) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ≤ (∫2𝐹))
213170, 8, 211, 212syl3anc 1318 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) ≤ (∫2𝐹))
214 ssun2 3739 . . . . . . . . . . . . . 14 𝐵 ⊆ (𝐴𝐵)
215214, 72syl5sseqr 3617 . . . . . . . . . . . . 13 (𝜑𝐵𝑈)
216215sselda 3568 . . . . . . . . . . . 12 ((𝜑𝑥𝐵) → 𝑥𝑈)
217216adantlr 747 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥𝑈)
218217, 85syldan 486 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
21986a1i 11 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥𝐵) → 0 ∈ (0[,]+∞))
220218, 219ifclda 4070 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐵, 𝐶, 0) ∈ (0[,]+∞))
221 itg2split.g . . . . . . . . 9 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0))
222220, 221fmptd 6292 . . . . . . . 8 (𝜑𝐺:ℝ⟶(0[,]+∞))
223222adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐺:ℝ⟶(0[,]+∞))
224 mblss 23106 . . . . . . . . . . . . . . . 16 (𝐵 ∈ dom vol → 𝐵 ⊆ ℝ)
22512, 224syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → 𝐵 ⊆ ℝ)
226225sselda 3568 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → 𝑥 ∈ ℝ)
227226, 189syldan 486 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → (𝑓𝑥) ≤ if(𝑥𝑈, 𝐶, 0))
228216adantlr 747 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → 𝑥𝑈)
229228iftrued 4044 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝑈, 𝐶, 0) = 𝐶)
230227, 229breqtrd 4609 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → (𝑓𝑥) ≤ 𝐶)
231 iftrue 4042 . . . . . . . . . . . . 13 (𝑥𝐵 → if(𝑥𝐵, (𝑓𝑥), 0) = (𝑓𝑥))
232231adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝐵, (𝑓𝑥), 0) = (𝑓𝑥))
233 iftrue 4042 . . . . . . . . . . . . 13 (𝑥𝐵 → if(𝑥𝐵, 𝐶, 0) = 𝐶)
234233adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝐵, 𝐶, 0) = 𝐶)
235230, 232, 2343brtr4d 4615 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ 𝑥𝐵) → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
236199a1i 11 . . . . . . . . . . . . 13 𝑥𝐵 → 0 ≤ 0)
237 iffalse 4045 . . . . . . . . . . . . 13 𝑥𝐵 → if(𝑥𝐵, (𝑓𝑥), 0) = 0)
238 iffalse 4045 . . . . . . . . . . . . 13 𝑥𝐵 → if(𝑥𝐵, 𝐶, 0) = 0)
239236, 237, 2383brtr4d 4615 . . . . . . . . . . . 12 𝑥𝐵 → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
240239adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) ∧ ¬ 𝑥𝐵) → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
241235, 240pm2.61dan 828 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
242241a1d 25 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ → if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0)))
243177, 242ralrimi 2940 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ∀𝑥 ∈ ℝ if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0))
244221a1i 11 . . . . . . . . . 10 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐵, 𝐶, 0)))
24531, 37, 220, 39, 244ofrfval2 6813 . . . . . . . . 9 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0)))
246245adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺 ↔ ∀𝑥 ∈ ℝ if(𝑥𝐵, (𝑓𝑥), 0) ≤ if(𝑥𝐵, 𝐶, 0)))
247243, 246mpbird 246 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺)
248 itg2ub 23306 . . . . . . 7 ((𝐺:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)) ∘𝑟𝐺) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ≤ (∫2𝐺))
249223, 15, 247, 248syl3anc 1318 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0))) ≤ (∫2𝐺))
25010, 17, 159, 160, 213, 249le2addd 10525 . . . . 5 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → ((∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (𝑓𝑥), 0))) + (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥𝐵, (𝑓𝑥), 0)))) ≤ ((∫2𝐹) + (∫2𝐺)))
2513, 18, 22, 158, 250letrd 10073 . . . 4 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑓𝑟𝐻)) → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺)))
252251expr 641 . . 3 ((𝜑𝑓 ∈ dom ∫1) → (𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺))))
253252ralrimiva 2949 . 2 (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺))))
25421rexrd 9968 . . 3 (𝜑 → ((∫2𝐹) + (∫2𝐺)) ∈ ℝ*)
255 itg2leub 23307 . . 3 ((𝐻:ℝ⟶(0[,]+∞) ∧ ((∫2𝐹) + (∫2𝐺)) ∈ ℝ*) → ((∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺)))))
25690, 254, 255syl2anc 691 . 2 (𝜑 → ((∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓𝑟𝐻 → (∫1𝑓) ≤ ((∫2𝐹) + (∫2𝐺)))))
257253, 256mpbird 246 1 (𝜑 → (∫2𝐻) ≤ ((∫2𝐹) + (∫2𝐺)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643   I cid 4948  dom cdm 5038   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘𝑓 cof 6793   ∘𝑟 cofr 6794  ℂcc 9813  ℝcr 9814  0cc0 9815   + caddc 9818  +∞cpnf 9950  ℝ*cxr 9952   ≤ cle 9954  [,]cicc 12049  vol*covol 23038  volcvol 23039  ∫1citg1 23190  ∫2citg2 23191 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-ofr 6796  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-mbf 23194  df-itg1 23195  df-itg2 23196 This theorem is referenced by:  itg2split  23322
 Copyright terms: Public domain W3C validator