Metamath Proof Explorer

Theorem pco1

Description: The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010)

Ref Expression
Hypotheses pcoval.2 ⊢φ→F∈IICnJ
pcoval.3 ⊢φ→G∈IICnJ
Assertion pco1 ⊢φ→F*𝑝⁡JG⁡1=G⁡1

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢φ→F∈IICnJ
2 pcoval.3 ⊢φ→G∈IICnJ
3 1 2 pcoval ⊢φ→F*𝑝⁡JG=x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1
4 3 fveq1d ⊢φ→F*𝑝⁡JG⁡1=x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1⁡1
5 1elunit ⊢1∈01
6 halflt1 ⊢12<1
7 halfre ⊢12∈ℝ
8 1re ⊢1∈ℝ
9 7 8 ltnlei ⊢12<1↔¬1≤12
10 6 9 mpbi ⊢¬1≤12
11 breq1 ⊢x=1→x≤12↔1≤12
12 10 11 mtbiri ⊢x=1→¬x≤12
13 12 iffalsed ⊢x=1→ifx≤12F⁡2⁢xG⁡2⁢x−1=G⁡2⁢x−1
14 oveq2 ⊢x=1→2⁢x=2⋅1
15 2t1e2 ⊢2⋅1=2
16 14 15 eqtrdi ⊢x=1→2⁢x=2
17 16 oveq1d ⊢x=1→2⁢x−1=2−1
18 2m1e1 ⊢2−1=1
19 17 18 eqtrdi ⊢x=1→2⁢x−1=1
20 19 fveq2d ⊢x=1→G⁡2⁢x−1=G⁡1
21 13 20 eqtrd ⊢x=1→ifx≤12F⁡2⁢xG⁡2⁢x−1=G⁡1
22 eqid ⊢x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1=x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1
23 fvex ⊢G⁡1∈V
24 21 22 23 fvmpt ⊢1∈01→x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1⁡1=G⁡1
25 5 24 ax-mp ⊢x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1⁡1=G⁡1
26 4 25 eqtrdi ⊢φ→F*𝑝⁡JG⁡1=G⁡1