Metamath Proof Explorer

Theorem itg2split

Description: The S.2 integral splits under an almost disjoint union. The proof avoids the use of itg2add , which requires countable choice. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itg2split.a 
|- ( ph -> A e. dom vol )
itg2split.b 
|- ( ph -> B e. dom vol )
itg2split.i 
|- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
itg2split.u 
|- ( ph -> U = ( A u. B ) )
itg2split.c 
|- ( ( ph /\ x e. U ) -> C e. ( 0 [,] +oo ) )
itg2split.f 
|- F = ( x e. RR |-> if ( x e. A , C , 0 ) )
itg2split.g 
|- G = ( x e. RR |-> if ( x e. B , C , 0 ) )
itg2split.h 
|- H = ( x e. RR |-> if ( x e. U , C , 0 ) )
itg2split.sf 
|- ( ph -> ( S.2 ` F ) e. RR )
itg2split.sg 
|- ( ph -> ( S.2 ` G ) e. RR )
Assertion itg2split 
|- ( ph -> ( S.2 ` H ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )

Proof

Step Hyp Ref Expression
1 itg2split.a 
 |-  ( ph -> A e. dom vol )
2 itg2split.b 
 |-  ( ph -> B e. dom vol )
3 itg2split.i 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
4 itg2split.u 
 |-  ( ph -> U = ( A u. B ) )
5 itg2split.c 
 |-  ( ( ph /\ x e. U ) -> C e. ( 0 [,] +oo ) )
6 itg2split.f 
 |-  F = ( x e. RR |-> if ( x e. A , C , 0 ) )
7 itg2split.g 
 |-  G = ( x e. RR |-> if ( x e. B , C , 0 ) )
8 itg2split.h 
 |-  H = ( x e. RR |-> if ( x e. U , C , 0 ) )
9 itg2split.sf 
 |-  ( ph -> ( S.2 ` F ) e. RR )
10 itg2split.sg 
 |-  ( ph -> ( S.2 ` G ) e. RR )
11 5 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. U ) -> C e. ( 0 [,] +oo ) )
12 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
13 12 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. U ) -> 0 e. ( 0 [,] +oo ) )
14 11 13 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) )
15 14 8 fmptd 
 |-  ( ph -> H : RR --> ( 0 [,] +oo ) )
16 itg2cl 
 |-  ( H : RR --> ( 0 [,] +oo ) -> ( S.2 ` H ) e. RR* )
17 15 16 syl 
 |-  ( ph -> ( S.2 ` H ) e. RR* )
18 9 10 readdcld 
 |-  ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR )
19 18 rexrd 
 |-  ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR* )
20 1 2 3 4 5 6 7 8 9 10 itg2splitlem 
 |-  ( ph -> ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) )
21 10 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( S.2 ` G ) e. RR )
22 itg2lecl 
 |-  ( ( H : RR --> ( 0 [,] +oo ) /\ ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR /\ ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) ) -> ( S.2 ` H ) e. RR )
23 15 18 20 22 syl3anc 
 |-  ( ph -> ( S.2 ` H ) e. RR )
24 23 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( S.2 ` H ) e. RR )
25 itg1cl 
 |-  ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
26 25 ad2antrl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( S.1 ` f ) e. RR )
27 simprll 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> f e. dom S.1 )
28 simprrl 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> g e. dom S.1 )
29 27 28 itg1add 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( S.1 ` ( f oF + g ) ) = ( ( S.1 ` f ) + ( S.1 ` g ) ) )
30 15 adantr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> H : RR --> ( 0 [,] +oo ) )
31 27 28 i1fadd 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( f oF + g ) e. dom S.1 )
32 inss1 
 |-  ( A i^i B ) C_ A
33 mblss 
 |-  ( A e. dom vol -> A C_ RR )
34 1 33 syl 
 |-  ( ph -> A C_ RR )
35 32 34 sstrid 
 |-  ( ph -> ( A i^i B ) C_ RR )
36 35 adantr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( A i^i B ) C_ RR )
37 3 adantr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( vol* ` ( A i^i B ) ) = 0 )
38 nfv 
 |-  F/ x ph
39 nfv 
 |-  F/ x f e. dom S.1
40 nfcv 
 |-  F/_ x f
41 nfcv 
 |-  F/_ x oR <_
42 nfmpt1 
 |-  F/_ x ( x e. RR |-> if ( x e. A , C , 0 ) )
43 6 42 nfcxfr 
 |-  F/_ x F
44 40 41 43 nfbr 
 |-  F/ x f oR <_ F
45 39 44 nfan 
 |-  F/ x ( f e. dom S.1 /\ f oR <_ F )
46 nfv 
 |-  F/ x g e. dom S.1
47 nfcv 
 |-  F/_ x g
48 nfmpt1 
 |-  F/_ x ( x e. RR |-> if ( x e. B , C , 0 ) )
49 7 48 nfcxfr 
 |-  F/_ x G
50 47 41 49 nfbr 
 |-  F/ x g oR <_ G
51 46 50 nfan 
 |-  F/ x ( g e. dom S.1 /\ g oR <_ G )
52 45 51 nfan 
 |-  F/ x ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) )
53 38 52 nfan 
 |-  F/ x ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) )
54 eldifi 
 |-  ( x e. ( RR \ ( A i^i B ) ) -> x e. RR )
55 i1ff 
 |-  ( f e. dom S.1 -> f : RR --> RR )
56 27 55 syl 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> f : RR --> RR )
57 56 ffnd 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> f Fn RR )
58 i1ff 
 |-  ( g e. dom S.1 -> g : RR --> RR )
59 28 58 syl 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> g : RR --> RR )
60 59 ffnd 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> g Fn RR )
61 reex 
 |-  RR e. _V
62 61 a1i 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> RR e. _V )
63 inidm 
 |-  ( RR i^i RR ) = RR
64 eqidd 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. RR ) -> ( f ` x ) = ( f ` x ) )
65 eqidd 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. RR ) -> ( g ` x ) = ( g ` x ) )
66 57 60 62 62 63 64 65 ofval 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. RR ) -> ( ( f oF + g ) ` x ) = ( ( f ` x ) + ( g ` x ) ) )
67 54 66 sylan2 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f oF + g ) ` x ) = ( ( f ` x ) + ( g ` x ) ) )
68 ffvelcdm 
 |-  ( ( f : RR --> RR /\ x e. RR ) -> ( f ` x ) e. RR )
69 56 54 68 syl2an 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( f ` x ) e. RR )
70 ffvelcdm 
 |-  ( ( g : RR --> RR /\ x e. RR ) -> ( g ` x ) e. RR )
71 59 54 70 syl2an 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( g ` x ) e. RR )
72 69 71 readdcld 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f ` x ) + ( g ` x ) ) e. RR )
73 72 rexrd 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f ` x ) + ( g ` x ) ) e. RR* )
74 73 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + ( g ` x ) ) e. RR* )
75 69 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) e. RR )
76 75 rexrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) e. RR* )
77 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
78 ffvelcdm 
 |-  ( ( H : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( H ` x ) e. ( 0 [,] +oo ) )
79 30 54 78 syl2an 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( H ` x ) e. ( 0 [,] +oo ) )
80 77 79 sselid 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( H ` x ) e. RR* )
81 80 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( H ` x ) e. RR* )
82 71 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( g ` x ) e. RR )
83 0red 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> 0 e. RR )
84 simprrr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> g oR <_ G )
85 61 a1i 
 |-  ( ( ph /\ g Fn RR ) -> RR e. _V )
86 fvexd 
 |-  ( ( ( ph /\ g Fn RR ) /\ x e. RR ) -> ( g ` x ) e. _V )
87 ssun2 
 |-  B C_ ( A u. B )
88 87 4 sseqtrrid 
 |-  ( ph -> B C_ U )
89 88 sselda 
 |-  ( ( ph /\ x e. B ) -> x e. U )
90 89 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. B ) -> x e. U )
91 90 11 syldan 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. B ) -> C e. ( 0 [,] +oo ) )
92 12 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. B ) -> 0 e. ( 0 [,] +oo ) )
93 91 92 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. B , C , 0 ) e. ( 0 [,] +oo ) )
94 93 adantlr 
 |-  ( ( ( ph /\ g Fn RR ) /\ x e. RR ) -> if ( x e. B , C , 0 ) e. ( 0 [,] +oo ) )
95 simpr 
 |-  ( ( ph /\ g Fn RR ) -> g Fn RR )
96 dffn5 
 |-  ( g Fn RR <-> g = ( x e. RR |-> ( g ` x ) ) )
97 95 96 sylib 
 |-  ( ( ph /\ g Fn RR ) -> g = ( x e. RR |-> ( g ` x ) ) )
98 7 a1i 
 |-  ( ( ph /\ g Fn RR ) -> G = ( x e. RR |-> if ( x e. B , C , 0 ) ) )
99 85 86 94 97 98 ofrfval2 
 |-  ( ( ph /\ g Fn RR ) -> ( g oR <_ G <-> A. x e. RR ( g ` x ) <_ if ( x e. B , C , 0 ) ) )
100 60 99 syldan 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( g oR <_ G <-> A. x e. RR ( g ` x ) <_ if ( x e. B , C , 0 ) ) )
101 84 100 mpbid 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> A. x e. RR ( g ` x ) <_ if ( x e. B , C , 0 ) )
102 101 r19.21bi 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. RR ) -> ( g ` x ) <_ if ( x e. B , C , 0 ) )
103 54 102 sylan2 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( g ` x ) <_ if ( x e. B , C , 0 ) )
104 103 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( g ` x ) <_ if ( x e. B , C , 0 ) )
105 eldifn 
 |-  ( x e. ( RR \ ( A i^i B ) ) -> -. x e. ( A i^i B ) )
106 105 adantl 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> -. x e. ( A i^i B ) )
107 elin 
 |-  ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
108 106 107 sylnib 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> -. ( x e. A /\ x e. B ) )
109 imnan 
 |-  ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
110 108 109 sylibr 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( x e. A -> -. x e. B ) )
111 110 imp 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> -. x e. B )
112 111 iffalsed 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> if ( x e. B , C , 0 ) = 0 )
113 104 112 breqtrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( g ` x ) <_ 0 )
114 82 83 75 113 leadd2dd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( ( f ` x ) + 0 ) )
115 75 recnd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) e. CC )
116 115 addridd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + 0 ) = ( f ` x ) )
117 114 116 breqtrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( f ` x ) )
118 simprlr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> f oR <_ F )
119 61 a1i 
 |-  ( ( ph /\ f Fn RR ) -> RR e. _V )
120 fvexd 
 |-  ( ( ( ph /\ f Fn RR ) /\ x e. RR ) -> ( f ` x ) e. _V )
121 ssun1 
 |-  A C_ ( A u. B )
122 121 4 sseqtrrid 
 |-  ( ph -> A C_ U )
123 122 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. U )
124 123 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. A ) -> x e. U )
125 124 11 syldan 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. A ) -> C e. ( 0 [,] +oo ) )
126 12 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
127 125 126 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,] +oo ) )
128 127 adantlr 
 |-  ( ( ( ph /\ f Fn RR ) /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,] +oo ) )
129 simpr 
 |-  ( ( ph /\ f Fn RR ) -> f Fn RR )
130 dffn5 
 |-  ( f Fn RR <-> f = ( x e. RR |-> ( f ` x ) ) )
131 129 130 sylib 
 |-  ( ( ph /\ f Fn RR ) -> f = ( x e. RR |-> ( f ` x ) ) )
132 6 a1i 
 |-  ( ( ph /\ f Fn RR ) -> F = ( x e. RR |-> if ( x e. A , C , 0 ) ) )
133 119 120 128 131 132 ofrfval2 
 |-  ( ( ph /\ f Fn RR ) -> ( f oR <_ F <-> A. x e. RR ( f ` x ) <_ if ( x e. A , C , 0 ) ) )
134 57 133 syldan 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( f oR <_ F <-> A. x e. RR ( f ` x ) <_ if ( x e. A , C , 0 ) ) )
135 118 134 mpbid 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> A. x e. RR ( f ` x ) <_ if ( x e. A , C , 0 ) )
136 135 r19.21bi 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. RR ) -> ( f ` x ) <_ if ( x e. A , C , 0 ) )
137 54 136 sylan2 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( f ` x ) <_ if ( x e. A , C , 0 ) )
138 137 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) <_ if ( x e. A , C , 0 ) )
139 122 ad2antrr 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> A C_ U )
140 139 sselda 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> x e. U )
141 140 iftrued 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> if ( x e. U , C , 0 ) = C )
142 simpr 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. RR ) -> x e. RR )
143 14 adantlr 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. RR ) -> if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) )
144 8 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
145 142 143 144 syl2anc 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. RR ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
146 54 145 sylan2 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
147 146 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
148 iftrue 
 |-  ( x e. A -> if ( x e. A , C , 0 ) = C )
149 148 adantl 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> if ( x e. A , C , 0 ) = C )
150 141 147 149 3eqtr4d 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( H ` x ) = if ( x e. A , C , 0 ) )
151 138 150 breqtrrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) <_ ( H ` x ) )
152 74 76 81 117 151 xrletrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( H ` x ) )
153 73 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( ( f ` x ) + ( g ` x ) ) e. RR* )
154 71 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) e. RR )
155 154 rexrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) e. RR* )
156 80 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( H ` x ) e. RR* )
157 69 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( f ` x ) e. RR )
158 0red 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> 0 e. RR )
159 137 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( f ` x ) <_ if ( x e. A , C , 0 ) )
160 iffalse 
 |-  ( -. x e. A -> if ( x e. A , C , 0 ) = 0 )
161 160 adantl 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> if ( x e. A , C , 0 ) = 0 )
162 159 161 breqtrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( f ` x ) <_ 0 )
163 157 158 154 162 leadd1dd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( 0 + ( g ` x ) ) )
164 154 recnd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) e. CC )
165 164 addlidd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( 0 + ( g ` x ) ) = ( g ` x ) )
166 163 165 breqtrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( g ` x ) )
167 103 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) <_ if ( x e. B , C , 0 ) )
168 146 adantr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
169 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> U = ( A u. B ) )
170 169 eleq2d 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( x e. U <-> x e. ( A u. B ) ) )
171 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
172 biorf 
 |-  ( -. x e. A -> ( x e. B <-> ( x e. A \/ x e. B ) ) )
173 171 172 bitr4id 
 |-  ( -. x e. A -> ( x e. ( A u. B ) <-> x e. B ) )
174 173 adantl 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( x e. ( A u. B ) <-> x e. B ) )
175 170 174 bitrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( x e. U <-> x e. B ) )
176 175 ifbid 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> if ( x e. U , C , 0 ) = if ( x e. B , C , 0 ) )
177 168 176 eqtrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( H ` x ) = if ( x e. B , C , 0 ) )
178 167 177 breqtrrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) <_ ( H ` x ) )
179 153 155 156 166 178 xrletrd 
 |-  ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( H ` x ) )
180 152 179 pm2.61dan 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( H ` x ) )
181 67 180 eqbrtrd 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f oF + g ) ` x ) <_ ( H ` x ) )
182 181 ex 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( x e. ( RR \ ( A i^i B ) ) -> ( ( f oF + g ) ` x ) <_ ( H ` x ) ) )
183 53 182 ralrimi 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> A. x e. ( RR \ ( A i^i B ) ) ( ( f oF + g ) ` x ) <_ ( H ` x ) )
184 nfv 
 |-  F/ y ( ( f oF + g ) ` x ) <_ ( H ` x )
185 nfcv 
 |-  F/_ x ( ( f oF + g ) ` y )
186 nfcv 
 |-  F/_ x <_
187 nfmpt1 
 |-  F/_ x ( x e. RR |-> if ( x e. U , C , 0 ) )
188 8 187 nfcxfr 
 |-  F/_ x H
189 nfcv 
 |-  F/_ x y
190 188 189 nffv 
 |-  F/_ x ( H ` y )
191 185 186 190 nfbr 
 |-  F/ x ( ( f oF + g ) ` y ) <_ ( H ` y )
192 fveq2 
 |-  ( x = y -> ( ( f oF + g ) ` x ) = ( ( f oF + g ) ` y ) )
193 fveq2 
 |-  ( x = y -> ( H ` x ) = ( H ` y ) )
194 192 193 breq12d 
 |-  ( x = y -> ( ( ( f oF + g ) ` x ) <_ ( H ` x ) <-> ( ( f oF + g ) ` y ) <_ ( H ` y ) ) )
195 184 191 194 cbvralw 
 |-  ( A. x e. ( RR \ ( A i^i B ) ) ( ( f oF + g ) ` x ) <_ ( H ` x ) <-> A. y e. ( RR \ ( A i^i B ) ) ( ( f oF + g ) ` y ) <_ ( H ` y ) )
196 183 195 sylib 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> A. y e. ( RR \ ( A i^i B ) ) ( ( f oF + g ) ` y ) <_ ( H ` y ) )
197 196 r19.21bi 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( ( f oF + g ) ` y ) <_ ( H ` y ) )
198 30 31 36 37 197 itg2uba 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( S.1 ` ( f oF + g ) ) <_ ( S.2 ` H ) )
199 29 198 eqbrtrrd 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( ( S.1 ` f ) + ( S.1 ` g ) ) <_ ( S.2 ` H ) )
200 26 adantrr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( S.1 ` f ) e. RR )
201 itg1cl 
 |-  ( g e. dom S.1 -> ( S.1 ` g ) e. RR )
202 28 201 syl 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( S.1 ` g ) e. RR )
203 23 adantr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( S.2 ` H ) e. RR )
204 200 202 203 leaddsub2d 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( ( ( S.1 ` f ) + ( S.1 ` g ) ) <_ ( S.2 ` H ) <-> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) )
205 199 204 mpbid 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) )
206 205 anassrs 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) )
207 206 expr 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ g e. dom S.1 ) -> ( g oR <_ G -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) )
208 207 ralrimiva 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> A. g e. dom S.1 ( g oR <_ G -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) )
209 93 7 fmptd 
 |-  ( ph -> G : RR --> ( 0 [,] +oo ) )
210 209 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> G : RR --> ( 0 [,] +oo ) )
211 24 26 resubcld 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR )
212 211 rexrd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR* )
213 itg2leub 
 |-  ( ( G : RR --> ( 0 [,] +oo ) /\ ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR* ) -> ( ( S.2 ` G ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) <-> A. g e. dom S.1 ( g oR <_ G -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) ) )
214 210 212 213 syl2anc 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( ( S.2 ` G ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) <-> A. g e. dom S.1 ( g oR <_ G -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) ) )
215 208 214 mpbird 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( S.2 ` G ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) )
216 21 24 26 215 lesubd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) )
217 216 expr 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
218 217 ralrimiva 
 |-  ( ph -> A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
219 127 6 fmptd 
 |-  ( ph -> F : RR --> ( 0 [,] +oo ) )
220 23 10 resubcld 
 |-  ( ph -> ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR )
221 220 rexrd 
 |-  ( ph -> ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR* )
222 itg2leub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR* ) -> ( ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) <-> A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) ) )
223 219 221 222 syl2anc 
 |-  ( ph -> ( ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) <-> A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) ) )
224 218 223 mpbird 
 |-  ( ph -> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) )
225 leaddsub 
 |-  ( ( ( S.2 ` F ) e. RR /\ ( S.2 ` G ) e. RR /\ ( S.2 ` H ) e. RR ) -> ( ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) <-> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
226 9 10 23 225 syl3anc 
 |-  ( ph -> ( ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) <-> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
227 224 226 mpbird 
 |-  ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) )
228 17 19 20 227 xrletrid 
 |-  ( ph -> ( S.2 ` H ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )