Metamath Proof Explorer

Theorem pcoval2

Description: Evaluate the concatenation of two paths on the second half. (Contributed by Jeff Madsen, 15-Jun-2010) (Proof shortened by Mario Carneiro, 7-Jun-2014)

Ref Expression
Hypotheses pcoval.2 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
pcoval.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
pcoval2.4 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
Assertion pcoval2 ( ( 𝜑 ∧ 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) )

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
2 pcoval.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
3 pcoval2.4 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
4 0re ⊢ 0 ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 halfge0 ⊢ 0 ≤ ( 1 / 2 )
7 1le1 ⊢ 1 ≤ 1
8 iccss ⊢ ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ ( 1 / 2 ) ∧ 1 ≤ 1 ) ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ( 0 [,] 1 ) )
9 4 5 6 7 8 mp4an ⊢ ( ( 1 / 2 ) [,] 1 ) ⊆ ( 0 [,] 1 )
10 9 sseli ⊢ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) → 𝑋 ∈ ( 0 [,] 1 ) )
11 1 2 pcovalg ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
12 10 11 sylan2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
14 simprr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → 𝑋 ≤ ( 1 / 2 ) )
15 halfre ⊢ ( 1 / 2 ) ∈ ℝ
16 15 5 elicc2i ⊢ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ↔ ( 𝑋 ∈ ℝ ∧ ( 1 / 2 ) ≤ 𝑋 ∧ 𝑋 ≤ 1 ) )
17 16 simp2bi ⊢ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) → ( 1 / 2 ) ≤ 𝑋 )
18 17 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( 1 / 2 ) ≤ 𝑋 )
19 16 simp1bi ⊢ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) → 𝑋 ∈ ℝ )
20 19 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → 𝑋 ∈ ℝ )
21 letri3 ⊢ ( ( 𝑋 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝑋 = ( 1 / 2 ) ↔ ( 𝑋 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 𝑋 ) ) )
22 20 15 21 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( 𝑋 = ( 1 / 2 ) ↔ ( 𝑋 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 𝑋 ) ) )
23 14 18 22 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → 𝑋 = ( 1 / 2 ) )
24 23 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( 2 · 𝑋 ) = ( 2 · ( 1 / 2 ) ) )
25 2cn ⊢ 2 ∈ ℂ
26 2ne0 ⊢ 2 ≠ 0
27 25 26 recidi ⊢ ( 2 · ( 1 / 2 ) ) = 1
28 24 27 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( 2 · 𝑋 ) = 1 )
29 28 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( 𝐹 ‘ ( 2 · 𝑋 ) ) = ( 𝐹 ‘ 1 ) )
30 28 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( ( 2 · 𝑋 ) − 1 ) = ( 1 − 1 ) )
31 1m1e0 ⊢ ( 1 − 1 ) = 0
32 30 31 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( ( 2 · 𝑋 ) − 1 ) = 0 )
33 32 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) = ( 𝐺 ‘ 0 ) )
34 13 29 33 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → ( 𝐹 ‘ ( 2 · 𝑋 ) ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) )
35 34 ifeq1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
36 ifid ⊢ if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) )
37 35 36 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) → if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) )
38 37 expr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( 𝑋 ≤ ( 1 / 2 ) → if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
39 iffalse ⊢ ( ¬ 𝑋 ≤ ( 1 / 2 ) → if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) )
40 38 39 pm2.61d1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ) → if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) )
41 12 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) )