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 ‘ 𝐺 ) ) )