Metamath Proof Explorer


Theorem pcoval1

Description: Evaluate the concatenation of two paths on the first half. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 7-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 pcoval.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
2 pcoval.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
3 0re 0 ∈ ℝ
4 1re 1 ∈ ℝ
5 0le0 0 ≤ 0
6 halfre ( 1 / 2 ) ∈ ℝ
7 halflt1 ( 1 / 2 ) < 1
8 6 4 7 ltleii ( 1 / 2 ) ≤ 1
9 iccss ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ 0 ∧ ( 1 / 2 ) ≤ 1 ) ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ( 0 [,] 1 ) )
10 3 4 5 8 9 mp4an ( 0 [,] ( 1 / 2 ) ) ⊆ ( 0 [,] 1 )
11 10 sseli ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) → 𝑋 ∈ ( 0 [,] 1 ) )
12 1 2 pcovalg ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
13 11 12 sylan2 ( ( 𝜑𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
14 elii1 ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) )
15 14 simprbi ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) → 𝑋 ≤ ( 1 / 2 ) )
16 15 iftrued ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) → if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = ( 𝐹 ‘ ( 2 · 𝑋 ) ) )
17 16 adantl ( ( 𝜑𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ) → if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = ( 𝐹 ‘ ( 2 · 𝑋 ) ) )
18 13 17 eqtrd ( ( 𝜑𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 2 · 𝑋 ) ) )