Metamath Proof Explorer

Theorem pcoval

Description: The concatenation of two paths. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses pcoval.2 ⊢φ→F∈IICnJ
pcoval.3 ⊢φ→G∈IICnJ
Assertion pcoval ⊢φ→F*𝑝⁡JG=x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢φ→F∈IICnJ
2 pcoval.3 ⊢φ→G∈IICnJ
3 fveq1 ⊢f=F→f⁡2⁢x=F⁡2⁢x
4 3 adantr ⊢f=F∧g=G→f⁡2⁢x=F⁡2⁢x
5 fveq1 ⊢g=G→g⁡2⁢x−1=G⁡2⁢x−1
6 5 adantl ⊢f=F∧g=G→g⁡2⁢x−1=G⁡2⁢x−1
7 4 6 ifeq12d ⊢f=F∧g=G→ifx≤12f⁡2⁢xg⁡2⁢x−1=ifx≤12F⁡2⁢xG⁡2⁢x−1
8 7 mpteq2dv ⊢f=F∧g=G→x∈01⟼ifx≤12f⁡2⁢xg⁡2⁢x−1=x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1
9 pcofval ⊢*𝑝⁡J=f∈IICnJ,g∈IICnJ⟼x∈01⟼ifx≤12f⁡2⁢xg⁡2⁢x−1
10 ovex ⊢01∈V
11 10 mptex ⊢x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1∈V
12 8 9 11 ovmpoa ⊢F∈IICnJ∧G∈IICnJ→F*𝑝⁡JG=x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1
13 1 2 12 syl2anc ⊢φ→F*𝑝⁡JG=x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1