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 ⊢φ→F∈IICnJ
pcoval.3 ⊢φ→G∈IICnJ
pcoval2.4 ⊢φ→F⁡1=G⁡0
Assertion pcoval2 ⊢φ∧X∈121→F*𝑝⁡JG⁡X=G⁡2⁢X−1

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢φ→F∈IICnJ
2 pcoval.3 ⊢φ→G∈IICnJ
3 pcoval2.4 ⊢φ→F⁡1=G⁡0
4 0re ⊢0∈ℝ
5 1re ⊢1∈ℝ
6 halfge0 ⊢0≤12
7 1le1 ⊢1≤1
8 iccss ⊢0∈ℝ∧1∈ℝ∧0≤12∧1≤1→121⊆01
9 4 5 6 7 8 mp4an ⊢121⊆01
10 9 sseli ⊢X∈121→X∈01
11 1 2 pcovalg ⊢φ∧X∈01→F*𝑝⁡JG⁡X=ifX≤12F⁡2⁢XG⁡2⁢X−1
12 10 11 sylan2 ⊢φ∧X∈121→F*𝑝⁡JG⁡X=ifX≤12F⁡2⁢XG⁡2⁢X−1
13 3 adantr ⊢φ∧X∈121∧X≤12→F⁡1=G⁡0
14 simprr ⊢φ∧X∈121∧X≤12→X≤12
15 halfre ⊢12∈ℝ
16 15 5 elicc2i ⊢X∈121↔X∈ℝ∧12≤X∧X≤1
17 16 simp2bi ⊢X∈121→12≤X
18 17 ad2antrl ⊢φ∧X∈121∧X≤12→12≤X
19 16 simp1bi ⊢X∈121→X∈ℝ
20 19 ad2antrl ⊢φ∧X∈121∧X≤12→X∈ℝ
21 letri3 ⊢X∈ℝ∧12∈ℝ→X=12↔X≤12∧12≤X
22 20 15 21 sylancl ⊢φ∧X∈121∧X≤12→X=12↔X≤12∧12≤X
23 14 18 22 mpbir2and ⊢φ∧X∈121∧X≤12→X=12
24 23 oveq2d ⊢φ∧X∈121∧X≤12→2⁢X=2⁢12
25 2cn ⊢2∈ℂ
26 2ne0 ⊢2≠0
27 25 26 recidi ⊢2⁢12=1
28 24 27 eqtrdi ⊢φ∧X∈121∧X≤12→2⁢X=1
29 28 fveq2d ⊢φ∧X∈121∧X≤12→F⁡2⁢X=F⁡1
30 28 oveq1d ⊢φ∧X∈121∧X≤12→2⁢X−1=1−1
31 1m1e0 ⊢1−1=0
32 30 31 eqtrdi ⊢φ∧X∈121∧X≤12→2⁢X−1=0
33 32 fveq2d ⊢φ∧X∈121∧X≤12→G⁡2⁢X−1=G⁡0
34 13 29 33 3eqtr4d ⊢φ∧X∈121∧X≤12→F⁡2⁢X=G⁡2⁢X−1
35 34 ifeq1d ⊢φ∧X∈121∧X≤12→ifX≤12F⁡2⁢XG⁡2⁢X−1=ifX≤12G⁡2⁢X−1G⁡2⁢X−1
36 ifid ⊢ifX≤12G⁡2⁢X−1G⁡2⁢X−1=G⁡2⁢X−1
37 35 36 eqtrdi ⊢φ∧X∈121∧X≤12→ifX≤12F⁡2⁢XG⁡2⁢X−1=G⁡2⁢X−1
38 37 expr ⊢φ∧X∈121→X≤12→ifX≤12F⁡2⁢XG⁡2⁢X−1=G⁡2⁢X−1
39 iffalse ⊢¬X≤12→ifX≤12F⁡2⁢XG⁡2⁢X−1=G⁡2⁢X−1
40 38 39 pm2.61d1 ⊢φ∧X∈121→ifX≤12F⁡2⁢XG⁡2⁢X−1=G⁡2⁢X−1
41 12 40 eqtrd ⊢φ∧X∈121→F*𝑝⁡JG⁡X=G⁡2⁢X−1