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 𝐴 ∈ ℝ
oprpiece1.2 𝐵 ∈ ℝ
oprpiece1.3 𝐴𝐵
oprpiece1.4 𝑅 ∈ V
oprpiece1.5 𝑆 ∈ V
oprpiece1.6 𝐾 ∈ ( 𝐴 [,] 𝐵 )
oprpiece1.7 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝐶 ↦ if ( 𝑥𝐾 , 𝑅 , 𝑆 ) )
oprpiece1.8 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦𝐶𝑅 )
Assertion oprpiece1res1 ( 𝐹 ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = 𝐺

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.8 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦𝐶𝑅 )
9 1 rexri 𝐴 ∈ ℝ*
10 2 rexri 𝐵 ∈ ℝ*
11 lbicc2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
12 9 10 3 11 mp3an 𝐴 ∈ ( 𝐴 [,] 𝐵 )
13 iccss2 ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐾 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐾 ) ⊆ ( 𝐴 [,] 𝐵 ) )
14 12 6 13 mp2an ( 𝐴 [,] 𝐾 ) ⊆ ( 𝐴 [,] 𝐵 )
15 ssid 𝐶𝐶
16 resmpo ( ( ( 𝐴 [,] 𝐾 ) ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐶𝐶 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝐶 ↦ if ( 𝑥𝐾 , 𝑅 , 𝑆 ) ) ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦𝐶 ↦ if ( 𝑥𝐾 , 𝑅 , 𝑆 ) ) )
17 14 15 16 mp2an ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝐶 ↦ if ( 𝑥𝐾 , 𝑅 , 𝑆 ) ) ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦𝐶 ↦ if ( 𝑥𝐾 , 𝑅 , 𝑆 ) )
18 7 reseq1i ( 𝐹 ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝐶 ↦ if ( 𝑥𝐾 , 𝑅 , 𝑆 ) ) ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) )
19 eliccxr ( 𝐾 ∈ ( 𝐴 [,] 𝐵 ) → 𝐾 ∈ ℝ* )
20 6 19 ax-mp 𝐾 ∈ ℝ*
21 iccleub ( ( 𝐴 ∈ ℝ*𝐾 ∈ ℝ*𝑥 ∈ ( 𝐴 [,] 𝐾 ) ) → 𝑥𝐾 )
22 9 20 21 mp3an12 ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) → 𝑥𝐾 )
23 22 iftrued ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) → if ( 𝑥𝐾 , 𝑅 , 𝑆 ) = 𝑅 )
24 23 adantr ( ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) ∧ 𝑦𝐶 ) → if ( 𝑥𝐾 , 𝑅 , 𝑆 ) = 𝑅 )
25 24 mpoeq3ia ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦𝐶 ↦ if ( 𝑥𝐾 , 𝑅 , 𝑆 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦𝐶𝑅 )
26 8 25 eqtr4i 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦𝐶 ↦ if ( 𝑥𝐾 , 𝑅 , 𝑆 ) )
27 17 18 26 3eqtr4i ( 𝐹 ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = 𝐺