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 ∈ II Cn J
pcoval.3 ⊢ φ → G ∈ II Cn J
Assertion pcoval ⊢ φ → F * 𝑝 ⁡ J G = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢ φ → F ∈ II Cn J
2 pcoval.3 ⊢ φ → G ∈ II Cn J
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 → if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1 = if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1
8 7 mpteq2dv ⊢ f = F ∧ g = G → x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1 = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1
9 pcofval ⊢ * 𝑝 ⁡ J = f ∈ II Cn J , g ∈ II Cn J ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
10 ovex ⊢ 0 1 ∈ V
11 10 mptex ⊢ x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 ∈ V
12 8 9 11 ovmpoa ⊢ F ∈ II Cn J ∧ G ∈ II Cn J → F * 𝑝 ⁡ J G = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1
13 1 2 12 syl2anc ⊢ φ → F * 𝑝 ⁡ J G = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1