# 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}\in ℝ$
oprpiece1.2 ${⊢}{B}\in ℝ$
oprpiece1.3 ${⊢}{A}\le {B}$
oprpiece1.4 ${⊢}{R}\in \mathrm{V}$
oprpiece1.5 ${⊢}{S}\in \mathrm{V}$
oprpiece1.6 ${⊢}{K}\in \left[{A},{B}\right]$
oprpiece1.7 ${⊢}{F}=\left({x}\in \left[{A},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)$
oprpiece1.9 ${⊢}{x}={K}\to {R}={P}$
oprpiece1.10 ${⊢}{x}={K}\to {S}={Q}$
oprpiece1.11 ${⊢}{y}\in {C}\to {P}={Q}$
oprpiece1.12 ${⊢}{G}=\left({x}\in \left[{K},{B}\right],{y}\in {C}⟼{S}\right)$
Assertion oprpiece1res2 ${⊢}{{F}↾}_{\left(\left[{K},{B}\right]×{C}\right)}={G}$

### Proof

Step Hyp Ref Expression
1 oprpiece1.1 ${⊢}{A}\in ℝ$
2 oprpiece1.2 ${⊢}{B}\in ℝ$
3 oprpiece1.3 ${⊢}{A}\le {B}$
4 oprpiece1.4 ${⊢}{R}\in \mathrm{V}$
5 oprpiece1.5 ${⊢}{S}\in \mathrm{V}$
6 oprpiece1.6 ${⊢}{K}\in \left[{A},{B}\right]$
7 oprpiece1.7 ${⊢}{F}=\left({x}\in \left[{A},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)$
8 oprpiece1.9 ${⊢}{x}={K}\to {R}={P}$
9 oprpiece1.10 ${⊢}{x}={K}\to {S}={Q}$
10 oprpiece1.11 ${⊢}{y}\in {C}\to {P}={Q}$
11 oprpiece1.12 ${⊢}{G}=\left({x}\in \left[{K},{B}\right],{y}\in {C}⟼{S}\right)$
12 1 rexri ${⊢}{A}\in {ℝ}^{*}$
13 2 rexri ${⊢}{B}\in {ℝ}^{*}$
14 ubicc2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to {B}\in \left[{A},{B}\right]$
15 12 13 3 14 mp3an ${⊢}{B}\in \left[{A},{B}\right]$
16 iccss2 ${⊢}\left({K}\in \left[{A},{B}\right]\wedge {B}\in \left[{A},{B}\right]\right)\to \left[{K},{B}\right]\subseteq \left[{A},{B}\right]$
17 6 15 16 mp2an ${⊢}\left[{K},{B}\right]\subseteq \left[{A},{B}\right]$
18 ssid ${⊢}{C}\subseteq {C}$
19 resmpo ${⊢}\left(\left[{K},{B}\right]\subseteq \left[{A},{B}\right]\wedge {C}\subseteq {C}\right)\to {\left({x}\in \left[{A},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)↾}_{\left(\left[{K},{B}\right]×{C}\right)}=\left({x}\in \left[{K},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)$
20 17 18 19 mp2an ${⊢}{\left({x}\in \left[{A},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)↾}_{\left(\left[{K},{B}\right]×{C}\right)}=\left({x}\in \left[{K},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)$
21 7 reseq1i ${⊢}{{F}↾}_{\left(\left[{K},{B}\right]×{C}\right)}={\left({x}\in \left[{A},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)↾}_{\left(\left[{K},{B}\right]×{C}\right)}$
22 10 ad2antlr ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge {x}\le {K}\right)\to {P}={Q}$
23 simpr ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge {x}\le {K}\right)\to {x}\le {K}$
24 1 2 elicc2i ${⊢}{K}\in \left[{A},{B}\right]↔\left({K}\in ℝ\wedge {A}\le {K}\wedge {K}\le {B}\right)$
25 24 simp1bi ${⊢}{K}\in \left[{A},{B}\right]\to {K}\in ℝ$
26 6 25 ax-mp ${⊢}{K}\in ℝ$
27 26 2 elicc2i ${⊢}{x}\in \left[{K},{B}\right]↔\left({x}\in ℝ\wedge {K}\le {x}\wedge {x}\le {B}\right)$
28 27 simp2bi ${⊢}{x}\in \left[{K},{B}\right]\to {K}\le {x}$
29 28 ad2antrr ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge {x}\le {K}\right)\to {K}\le {x}$
30 27 simp1bi ${⊢}{x}\in \left[{K},{B}\right]\to {x}\in ℝ$
31 30 ad2antrr ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge {x}\le {K}\right)\to {x}\in ℝ$
32 letri3 ${⊢}\left({x}\in ℝ\wedge {K}\in ℝ\right)\to \left({x}={K}↔\left({x}\le {K}\wedge {K}\le {x}\right)\right)$
33 31 26 32 sylancl ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge {x}\le {K}\right)\to \left({x}={K}↔\left({x}\le {K}\wedge {K}\le {x}\right)\right)$
34 23 29 33 mpbir2and ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge {x}\le {K}\right)\to {x}={K}$
35 34 8 syl ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge {x}\le {K}\right)\to {R}={P}$
36 34 9 syl ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge {x}\le {K}\right)\to {S}={Q}$
37 22 35 36 3eqtr4d ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge {x}\le {K}\right)\to {R}={S}$
38 eqidd ${⊢}\left(\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\wedge ¬{x}\le {K}\right)\to {S}={S}$
39 37 38 ifeqda ${⊢}\left({x}\in \left[{K},{B}\right]\wedge {y}\in {C}\right)\to if\left({x}\le {K},{R},{S}\right)={S}$
40 39 mpoeq3ia ${⊢}\left({x}\in \left[{K},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)=\left({x}\in \left[{K},{B}\right],{y}\in {C}⟼{S}\right)$
41 11 40 eqtr4i ${⊢}{G}=\left({x}\in \left[{K},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)$
42 20 21 41 3eqtr4i ${⊢}{{F}↾}_{\left(\left[{K},{B}\right]×{C}\right)}={G}$