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	$⊢ φ \to F \in (II Cn J)$
		pcoval.3	$⊢ φ \to G \in (II Cn J)$
	Assertion	pcoval1	$⊢ (φ \land X \in [0, \frac{1}{2}]) \to (F *_{𝑝} (J) G) (X) = F (2 X)$

Proof

Step	Hyp	Ref	Expression
1		pcoval.2	$⊢ φ \to F \in (II Cn J)$
2		pcoval.3	$⊢ φ \to G \in (II Cn J)$
3		0re	$⊢ 0 \in ℝ$
4		1re	$⊢ 1 \in ℝ$
5		0le0	$⊢ 0 \leq 0$
6		halfre	$⊢ \frac{1}{2} \in ℝ$
7		halflt1	$⊢ \frac{1}{2} < 1$
8	6 4 7	ltleii	$⊢ \frac{1}{2} \leq 1$
9		iccss	$⊢ ((0 \in ℝ \land 1 \in ℝ) \land (0 \leq 0 \land \frac{1}{2} \leq 1)) \to [0, \frac{1}{2}] \subseteq [0, 1]$
10	3 4 5 8 9	mp4an	$⊢ [0, \frac{1}{2}] \subseteq [0, 1]$
11	10	sseli	$⊢ X \in [0, \frac{1}{2}] \to X \in [0, 1]$
12	1 2	pcovalg	$⊢ (φ \land X \in [0, 1]) \to (F *_{𝑝} (J) G) (X) = if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1))$
13	11 12	sylan2	$⊢ (φ \land X \in [0, \frac{1}{2}]) \to (F *_{𝑝} (J) G) (X) = if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1))$
14		elii1	$⊢ X \in [0, \frac{1}{2}] \leftrightarrow (X \in [0, 1] \land X \leq \frac{1}{2})$
15	14	simprbi	$⊢ X \in [0, \frac{1}{2}] \to X \leq \frac{1}{2}$
16	15	iftrued	$⊢ X \in [0, \frac{1}{2}] \to if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1)) = F (2 X)$
17	16	adantl	$⊢ (φ \land X \in [0, \frac{1}{2}]) \to if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1)) = F (2 X)$
18	13 17	eqtrd	$⊢ (φ \land X \in [0, \frac{1}{2}]) \to (F *_{𝑝} (J) G) (X) = F (2 X)$