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 · 𝑋 ) ) )