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 \leq B$
	oprpiece1.4	$⊢ R \in V$
	oprpiece1.5	$⊢ S \in V$
	oprpiece1.6	$⊢ K \in [A, B]$
	oprpiece1.7	$⊢ F = (x \in [A, B], y \in C ⟼ if (x \leq K, R, S))$
	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 = (x \in [K, B], y \in C ⟼ S)$
Assertion	oprpiece1res2	$⊢ {F ↾}_{([K, B] \times C)} = G$

Proof

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

Metamath Proof Explorer

Theorem oprpiece1res2

Proof