Metamath Proof Explorer

Theorem ibladdlem

Description: Lemma for ibladd . (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses ibladd.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
ibladd.2 
|- ( ( ph /\ x e. A ) -> C e. RR )
ibladd.3 
|- ( ( ph /\ x e. A ) -> D = ( B + C ) )
ibladd.4 
|- ( ph -> ( x e. A |-> B ) e. MblFn )
ibladd.5 
|- ( ph -> ( x e. A |-> C ) e. MblFn )
ibladd.6 
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR )
ibladd.7 
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR )
Assertion ibladdlem 
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )

Proof

Step Hyp Ref Expression
1 ibladd.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 ibladd.2 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
3 ibladd.3 
 |-  ( ( ph /\ x e. A ) -> D = ( B + C ) )
4 ibladd.4 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
5 ibladd.5 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
6 ibladd.6 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR )
7 ibladd.7 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR )
8 ifan 
 |-  if ( ( x e. A /\ 0 <_ D ) , D , 0 ) = if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 )
9 1 2 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. RR )
10 3 9 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> D e. RR )
11 0re 
 |-  0 e. RR
12 ifcl 
 |-  ( ( D e. RR /\ 0 e. RR ) -> if ( 0 <_ D , D , 0 ) e. RR )
13 10 11 12 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) e. RR )
14 13 rexrd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) e. RR* )
15 max1 
 |-  ( ( 0 e. RR /\ D e. RR ) -> 0 <_ if ( 0 <_ D , D , 0 ) )
16 11 10 15 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ D , D , 0 ) )
17 elxrge0 
 |-  ( if ( 0 <_ D , D , 0 ) e. ( 0 [,] +oo ) <-> ( if ( 0 <_ D , D , 0 ) e. RR* /\ 0 <_ if ( 0 <_ D , D , 0 ) ) )
18 14 16 17 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) e. ( 0 [,] +oo ) )
19 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
20 19 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
21 18 20 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) e. ( 0 [,] +oo ) )
22 21 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) e. ( 0 [,] +oo ) )
23 8 22 eqeltrid 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) e. ( 0 [,] +oo ) )
24 23 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) : RR --> ( 0 [,] +oo ) )
25 reex 
 |-  RR e. _V
26 25 a1i 
 |-  ( ph -> RR e. _V )
27 ifan 
 |-  if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 )
28 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
29 1 11 28 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
30 11 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. RR )
31 29 30 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) e. RR )
32 27 31 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. RR )
33 32 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. RR )
34 ifan 
 |-  if ( ( x e. A /\ 0 <_ C ) , C , 0 ) = if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 )
35 ifcl 
 |-  ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
36 2 11 35 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
37 36 30 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) e. RR )
38 34 37 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. RR )
39 38 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. RR )
40 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) )
41 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) )
42 26 33 39 40 41 offval2 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) = ( x e. RR |-> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) )
43 iftrue 
 |-  ( x e. A -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
44 ibar 
 |-  ( x e. A -> ( 0 <_ B <-> ( x e. A /\ 0 <_ B ) ) )
45 44 ifbid 
 |-  ( x e. A -> if ( 0 <_ B , B , 0 ) = if ( ( x e. A /\ 0 <_ B ) , B , 0 ) )
46 ibar 
 |-  ( x e. A -> ( 0 <_ C <-> ( x e. A /\ 0 <_ C ) ) )
47 46 ifbid 
 |-  ( x e. A -> if ( 0 <_ C , C , 0 ) = if ( ( x e. A /\ 0 <_ C ) , C , 0 ) )
48 45 47 oveq12d 
 |-  ( x e. A -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) )
49 43 48 eqtr2d 
 |-  ( x e. A -> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
50 00id 
 |-  ( 0 + 0 ) = 0
51 simpl 
 |-  ( ( x e. A /\ 0 <_ B ) -> x e. A )
52 51 con3i 
 |-  ( -. x e. A -> -. ( x e. A /\ 0 <_ B ) )
53 52 iffalsed 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = 0 )
54 simpl 
 |-  ( ( x e. A /\ 0 <_ C ) -> x e. A )
55 54 con3i 
 |-  ( -. x e. A -> -. ( x e. A /\ 0 <_ C ) )
56 55 iffalsed 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) = 0 )
57 53 56 oveq12d 
 |-  ( -. x e. A -> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = ( 0 + 0 ) )
58 iffalse 
 |-  ( -. x e. A -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = 0 )
59 50 57 58 3eqtr4a 
 |-  ( -. x e. A -> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
60 49 59 pm2.61i 
 |-  ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 )
61 60 mpteq2i 
 |-  ( x e. RR |-> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
62 42 61 eqtrdi 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
63 62 fveq2d 
 |-  ( ph -> ( S.2 ` ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) )
64 4 1 mbfdm2 
 |-  ( ph -> A e. dom vol )
65 mblss 
 |-  ( A e. dom vol -> A C_ RR )
66 64 65 syl 
 |-  ( ph -> A C_ RR )
67 rembl 
 |-  RR e. dom vol
68 67 a1i 
 |-  ( ph -> RR e. dom vol )
69 32 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. RR )
70 eldifn 
 |-  ( x e. ( RR \ A ) -> -. x e. A )
71 70 adantl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> -. x e. A )
72 71 intnanrd 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> -. ( x e. A /\ 0 <_ B ) )
73 72 iffalsed 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = 0 )
74 45 mpteq2ia 
 |-  ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( x e. A |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) )
75 1 4 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
76 74 75 eqeltrrid 
 |-  ( ph -> ( x e. A |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) e. MblFn )
77 66 68 69 73 76 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) e. MblFn )
78 max1 
 |-  ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
79 11 1 78 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
80 elrege0 
 |-  ( if ( 0 <_ B , B , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ B , B , 0 ) e. RR /\ 0 <_ if ( 0 <_ B , B , 0 ) ) )
81 29 79 80 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. ( 0 [,) +oo ) )
82 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
83 82 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
84 81 83 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) e. ( 0 [,) +oo ) )
85 27 84 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. ( 0 [,) +oo ) )
86 85 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. ( 0 [,) +oo ) )
87 86 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) : RR --> ( 0 [,) +oo ) )
88 38 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. RR )
89 71 56 syl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) = 0 )
90 47 mpteq2ia 
 |-  ( x e. A |-> if ( 0 <_ C , C , 0 ) ) = ( x e. A |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) )
91 2 5 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ C , C , 0 ) ) e. MblFn )
92 90 91 eqeltrrid 
 |-  ( ph -> ( x e. A |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) e. MblFn )
93 66 68 88 89 92 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) e. MblFn )
94 max1 
 |-  ( ( 0 e. RR /\ C e. RR ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
95 11 2 94 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
96 elrege0 
 |-  ( if ( 0 <_ C , C , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ C , C , 0 ) e. RR /\ 0 <_ if ( 0 <_ C , C , 0 ) ) )
97 36 95 96 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. ( 0 [,) +oo ) )
98 97 83 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) e. ( 0 [,) +oo ) )
99 34 98 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. ( 0 [,) +oo ) )
100 99 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. ( 0 [,) +oo ) )
101 100 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) : RR --> ( 0 [,) +oo ) )
102 77 87 6 93 101 7 itg2add 
 |-  ( ph -> ( S.2 ` ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) )
103 63 102 eqtr3d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) )
104 6 7 readdcld 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) e. RR )
105 103 104 eqeltrd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) e. RR )
106 29 36 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
107 106 rexrd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR* )
108 29 36 79 95 addge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
109 elxrge0 
 |-  ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. ( 0 [,] +oo ) <-> ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR* /\ 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
110 107 108 109 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. ( 0 [,] +oo ) )
111 110 20 ifclda 
 |-  ( ph -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) e. ( 0 [,] +oo ) )
112 111 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) e. ( 0 [,] +oo ) )
113 112 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
114 max2 
 |-  ( ( 0 e. RR /\ B e. RR ) -> B <_ if ( 0 <_ B , B , 0 ) )
115 11 1 114 sylancr 
 |-  ( ( ph /\ x e. A ) -> B <_ if ( 0 <_ B , B , 0 ) )
116 max2 
 |-  ( ( 0 e. RR /\ C e. RR ) -> C <_ if ( 0 <_ C , C , 0 ) )
117 11 2 116 sylancr 
 |-  ( ( ph /\ x e. A ) -> C <_ if ( 0 <_ C , C , 0 ) )
118 1 2 29 36 115 117 le2addd 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
119 3 118 eqbrtrd 
 |-  ( ( ph /\ x e. A ) -> D <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
120 breq1 
 |-  ( D = if ( 0 <_ D , D , 0 ) -> ( D <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) <-> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
121 breq1 
 |-  ( 0 = if ( 0 <_ D , D , 0 ) -> ( 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) <-> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
122 120 121 ifboth 
 |-  ( ( D <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) /\ 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) -> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
123 119 108 122 syl2anc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
124 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) = if ( 0 <_ D , D , 0 ) )
125 124 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) = if ( 0 <_ D , D , 0 ) )
126 43 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
127 123 125 126 3brtr4d 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
128 127 ex 
 |-  ( ph -> ( x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
129 0le0 
 |-  0 <_ 0
130 129 a1i 
 |-  ( -. x e. A -> 0 <_ 0 )
131 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) = 0 )
132 130 131 58 3brtr4d 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
133 128 132 pm2.61d1 
 |-  ( ph -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
134 8 133 eqbrtrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
135 134 ralrimivw 
 |-  ( ph -> A. x e. RR if ( ( x e. A /\ 0 <_ D ) , D , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
136 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) )
137 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
138 26 23 112 136 137 ofrfval2 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) <-> A. x e. RR if ( ( x e. A /\ 0 <_ D ) , D , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
139 135 138 mpbird 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
140 itg2le 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) )
141 24 113 139 140 syl3anc 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) )
142 itg2lecl 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )
143 24 105 141 142 syl3anc 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )