Metamath Proof Explorer


Theorem itg2splitlem

Description: Lemma for itg2split . (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses 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 itg2splitlem ( 𝜑 → ( ∫2𝐻 ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 itg2split.a ( 𝜑𝐴 ∈ dom vol )
2 itg2split.b ( 𝜑𝐵 ∈ dom vol )
3 itg2split.i ( 𝜑 → ( vol* ‘ ( 𝐴𝐵 ) ) = 0 )
4 itg2split.u ( 𝜑𝑈 = ( 𝐴𝐵 ) )
5 itg2split.c ( ( 𝜑𝑥𝑈 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
6 itg2split.f 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , 𝐶 , 0 ) )
7 itg2split.g 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , 𝐶 , 0 ) )
8 itg2split.h 𝐻 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝑈 , 𝐶 , 0 ) )
9 itg2split.sf ( 𝜑 → ( ∫2𝐹 ) ∈ ℝ )
10 itg2split.sg ( 𝜑 → ( ∫2𝐺 ) ∈ ℝ )
11 simprl ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝑓 ∈ dom ∫1 )
12 itg1cl ( 𝑓 ∈ dom ∫1 → ( ∫1𝑓 ) ∈ ℝ )
13 11 12 syl ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1𝑓 ) ∈ ℝ )
14 1 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝐴 ∈ dom vol )
15 eqid ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) )
16 15 i1fres ( ( 𝑓 ∈ dom ∫1𝐴 ∈ dom vol ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∈ dom ∫1 )
17 11 14 16 syl2anc ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∈ dom ∫1 )
18 itg1cl ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ) ∈ ℝ )
19 17 18 syl ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ) ∈ ℝ )
20 2 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝐵 ∈ dom vol )
21 eqid ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) )
22 21 i1fres ( ( 𝑓 ∈ dom ∫1𝐵 ∈ dom vol ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ∈ dom ∫1 )
23 11 20 22 syl2anc ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ∈ dom ∫1 )
24 itg1cl ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ∈ ℝ )
25 23 24 syl ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ∈ ℝ )
26 19 25 readdcld ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ) + ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) ∈ ℝ )
27 9 10 readdcld ( 𝜑 → ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ∈ ℝ )
28 27 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ∈ ℝ )
29 inss1 ( 𝐴𝐵 ) ⊆ 𝐴
30 mblss ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
31 1 30 syl ( 𝜑𝐴 ⊆ ℝ )
32 29 31 sstrid ( 𝜑 → ( 𝐴𝐵 ) ⊆ ℝ )
33 32 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( 𝐴𝐵 ) ⊆ ℝ )
34 3 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) = 0 )
35 reex ℝ ∈ V
36 35 a1i ( 𝜑 → ℝ ∈ V )
37 fvex ( 𝑓𝑥 ) ∈ V
38 c0ex 0 ∈ V
39 37 38 ifex if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ∈ V
40 39 a1i ( ( 𝜑𝑥 ∈ ℝ ) → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ∈ V )
41 37 38 ifex if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ∈ V
42 41 a1i ( ( 𝜑𝑥 ∈ ℝ ) → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ∈ V )
43 eqidd ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) )
44 eqidd ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) )
45 36 40 42 43 44 offval2 ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) )
46 45 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) )
47 17 23 i1fadd ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ∈ dom ∫1 )
48 46 47 eqeltrrd ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ∈ dom ∫1 )
49 i1ff ( 𝑓 ∈ dom ∫1𝑓 : ℝ ⟶ ℝ )
50 11 49 syl ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝑓 : ℝ ⟶ ℝ )
51 eldifi ( 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) → 𝑦 ∈ ℝ )
52 ffvelrn ( ( 𝑓 : ℝ ⟶ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑓𝑦 ) ∈ ℝ )
53 50 51 52 syl2an ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( 𝑓𝑦 ) ∈ ℝ )
54 53 leidd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( 𝑓𝑦 ) ≤ ( 𝑓𝑦 ) )
55 54 adantr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ 𝑦𝐴 ) → ( 𝑓𝑦 ) ≤ ( 𝑓𝑦 ) )
56 iftrue ( 𝑦𝐴 → if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) = ( 𝑓𝑦 ) )
57 56 adantl ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ 𝑦𝐴 ) → if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) = ( 𝑓𝑦 ) )
58 eldifn ( 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) → ¬ 𝑦 ∈ ( 𝐴𝐵 ) )
59 58 adantl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ¬ 𝑦 ∈ ( 𝐴𝐵 ) )
60 elin ( 𝑦 ∈ ( 𝐴𝐵 ) ↔ ( 𝑦𝐴𝑦𝐵 ) )
61 59 60 sylnib ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ¬ ( 𝑦𝐴𝑦𝐵 ) )
62 imnan ( ( 𝑦𝐴 → ¬ 𝑦𝐵 ) ↔ ¬ ( 𝑦𝐴𝑦𝐵 ) )
63 61 62 sylibr ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( 𝑦𝐴 → ¬ 𝑦𝐵 ) )
64 63 imp ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ 𝑦𝐴 ) → ¬ 𝑦𝐵 )
65 iffalse ( ¬ 𝑦𝐵 → if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) = 0 )
66 64 65 syl ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ 𝑦𝐴 ) → if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) = 0 )
67 57 66 oveq12d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ 𝑦𝐴 ) → ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) = ( ( 𝑓𝑦 ) + 0 ) )
68 53 recnd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( 𝑓𝑦 ) ∈ ℂ )
69 68 adantr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ 𝑦𝐴 ) → ( 𝑓𝑦 ) ∈ ℂ )
70 69 addid1d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ 𝑦𝐴 ) → ( ( 𝑓𝑦 ) + 0 ) = ( 𝑓𝑦 ) )
71 67 70 eqtrd ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ 𝑦𝐴 ) → ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) = ( 𝑓𝑦 ) )
72 55 71 breqtrrd ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ 𝑦𝐴 ) → ( 𝑓𝑦 ) ≤ ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) )
73 54 ad2antrr ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) ∧ 𝑦𝐵 ) → ( 𝑓𝑦 ) ≤ ( 𝑓𝑦 ) )
74 iftrue ( 𝑦𝐵 → if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) = ( 𝑓𝑦 ) )
75 74 adantl ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) ∧ 𝑦𝐵 ) → if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) = ( 𝑓𝑦 ) )
76 73 75 breqtrrd ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) ∧ 𝑦𝐵 ) → ( 𝑓𝑦 ) ≤ if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) )
77 4 ad2antrr ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → 𝑈 = ( 𝐴𝐵 ) )
78 77 eleq2d ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( 𝑦𝑈𝑦 ∈ ( 𝐴𝐵 ) ) )
79 elun ( 𝑦 ∈ ( 𝐴𝐵 ) ↔ ( 𝑦𝐴𝑦𝐵 ) )
80 78 79 bitrdi ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( 𝑦𝑈 ↔ ( 𝑦𝐴𝑦𝐵 ) ) )
81 80 notbid ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( ¬ 𝑦𝑈 ↔ ¬ ( 𝑦𝐴𝑦𝐵 ) ) )
82 ioran ( ¬ ( 𝑦𝐴𝑦𝐵 ) ↔ ( ¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵 ) )
83 81 82 bitrdi ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( ¬ 𝑦𝑈 ↔ ( ¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵 ) ) )
84 83 biimpar ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ( ¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵 ) ) → ¬ 𝑦𝑈 )
85 simprr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝑓r𝐻 )
86 50 ffnd ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝑓 Fn ℝ )
87 5 adantlr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑥𝑈 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
88 0e0iccpnf 0 ∈ ( 0 [,] +∞ )
89 88 a1i ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ¬ 𝑥𝑈 ) → 0 ∈ ( 0 [,] +∞ ) )
90 87 89 ifclda ( ( 𝜑𝑥 ∈ ℝ ) → if ( 𝑥𝑈 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
91 90 8 fmptd ( 𝜑𝐻 : ℝ ⟶ ( 0 [,] +∞ ) )
92 91 ffnd ( 𝜑𝐻 Fn ℝ )
93 92 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝐻 Fn ℝ )
94 35 a1i ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ℝ ∈ V )
95 inidm ( ℝ ∩ ℝ ) = ℝ
96 eqidd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ℝ ) → ( 𝑓𝑦 ) = ( 𝑓𝑦 ) )
97 eqidd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ℝ ) → ( 𝐻𝑦 ) = ( 𝐻𝑦 ) )
98 86 93 94 94 95 96 97 ofrfval ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( 𝑓r𝐻 ↔ ∀ 𝑦 ∈ ℝ ( 𝑓𝑦 ) ≤ ( 𝐻𝑦 ) ) )
99 85 98 mpbid ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ∀ 𝑦 ∈ ℝ ( 𝑓𝑦 ) ≤ ( 𝐻𝑦 ) )
100 99 r19.21bi ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ℝ ) → ( 𝑓𝑦 ) ≤ ( 𝐻𝑦 ) )
101 51 100 sylan2 ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( 𝑓𝑦 ) ≤ ( 𝐻𝑦 ) )
102 101 adantr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝑈 ) → ( 𝑓𝑦 ) ≤ ( 𝐻𝑦 ) )
103 51 adantl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → 𝑦 ∈ ℝ )
104 eldif ( 𝑦 ∈ ( ℝ ∖ 𝑈 ) ↔ ( 𝑦 ∈ ℝ ∧ ¬ 𝑦𝑈 ) )
105 nfcv 𝑥 𝑦
106 nfmpt1 𝑥 ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝑈 , 𝐶 , 0 ) )
107 8 106 nfcxfr 𝑥 𝐻
108 107 105 nffv 𝑥 ( 𝐻𝑦 )
109 108 nfeq1 𝑥 ( 𝐻𝑦 ) = 0
110 fveqeq2 ( 𝑥 = 𝑦 → ( ( 𝐻𝑥 ) = 0 ↔ ( 𝐻𝑦 ) = 0 ) )
111 eldif ( 𝑥 ∈ ( ℝ ∖ 𝑈 ) ↔ ( 𝑥 ∈ ℝ ∧ ¬ 𝑥𝑈 ) )
112 8 fvmpt2i ( 𝑥 ∈ ℝ → ( 𝐻𝑥 ) = ( I ‘ if ( 𝑥𝑈 , 𝐶 , 0 ) ) )
113 iffalse ( ¬ 𝑥𝑈 → if ( 𝑥𝑈 , 𝐶 , 0 ) = 0 )
114 113 fveq2d ( ¬ 𝑥𝑈 → ( I ‘ if ( 𝑥𝑈 , 𝐶 , 0 ) ) = ( I ‘ 0 ) )
115 0cn 0 ∈ ℂ
116 fvi ( 0 ∈ ℂ → ( I ‘ 0 ) = 0 )
117 115 116 ax-mp ( I ‘ 0 ) = 0
118 114 117 eqtrdi ( ¬ 𝑥𝑈 → ( I ‘ if ( 𝑥𝑈 , 𝐶 , 0 ) ) = 0 )
119 112 118 sylan9eq ( ( 𝑥 ∈ ℝ ∧ ¬ 𝑥𝑈 ) → ( 𝐻𝑥 ) = 0 )
120 111 119 sylbi ( 𝑥 ∈ ( ℝ ∖ 𝑈 ) → ( 𝐻𝑥 ) = 0 )
121 105 109 110 120 vtoclgaf ( 𝑦 ∈ ( ℝ ∖ 𝑈 ) → ( 𝐻𝑦 ) = 0 )
122 104 121 sylbir ( ( 𝑦 ∈ ℝ ∧ ¬ 𝑦𝑈 ) → ( 𝐻𝑦 ) = 0 )
123 103 122 sylan ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝑈 ) → ( 𝐻𝑦 ) = 0 )
124 102 123 breqtrd ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝑈 ) → ( 𝑓𝑦 ) ≤ 0 )
125 84 124 syldan ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ( ¬ 𝑦𝐴 ∧ ¬ 𝑦𝐵 ) ) → ( 𝑓𝑦 ) ≤ 0 )
126 125 anassrs ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) ∧ ¬ 𝑦𝐵 ) → ( 𝑓𝑦 ) ≤ 0 )
127 65 adantl ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) ∧ ¬ 𝑦𝐵 ) → if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) = 0 )
128 126 127 breqtrrd ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) ∧ ¬ 𝑦𝐵 ) → ( 𝑓𝑦 ) ≤ if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) )
129 76 128 pm2.61dan ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) → ( 𝑓𝑦 ) ≤ if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) )
130 iffalse ( ¬ 𝑦𝐴 → if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) = 0 )
131 130 adantl ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) → if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) = 0 )
132 131 oveq1d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) → ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) = ( 0 + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) )
133 0re 0 ∈ ℝ
134 ifcl ( ( ( 𝑓𝑦 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ∈ ℝ )
135 53 133 134 sylancl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ∈ ℝ )
136 135 recnd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ∈ ℂ )
137 136 adantr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) → if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ∈ ℂ )
138 137 addid2d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) → ( 0 + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) = if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) )
139 132 138 eqtrd ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) → ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) = if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) )
140 129 139 breqtrrd ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) ∧ ¬ 𝑦𝐴 ) → ( 𝑓𝑦 ) ≤ ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) )
141 72 140 pm2.61dan ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( 𝑓𝑦 ) ≤ ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) )
142 eleq1w ( 𝑥 = 𝑦 → ( 𝑥𝐴𝑦𝐴 ) )
143 fveq2 ( 𝑥 = 𝑦 → ( 𝑓𝑥 ) = ( 𝑓𝑦 ) )
144 142 143 ifbieq1d ( 𝑥 = 𝑦 → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) = if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) )
145 eleq1w ( 𝑥 = 𝑦 → ( 𝑥𝐵𝑦𝐵 ) )
146 145 143 ifbieq1d ( 𝑥 = 𝑦 → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) = if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) )
147 144 146 oveq12d ( 𝑥 = 𝑦 → ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) = ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) )
148 eqid ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) )
149 ovex ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) ∈ V
150 147 148 149 fvmpt ( 𝑦 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ‘ 𝑦 ) = ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) )
151 103 150 syl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ‘ 𝑦 ) = ( if ( 𝑦𝐴 , ( 𝑓𝑦 ) , 0 ) + if ( 𝑦𝐵 , ( 𝑓𝑦 ) , 0 ) ) )
152 141 151 breqtrrd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴𝐵 ) ) ) → ( 𝑓𝑦 ) ≤ ( ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ‘ 𝑦 ) )
153 11 33 34 48 152 itg1lea ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1𝑓 ) ≤ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) )
154 46 fveq2d ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) )
155 17 23 itg1add ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) = ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ) + ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) )
156 154 155 eqtr3d ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) + if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) = ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ) + ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) )
157 153 156 breqtrd ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1𝑓 ) ≤ ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ) + ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) )
158 9 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫2𝐹 ) ∈ ℝ )
159 10 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫2𝐺 ) ∈ ℝ )
160 ssun1 𝐴 ⊆ ( 𝐴𝐵 )
161 160 4 sseqtrrid ( 𝜑𝐴𝑈 )
162 161 sselda ( ( 𝜑𝑥𝐴 ) → 𝑥𝑈 )
163 162 adantlr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝑥𝑈 )
164 163 87 syldan ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
165 88 a1i ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ¬ 𝑥𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
166 164 165 ifclda ( ( 𝜑𝑥 ∈ ℝ ) → if ( 𝑥𝐴 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
167 166 6 fmptd ( 𝜑𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
168 167 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
169 nfv 𝑥 𝜑
170 nfv 𝑥 𝑓 ∈ dom ∫1
171 nfcv 𝑥 𝑓
172 nfcv 𝑥r
173 171 172 107 nfbr 𝑥 𝑓r𝐻
174 170 173 nfan 𝑥 ( 𝑓 ∈ dom ∫1𝑓r𝐻 )
175 169 174 nfan 𝑥 ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) )
176 14 30 syl ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝐴 ⊆ ℝ )
177 176 sselda ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐴 ) → 𝑥 ∈ ℝ )
178 35 a1i ( ( 𝜑𝑓 ∈ dom ∫1 ) → ℝ ∈ V )
179 37 a1i ( ( ( 𝜑𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓𝑥 ) ∈ V )
180 90 adantlr ( ( ( 𝜑𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥𝑈 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
181 49 adantl ( ( 𝜑𝑓 ∈ dom ∫1 ) → 𝑓 : ℝ ⟶ ℝ )
182 181 feqmptd ( ( 𝜑𝑓 ∈ dom ∫1 ) → 𝑓 = ( 𝑥 ∈ ℝ ↦ ( 𝑓𝑥 ) ) )
183 8 a1i ( ( 𝜑𝑓 ∈ dom ∫1 ) → 𝐻 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝑈 , 𝐶 , 0 ) ) )
184 178 179 180 182 183 ofrfval2 ( ( 𝜑𝑓 ∈ dom ∫1 ) → ( 𝑓r𝐻 ↔ ∀ 𝑥 ∈ ℝ ( 𝑓𝑥 ) ≤ if ( 𝑥𝑈 , 𝐶 , 0 ) ) )
185 184 biimpd ( ( 𝜑𝑓 ∈ dom ∫1 ) → ( 𝑓r𝐻 → ∀ 𝑥 ∈ ℝ ( 𝑓𝑥 ) ≤ if ( 𝑥𝑈 , 𝐶 , 0 ) ) )
186 185 impr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ∀ 𝑥 ∈ ℝ ( 𝑓𝑥 ) ≤ if ( 𝑥𝑈 , 𝐶 , 0 ) )
187 186 r19.21bi ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓𝑥 ) ≤ if ( 𝑥𝑈 , 𝐶 , 0 ) )
188 177 187 syldan ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐴 ) → ( 𝑓𝑥 ) ≤ if ( 𝑥𝑈 , 𝐶 , 0 ) )
189 162 adantlr ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐴 ) → 𝑥𝑈 )
190 189 iftrued ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐴 ) → if ( 𝑥𝑈 , 𝐶 , 0 ) = 𝐶 )
191 188 190 breqtrd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐴 ) → ( 𝑓𝑥 ) ≤ 𝐶 )
192 iftrue ( 𝑥𝐴 → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) = ( 𝑓𝑥 ) )
193 192 adantl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐴 ) → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) = ( 𝑓𝑥 ) )
194 iftrue ( 𝑥𝐴 → if ( 𝑥𝐴 , 𝐶 , 0 ) = 𝐶 )
195 194 adantl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐴 ) → if ( 𝑥𝐴 , 𝐶 , 0 ) = 𝐶 )
196 191 193 195 3brtr4d ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐴 ) → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐴 , 𝐶 , 0 ) )
197 0le0 0 ≤ 0
198 197 a1i ( ¬ 𝑥𝐴 → 0 ≤ 0 )
199 iffalse ( ¬ 𝑥𝐴 → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) = 0 )
200 iffalse ( ¬ 𝑥𝐴 → if ( 𝑥𝐴 , 𝐶 , 0 ) = 0 )
201 198 199 200 3brtr4d ( ¬ 𝑥𝐴 → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐴 , 𝐶 , 0 ) )
202 201 adantl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ ¬ 𝑥𝐴 ) → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐴 , 𝐶 , 0 ) )
203 196 202 pm2.61dan ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐴 , 𝐶 , 0 ) )
204 203 a1d ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( 𝑥 ∈ ℝ → if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐴 , 𝐶 , 0 ) ) )
205 175 204 ralrimi ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐴 , 𝐶 , 0 ) )
206 6 a1i ( 𝜑𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , 𝐶 , 0 ) ) )
207 36 40 166 43 206 ofrfval2 ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∘r𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐴 , 𝐶 , 0 ) ) )
208 207 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∘r𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐴 , 𝐶 , 0 ) ) )
209 205 208 mpbird ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∘r𝐹 )
210 itg2ub ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ∘r𝐹 ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ) ≤ ( ∫2𝐹 ) )
211 168 17 209 210 syl3anc ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ) ≤ ( ∫2𝐹 ) )
212 ssun2 𝐵 ⊆ ( 𝐴𝐵 )
213 212 4 sseqtrrid ( 𝜑𝐵𝑈 )
214 213 sselda ( ( 𝜑𝑥𝐵 ) → 𝑥𝑈 )
215 214 adantlr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑥𝐵 ) → 𝑥𝑈 )
216 215 87 syldan ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑥𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
217 88 a1i ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ¬ 𝑥𝐵 ) → 0 ∈ ( 0 [,] +∞ ) )
218 216 217 ifclda ( ( 𝜑𝑥 ∈ ℝ ) → if ( 𝑥𝐵 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
219 218 7 fmptd ( 𝜑𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
220 219 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
221 mblss ( 𝐵 ∈ dom vol → 𝐵 ⊆ ℝ )
222 20 221 syl ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → 𝐵 ⊆ ℝ )
223 222 sselda ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐵 ) → 𝑥 ∈ ℝ )
224 223 187 syldan ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐵 ) → ( 𝑓𝑥 ) ≤ if ( 𝑥𝑈 , 𝐶 , 0 ) )
225 214 adantlr ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐵 ) → 𝑥𝑈 )
226 225 iftrued ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐵 ) → if ( 𝑥𝑈 , 𝐶 , 0 ) = 𝐶 )
227 224 226 breqtrd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐵 ) → ( 𝑓𝑥 ) ≤ 𝐶 )
228 iftrue ( 𝑥𝐵 → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) = ( 𝑓𝑥 ) )
229 228 adantl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐵 ) → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) = ( 𝑓𝑥 ) )
230 iftrue ( 𝑥𝐵 → if ( 𝑥𝐵 , 𝐶 , 0 ) = 𝐶 )
231 230 adantl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐵 ) → if ( 𝑥𝐵 , 𝐶 , 0 ) = 𝐶 )
232 227 229 231 3brtr4d ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ 𝑥𝐵 ) → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐵 , 𝐶 , 0 ) )
233 197 a1i ( ¬ 𝑥𝐵 → 0 ≤ 0 )
234 iffalse ( ¬ 𝑥𝐵 → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) = 0 )
235 iffalse ( ¬ 𝑥𝐵 → if ( 𝑥𝐵 , 𝐶 , 0 ) = 0 )
236 233 234 235 3brtr4d ( ¬ 𝑥𝐵 → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐵 , 𝐶 , 0 ) )
237 236 adantl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) ∧ ¬ 𝑥𝐵 ) → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐵 , 𝐶 , 0 ) )
238 232 237 pm2.61dan ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐵 , 𝐶 , 0 ) )
239 238 a1d ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( 𝑥 ∈ ℝ → if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐵 , 𝐶 , 0 ) ) )
240 175 239 ralrimi ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐵 , 𝐶 , 0 ) )
241 7 a1i ( 𝜑𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , 𝐶 , 0 ) ) )
242 36 42 218 44 241 ofrfval2 ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ∘r𝐺 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐵 , 𝐶 , 0 ) ) )
243 242 adantr ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ∘r𝐺 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ≤ if ( 𝑥𝐵 , 𝐶 , 0 ) ) )
244 240 243 mpbird ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ∘r𝐺 )
245 itg2ub ( ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ∘r𝐺 ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ≤ ( ∫2𝐺 ) )
246 220 23 244 245 syl3anc ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ≤ ( ∫2𝐺 ) )
247 19 25 158 159 211 246 le2addd ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( 𝑓𝑥 ) , 0 ) ) ) + ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐵 , ( 𝑓𝑥 ) , 0 ) ) ) ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )
248 13 26 28 157 247 letrd ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑓r𝐻 ) ) → ( ∫1𝑓 ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )
249 248 expr ( ( 𝜑𝑓 ∈ dom ∫1 ) → ( 𝑓r𝐻 → ( ∫1𝑓 ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ) )
250 249 ralrimiva ( 𝜑 → ∀ 𝑓 ∈ dom ∫1 ( 𝑓r𝐻 → ( ∫1𝑓 ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ) )
251 27 rexrd ( 𝜑 → ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ∈ ℝ* )
252 itg2leub ( ( 𝐻 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ∈ ℝ* ) → ( ( ∫2𝐻 ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓r𝐻 → ( ∫1𝑓 ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ) ) )
253 91 251 252 syl2anc ( 𝜑 → ( ( ∫2𝐻 ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓r𝐻 → ( ∫1𝑓 ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ) ) )
254 250 253 mpbird ( 𝜑 → ( ∫2𝐻 ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )