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