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 ⊢ φ → F ∈ II Cn J
pcoval.3 ⊢ φ → G ∈ II Cn J
Assertion pcoval1 ⊢ φ ∧ X ∈ 0 1 2 → F * 𝑝 ⁡ J G ⁡ X = F ⁡ 2 ⁢ X

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢ φ → F ∈ II Cn J
2 pcoval.3 ⊢ φ → G ∈ II Cn J
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 ⊢ X ∈ 0 1 2 → X ∈ 0 1
12 1 2 pcovalg ⊢ φ ∧ X ∈ 0 1 → F * 𝑝 ⁡ J G ⁡ X = if X ≤ 1 2 F ⁡ 2 ⁢ X G ⁡ 2 ⁢ X − 1
13 11 12 sylan2 ⊢ φ ∧ X ∈ 0 1 2 → F * 𝑝 ⁡ J G ⁡ X = if X ≤ 1 2 F ⁡ 2 ⁢ X G ⁡ 2 ⁢ X − 1
14 elii1 ⊢ X ∈ 0 1 2 ↔ X ∈ 0 1 ∧ X ≤ 1 2
15 14 simprbi ⊢ X ∈ 0 1 2 → X ≤ 1 2
16 15 iftrued ⊢ X ∈ 0 1 2 → if X ≤ 1 2 F ⁡ 2 ⁢ X G ⁡ 2 ⁢ X − 1 = F ⁡ 2 ⁢ X
17 16 adantl ⊢ φ ∧ X ∈ 0 1 2 → if X ≤ 1 2 F ⁡ 2 ⁢ X G ⁡ 2 ⁢ X − 1 = F ⁡ 2 ⁢ X
18 13 17 eqtrd ⊢ φ ∧ X ∈ 0 1 2 → F * 𝑝 ⁡ J G ⁡ X = F ⁡ 2 ⁢ X