Metamath Proof Explorer


Theorem pcovalg

Description: Evaluate the concatenation of two paths. (Contributed by Mario Carneiro, 7-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 pcoval.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
2 pcoval.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
3 1 2 pcoval ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
4 3 fveq1d ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ‘ 𝑋 ) )
5 breq1 ( 𝑥 = 𝑋 → ( 𝑥 ≤ ( 1 / 2 ) ↔ 𝑋 ≤ ( 1 / 2 ) ) )
6 oveq2 ( 𝑥 = 𝑋 → ( 2 · 𝑥 ) = ( 2 · 𝑋 ) )
7 6 fveq2d ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 2 · 𝑥 ) ) = ( 𝐹 ‘ ( 2 · 𝑋 ) ) )
8 6 fvoveq1d ( 𝑥 = 𝑋 → ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) )
9 5 7 8 ifbieq12d ( 𝑥 = 𝑋 → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
10 eqid ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
11 fvex ( 𝐹 ‘ ( 2 · 𝑋 ) ) ∈ V
12 fvex ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ∈ V
13 11 12 ifex if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) ∈ V
14 9 10 13 fvmpt ( 𝑋 ∈ ( 0 [,] 1 ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
15 4 14 sylan9eq ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )