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\upharpoonright }_{\left(\left[A,K\right]\times 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)\upharpoonright }_{\left(\left[A,K\right]\times 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)\upharpoonright }_{\left(\left[A,K\right]\times 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\upharpoonright }_{\left(\left[A,K\right]\times C\right)}={\left(x\in \left[A,B\right],y\in C⟼if\left(x\le K,R,S\right)\right)\upharpoonright }_{\left(\left[A,K\right]\times 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\upharpoonright }_{\left(\left[A,K\right]\times C\right)}=G$$