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 ⊢ 𝐴 ∈ ℝ
oprpiece1.2 ⊢ 𝐵 ∈ ℝ
oprpiece1.3 ⊢ 𝐴 ≤ 𝐵
oprpiece1.4 ⊢ 𝑅 ∈ V
oprpiece1.5 ⊢ 𝑆 ∈ V
oprpiece1.6 ⊢ 𝐾 ∈ ( 𝐴 [,] 𝐵 )
oprpiece1.7 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) )
oprpiece1.9 ⊢ ( 𝑥 = 𝐾 → 𝑅 = 𝑃 )
oprpiece1.10 ⊢ ( 𝑥 = 𝐾 → 𝑆 = 𝑄 )
oprpiece1.11 ⊢ ( 𝑦 ∈ 𝐶 → 𝑃 = 𝑄 )
oprpiece1.12 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ 𝑆 )
Assertion oprpiece1res2 ( 𝐹 ↾ ( ( 𝐾 [,] 𝐵 ) × 𝐶 ) ) = 𝐺

Proof

Step Hyp Ref Expression
1 oprpiece1.1 ⊢ 𝐴 ∈ ℝ
2 oprpiece1.2 ⊢ 𝐵 ∈ ℝ
3 oprpiece1.3 ⊢ 𝐴 ≤ 𝐵
4 oprpiece1.4 ⊢ 𝑅 ∈ V
5 oprpiece1.5 ⊢ 𝑆 ∈ V
6 oprpiece1.6 ⊢ 𝐾 ∈ ( 𝐴 [,] 𝐵 )
7 oprpiece1.7 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) )
8 oprpiece1.9 ⊢ ( 𝑥 = 𝐾 → 𝑅 = 𝑃 )
9 oprpiece1.10 ⊢ ( 𝑥 = 𝐾 → 𝑆 = 𝑄 )
10 oprpiece1.11 ⊢ ( 𝑦 ∈ 𝐶 → 𝑃 = 𝑄 )
11 oprpiece1.12 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ 𝑆 )
12 1 rexri ⊢ 𝐴 ∈ ℝ*
13 2 rexri ⊢ 𝐵 ∈ ℝ*
14 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
15 12 13 3 14 mp3an ⊢ 𝐵 ∈ ( 𝐴 [,] 𝐵 )
16 iccss2 ⊢ ( ( 𝐾 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐾 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
17 6 15 16 mp2an ⊢ ( 𝐾 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
18 ssid ⊢ 𝐶 ⊆ 𝐶
19 resmpo ⊢ ( ( ( 𝐾 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ⊆ 𝐶 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) ↾ ( ( 𝐾 [,] 𝐵 ) × 𝐶 ) ) = ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) )
20 17 18 19 mp2an ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) ↾ ( ( 𝐾 [,] 𝐵 ) × 𝐶 ) ) = ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) )
21 7 reseq1i ⊢ ( 𝐹 ↾ ( ( 𝐾 [,] 𝐵 ) × 𝐶 ) ) = ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) ↾ ( ( 𝐾 [,] 𝐵 ) × 𝐶 ) )
22 10 ad2antlr ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑃 = 𝑄 )
23 simpr ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑥 ≤ 𝐾 )
24 1 2 elicc2i ⊢ ( 𝐾 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐾 ∈ ℝ ∧ 𝐴 ≤ 𝐾 ∧ 𝐾 ≤ 𝐵 ) )
25 24 simp1bi ⊢ ( 𝐾 ∈ ( 𝐴 [,] 𝐵 ) → 𝐾 ∈ ℝ )
26 6 25 ax-mp ⊢ 𝐾 ∈ ℝ
27 26 2 elicc2i ⊢ ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐾 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
28 27 simp2bi ⊢ ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) → 𝐾 ≤ 𝑥 )
29 28 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ≤ 𝐾 ) → 𝐾 ≤ 𝑥 )
30 27 simp1bi ⊢ ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) → 𝑥 ∈ ℝ )
31 30 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑥 ∈ ℝ )
32 letri3 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑥 = 𝐾 ↔ ( 𝑥 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) ) )
33 31 26 32 sylancl ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ≤ 𝐾 ) → ( 𝑥 = 𝐾 ↔ ( 𝑥 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) ) )
34 23 29 33 mpbir2and ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑥 = 𝐾 )
35 34 8 syl ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑅 = 𝑃 )
36 34 9 syl ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑆 = 𝑄 )
37 22 35 36 3eqtr4d ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑅 = 𝑆 )
38 eqidd ⊢ ( ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ ¬ 𝑥 ≤ 𝐾 ) → 𝑆 = 𝑆 )
39 37 38 ifeqda ⊢ ( ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) → if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) = 𝑆 )
40 39 mpoeq3ia ⊢ ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) = ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ 𝑆 )
41 11 40 eqtr4i ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐾 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) )
42 20 21 41 3eqtr4i ⊢ ( 𝐹 ↾ ( ( 𝐾 [,] 𝐵 ) × 𝐶 ) ) = 𝐺