# 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}\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.8 ${⊢}{G}=\left({x}\in \left[{A},{K}\right],{y}\in {C}⟼{R}\right)$
Assertion oprpiece1res1 ${⊢}{{F}↾}_{\left(\left[{A},{K}\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.8 ${⊢}{G}=\left({x}\in \left[{A},{K}\right],{y}\in {C}⟼{R}\right)$
9 1 rexri ${⊢}{A}\in {ℝ}^{*}$
10 2 rexri ${⊢}{B}\in {ℝ}^{*}$
11 lbicc2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to {A}\in \left[{A},{B}\right]$
12 9 10 3 11 mp3an ${⊢}{A}\in \left[{A},{B}\right]$
13 iccss2 ${⊢}\left({A}\in \left[{A},{B}\right]\wedge {K}\in \left[{A},{B}\right]\right)\to \left[{A},{K}\right]\subseteq \left[{A},{B}\right]$
14 12 6 13 mp2an ${⊢}\left[{A},{K}\right]\subseteq \left[{A},{B}\right]$
15 ssid ${⊢}{C}\subseteq {C}$
16 resmpo ${⊢}\left(\left[{A},{K}\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[{A},{K}\right]×{C}\right)}=\left({x}\in \left[{A},{K}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)$
17 14 15 16 mp2an ${⊢}{\left({x}\in \left[{A},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)↾}_{\left(\left[{A},{K}\right]×{C}\right)}=\left({x}\in \left[{A},{K}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)$
18 7 reseq1i ${⊢}{{F}↾}_{\left(\left[{A},{K}\right]×{C}\right)}={\left({x}\in \left[{A},{B}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)↾}_{\left(\left[{A},{K}\right]×{C}\right)}$
19 eliccxr ${⊢}{K}\in \left[{A},{B}\right]\to {K}\in {ℝ}^{*}$
20 6 19 ax-mp ${⊢}{K}\in {ℝ}^{*}$
21 iccleub ${⊢}\left({A}\in {ℝ}^{*}\wedge {K}\in {ℝ}^{*}\wedge {x}\in \left[{A},{K}\right]\right)\to {x}\le {K}$
22 9 20 21 mp3an12 ${⊢}{x}\in \left[{A},{K}\right]\to {x}\le {K}$
23 22 iftrued ${⊢}{x}\in \left[{A},{K}\right]\to if\left({x}\le {K},{R},{S}\right)={R}$
24 23 adantr ${⊢}\left({x}\in \left[{A},{K}\right]\wedge {y}\in {C}\right)\to if\left({x}\le {K},{R},{S}\right)={R}$
25 24 mpoeq3ia ${⊢}\left({x}\in \left[{A},{K}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)=\left({x}\in \left[{A},{K}\right],{y}\in {C}⟼{R}\right)$
26 8 25 eqtr4i ${⊢}{G}=\left({x}\in \left[{A},{K}\right],{y}\in {C}⟼if\left({x}\le {K},{R},{S}\right)\right)$
27 17 18 26 3eqtr4i ${⊢}{{F}↾}_{\left(\left[{A},{K}\right]×{C}\right)}={G}$