pcoval2

Description: Evaluate the concatenation of two paths on the second half. (Contributed by Jeff Madsen, 15-Jun-2010) (Proof shortened 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)$
	pcoval2.4	$⊢ φ \to F (1) = G (0)$
Assertion	pcoval2	$⊢ (φ \land X \in [\frac{1}{2}, 1]) \to (F *_{𝑝} (J) G) (X) = G (2 X - 1)$

Proof

Step	Hyp	Ref	Expression
1		pcoval.2	$⊢ φ \to F \in (II Cn J)$
2		pcoval.3	$⊢ φ \to G \in (II Cn J)$
3		pcoval2.4	$⊢ φ \to F (1) = G (0)$
4		0re	$⊢ 0 \in ℝ$
5		1re	$⊢ 1 \in ℝ$
6		halfge0	$⊢ 0 \leq \frac{1}{2}$
7		1le1	$⊢ 1 \leq 1$
8		iccss	$⊢ ((0 \in ℝ \land 1 \in ℝ) \land (0 \leq \frac{1}{2} \land 1 \leq 1)) \to [\frac{1}{2}, 1] \subseteq [0, 1]$
9	4 5 6 7 8	mp4an	$⊢ [\frac{1}{2}, 1] \subseteq [0, 1]$
10	9	sseli	$⊢ X \in [\frac{1}{2}, 1] \to X \in [0, 1]$
11	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))$
12	10 11	sylan2	$⊢ (φ \land X \in [\frac{1}{2}, 1]) \to (F *_{𝑝} (J) G) (X) = if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1))$
13	3	adantr	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to F (1) = G (0)$
14		simprr	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to X \leq \frac{1}{2}$
15		halfre	$⊢ \frac{1}{2} \in ℝ$
16	15 5	elicc2i	$⊢ X \in [\frac{1}{2}, 1] \leftrightarrow (X \in ℝ \land \frac{1}{2} \leq X \land X \leq 1)$
17	16	simp2bi	$⊢ X \in [\frac{1}{2}, 1] \to \frac{1}{2} \leq X$
18	17	ad2antrl	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to \frac{1}{2} \leq X$
19	16	simp1bi	$⊢ X \in [\frac{1}{2}, 1] \to X \in ℝ$
20	19	ad2antrl	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to X \in ℝ$
21		letri3	$⊢ (X \in ℝ \land \frac{1}{2} \in ℝ) \to (X = \frac{1}{2} \leftrightarrow (X \leq \frac{1}{2} \land \frac{1}{2} \leq X))$
22	20 15 21	sylancl	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to (X = \frac{1}{2} \leftrightarrow (X \leq \frac{1}{2} \land \frac{1}{2} \leq X))$
23	14 18 22	mpbir2and	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to X = \frac{1}{2}$
24	23	oveq2d	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to 2 X = 2 (\frac{1}{2})$
25		2thalfe1	$⊢ 2 (\frac{1}{2}) = 1$
26	24 25	eqtrdi	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to 2 X = 1$
27	26	fveq2d	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to F (2 X) = F (1)$
28	26	oveq1d	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to 2 X - 1 = 1 - 1$
29		1m1e0	$⊢ 1 - 1 = 0$
30	28 29	eqtrdi	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to 2 X - 1 = 0$
31	30	fveq2d	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to G (2 X - 1) = G (0)$
32	13 27 31	3eqtr4d	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to F (2 X) = G (2 X - 1)$
33	32	ifeq1d	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1)) = if (X \leq \frac{1}{2}, G (2 X - 1), G (2 X - 1))$
34		ifid	$⊢ if (X \leq \frac{1}{2}, G (2 X - 1), G (2 X - 1)) = G (2 X - 1)$
35	33 34	eqtrdi	$⊢ (φ \land (X \in [\frac{1}{2}, 1] \land X \leq \frac{1}{2})) \to if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1)) = G (2 X - 1)$
36	35	expr	$⊢ (φ \land X \in [\frac{1}{2}, 1]) \to (X \leq \frac{1}{2} \to if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1)) = G (2 X - 1))$
37		iffalse	$⊢ \neg X \leq \frac{1}{2} \to if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1)) = G (2 X - 1)$
38	36 37	pm2.61d1	$⊢ (φ \land X \in [\frac{1}{2}, 1]) \to if (X \leq \frac{1}{2}, F (2 X), G (2 X - 1)) = G (2 X - 1)$
39	12 38	eqtrd	$⊢ (φ \land X \in [\frac{1}{2}, 1]) \to (F *_{𝑝} (J) G) (X) = G (2 X - 1)$

Metamath Proof Explorer

Theorem pcoval2

Proof