Metamath Proof Explorer

Theorem oprpiece1res2

Description: Restriction to the second part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010) (Proof shortened by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses oprpiece1.1 
|- A e. RR
oprpiece1.2 
|- B e. RR
oprpiece1.3 
|- A <_ B
oprpiece1.4 
|- R e. _V
oprpiece1.5 
|- S e. _V
oprpiece1.6 
|- K e. ( A [,] B )
oprpiece1.7 
|- F = ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) )
oprpiece1.9 
|- ( x = K -> R = P )
oprpiece1.10 
|- ( x = K -> S = Q )
oprpiece1.11 
|- ( y e. C -> P = Q )
oprpiece1.12 
|- G = ( x e. ( K [,] B ) , y e. C |-> S )
Assertion oprpiece1res2 
|- ( F |` ( ( K [,] B ) X. C ) ) = G

Proof

Step Hyp Ref Expression
1 oprpiece1.1 
 |-  A e. RR
2 oprpiece1.2 
 |-  B e. RR
3 oprpiece1.3 
 |-  A <_ B
4 oprpiece1.4 
 |-  R e. _V
5 oprpiece1.5 
 |-  S e. _V
6 oprpiece1.6 
 |-  K e. ( A [,] B )
7 oprpiece1.7 
 |-  F = ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) )
8 oprpiece1.9 
 |-  ( x = K -> R = P )
9 oprpiece1.10 
 |-  ( x = K -> S = Q )
10 oprpiece1.11 
 |-  ( y e. C -> P = Q )
11 oprpiece1.12 
 |-  G = ( x e. ( K [,] B ) , y e. C |-> S )
12 1 rexri 
 |-  A e. RR*
13 2 rexri 
 |-  B e. RR*
14 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
15 12 13 3 14 mp3an 
 |-  B e. ( A [,] B )
16 iccss2 
 |-  ( ( K e. ( A [,] B ) /\ B e. ( A [,] B ) ) -> ( K [,] B ) C_ ( A [,] B ) )
17 6 15 16 mp2an 
 |-  ( K [,] B ) C_ ( A [,] B )
18 ssid 
 |-  C C_ C
19 resmpo 
 |-  ( ( ( K [,] B ) C_ ( A [,] B ) /\ C C_ C ) -> ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( K [,] B ) X. C ) ) = ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) )
20 17 18 19 mp2an 
 |-  ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( K [,] B ) X. C ) ) = ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) )
21 7 reseq1i 
 |-  ( F |` ( ( K [,] B ) X. C ) ) = ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( K [,] B ) X. C ) )
22 10 ad2antlr 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> P = Q )
23 simpr 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> x <_ K )
24 1 2 elicc2i 
 |-  ( K e. ( A [,] B ) <-> ( K e. RR /\ A <_ K /\ K <_ B ) )
25 24 simp1bi 
 |-  ( K e. ( A [,] B ) -> K e. RR )
26 6 25 ax-mp 
 |-  K e. RR
27 26 2 elicc2i 
 |-  ( x e. ( K [,] B ) <-> ( x e. RR /\ K <_ x /\ x <_ B ) )
28 27 simp2bi 
 |-  ( x e. ( K [,] B ) -> K <_ x )
29 28 ad2antrr 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> K <_ x )
30 27 simp1bi 
 |-  ( x e. ( K [,] B ) -> x e. RR )
31 30 ad2antrr 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> x e. RR )
32 letri3 
 |-  ( ( x e. RR /\ K e. RR ) -> ( x = K <-> ( x <_ K /\ K <_ x ) ) )
33 31 26 32 sylancl 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> ( x = K <-> ( x <_ K /\ K <_ x ) ) )
34 23 29 33 mpbir2and 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> x = K )
35 34 8 syl 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> R = P )
36 34 9 syl 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> S = Q )
37 22 35 36 3eqtr4d 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> R = S )
38 eqidd 
 |-  ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ -. x <_ K ) -> S = S )
39 37 38 ifeqda 
 |-  ( ( x e. ( K [,] B ) /\ y e. C ) -> if ( x <_ K , R , S ) = S )
40 39 mpoeq3ia 
 |-  ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) = ( x e. ( K [,] B ) , y e. C |-> S )
41 11 40 eqtr4i 
 |-  G = ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) )
42 20 21 41 3eqtr4i 
 |-  ( F |` ( ( K [,] B ) X. C ) ) = G