Metamath Proof Explorer


Theorem oprpiece1res1

Description: Restriction to the first 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.8
|- G = ( x e. ( A [,] K ) , y e. C |-> R )
Assertion oprpiece1res1
|- ( F |` ( ( A [,] K ) 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.8
 |-  G = ( x e. ( A [,] K ) , y e. C |-> R )
9 1 rexri
 |-  A e. RR*
10 2 rexri
 |-  B e. RR*
11 lbicc2
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
12 9 10 3 11 mp3an
 |-  A e. ( A [,] B )
13 iccss2
 |-  ( ( A e. ( A [,] B ) /\ K e. ( A [,] B ) ) -> ( A [,] K ) C_ ( A [,] B ) )
14 12 6 13 mp2an
 |-  ( A [,] K ) C_ ( A [,] B )
15 ssid
 |-  C C_ C
16 resmpo
 |-  ( ( ( A [,] K ) C_ ( A [,] B ) /\ C C_ C ) -> ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( A [,] K ) X. C ) ) = ( x e. ( A [,] K ) , y e. C |-> if ( x <_ K , R , S ) ) )
17 14 15 16 mp2an
 |-  ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( A [,] K ) X. C ) ) = ( x e. ( A [,] K ) , y e. C |-> if ( x <_ K , R , S ) )
18 7 reseq1i
 |-  ( F |` ( ( A [,] K ) X. C ) ) = ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( A [,] K ) X. C ) )
19 eliccxr
 |-  ( K e. ( A [,] B ) -> K e. RR* )
20 6 19 ax-mp
 |-  K e. RR*
21 iccleub
 |-  ( ( A e. RR* /\ K e. RR* /\ x e. ( A [,] K ) ) -> x <_ K )
22 9 20 21 mp3an12
 |-  ( x e. ( A [,] K ) -> x <_ K )
23 22 iftrued
 |-  ( x e. ( A [,] K ) -> if ( x <_ K , R , S ) = R )
24 23 adantr
 |-  ( ( x e. ( A [,] K ) /\ y e. C ) -> if ( x <_ K , R , S ) = R )
25 24 mpoeq3ia
 |-  ( x e. ( A [,] K ) , y e. C |-> if ( x <_ K , R , S ) ) = ( x e. ( A [,] K ) , y e. C |-> R )
26 8 25 eqtr4i
 |-  G = ( x e. ( A [,] K ) , y e. C |-> if ( x <_ K , R , S ) )
27 17 18 26 3eqtr4i
 |-  ( F |` ( ( A [,] K ) X. C ) ) = G