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 |
⊢ ( 𝐹 ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = 𝐺 |