This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 dffn5 
 |-  ( g Fn RR <-> g = ( x e. RR |-> ( g ` x ) ) )
96 95 bilani 
 |-  ( ( ph /\ g Fn RR ) -> g = ( x e. RR |-> ( g ` x ) ) )
97 7 a1i 
 |-  ( ( ph /\ g Fn RR ) -> G = ( x e. RR |-> if ( x e. B , C , 0 ) ) )
98 85 86 94 96 97 ofrfval2 
 |-  ( ( ph /\ g Fn RR ) -> ( g oR <_ G <-> A. x e. RR ( g ` x ) <_ if ( x e. B , C , 0 ) ) )
99 60 98 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 ) ) )
100 84 99 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 ) )
101 100 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 ) )
102 54 101 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 ) )
103 102 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 ) )
104 eldifn 
 |-  ( x e. ( RR \ ( A i^i B ) ) -> -. x e. ( A i^i B ) )
105 104 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 ) )
106 elin 
 |-  ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
107 105 106 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 ) )
108 imnan 
 |-  ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
109 107 108 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 ) )
110 109 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 )
111 110 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 )
112 103 111 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 )
113 82 83 75 112 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 ) )
114 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 )
115 114 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 ) )
116 113 115 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 ) )
117 simprlr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> f oR <_ F )
118 61 a1i 
 |-  ( ( ph /\ f Fn RR ) -> RR e. _V )
119 fvexd 
 |-  ( ( ( ph /\ f Fn RR ) /\ x e. RR ) -> ( f ` x ) e. _V )
120 ssun1 
 |-  A C_ ( A u. B )
121 120 4 sseqtrrid 
 |-  ( ph -> A C_ U )
122 121 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. U )
123 122 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. A ) -> x e. U )
124 123 11 syldan 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. A ) -> C e. ( 0 [,] +oo ) )
125 12 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
126 124 125 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,] +oo ) )
127 126 adantlr 
 |-  ( ( ( ph /\ f Fn RR ) /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,] +oo ) )
128 dffn5 
 |-  ( f Fn RR <-> f = ( x e. RR |-> ( f ` x ) ) )
129 128 bilani 
 |-  ( ( ph /\ f Fn RR ) -> f = ( x e. RR |-> ( f ` x ) ) )
130 6 a1i 
 |-  ( ( ph /\ f Fn RR ) -> F = ( x e. RR |-> if ( x e. A , C , 0 ) ) )
131 118 119 127 129 130 ofrfval2 
 |-  ( ( ph /\ f Fn RR ) -> ( f oR <_ F <-> A. x e. RR ( f ` x ) <_ if ( x e. A , C , 0 ) ) )
132 57 131 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 ) ) )
133 117 132 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 ) )
134 133 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 ) )
135 54 134 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 ) )
136 135 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 ) )
137 121 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 )
138 137 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 )
139 138 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 )
140 simpr 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) /\ x e. RR ) -> x e. RR )
141 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 ) )
142 8 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
143 140 141 142 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 ) )
144 54 143 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 ) )
145 144 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 ) )
146 iftrue 
 |-  ( x e. A -> if ( x e. A , C , 0 ) = C )
147 146 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 )
148 139 145 147 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 ) )
149 136 148 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 ) )
150 74 76 81 116 149 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 ) )
151 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* )
152 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 )
153 152 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* )
154 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* )
155 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 )
156 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 )
157 135 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 ) )
158 iffalse 
 |-  ( -. x e. A -> if ( x e. A , C , 0 ) = 0 )
159 158 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 )
160 157 159 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 )
161 155 156 152 160 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 ) ) )
162 152 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 )
163 162 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 ) )
164 161 163 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 ) )
165 102 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 ) )
166 144 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 ) )
167 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 ) )
168 167 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 ) ) )
169 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
170 biorf 
 |-  ( -. x e. A -> ( x e. B <-> ( x e. A \/ x e. B ) ) )
171 169 170 bitr4id 
 |-  ( -. x e. A -> ( x e. ( A u. B ) <-> x e. B ) )
172 171 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 ) )
173 168 172 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 ) )
174 173 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 ) )
175 166 174 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 ) )
176 165 175 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 ) )
177 151 153 154 164 176 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 ) )
178 150 177 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 ) )
179 67 178 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 ) )
180 179 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 ) ) )
181 53 180 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 ) )
182 nfv 
 |-  F/ y ( ( f oF + g ) ` x ) <_ ( H ` x )
183 nfcv 
 |-  F/_ x ( ( f oF + g ) ` y )
184 nfcv 
 |-  F/_ x <_
185 nfmpt1 
 |-  F/_ x ( x e. RR |-> if ( x e. U , C , 0 ) )
186 8 185 nfcxfr 
 |-  F/_ x H
187 nfcv 
 |-  F/_ x y
188 186 187 nffv 
 |-  F/_ x ( H ` y )
189 183 184 188 nfbr 
 |-  F/ x ( ( f oF + g ) ` y ) <_ ( H ` y )
190 fveq2 
 |-  ( x = y -> ( ( f oF + g ) ` x ) = ( ( f oF + g ) ` y ) )
191 fveq2 
 |-  ( x = y -> ( H ` x ) = ( H ` y ) )
192 190 191 breq12d 
 |-  ( x = y -> ( ( ( f oF + g ) ` x ) <_ ( H ` x ) <-> ( ( f oF + g ) ` y ) <_ ( H ` y ) ) )
193 182 189 192 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 ) )
194 181 193 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 ) )
195 194 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 ) )
196 30 31 36 37 195 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 ) )
197 29 196 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 ) )
198 26 adantrr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( S.1 ` f ) e. RR )
199 itg1cl 
 |-  ( g e. dom S.1 -> ( S.1 ` g ) e. RR )
200 28 199 syl 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( S.1 ` g ) e. RR )
201 23 adantr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ F ) /\ ( g e. dom S.1 /\ g oR <_ G ) ) ) -> ( S.2 ` H ) e. RR )
202 198 200 201 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 ) ) ) )
203 197 202 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 ) ) )
204 203 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 ) ) )
205 204 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 ) ) ) )
206 205 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 ) ) ) )
207 93 7 fmptd 
 |-  ( ph -> G : RR --> ( 0 [,] +oo ) )
208 207 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> G : RR --> ( 0 [,] +oo ) )
209 24 26 resubcld 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR )
210 209 rexrd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR* )
211 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 ) ) ) ) )
212 208 210 211 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 ) ) ) ) )
213 206 212 mpbird 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( S.2 ` G ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) )
214 21 24 26 213 lesubd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) )
215 214 expr 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
216 215 ralrimiva 
 |-  ( ph -> A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
217 126 6 fmptd 
 |-  ( ph -> F : RR --> ( 0 [,] +oo ) )
218 23 10 resubcld 
 |-  ( ph -> ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR )
219 218 rexrd 
 |-  ( ph -> ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR* )
220 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 ) ) ) ) )
221 217 219 220 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 ) ) ) ) )
222 216 221 mpbird 
 |-  ( ph -> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) )
223 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 ) ) ) )
224 9 10 23 223 syl3anc 
 |-  ( ph -> ( ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) <-> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
225 222 224 mpbird 
 |-  ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) )
226 17 19 20 225 xrletrid 
 |-  ( ph -> ( S.2 ` H ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )