Theorem pco0

Description: The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010)

	Ref	Expression
Hypotheses	pcoval.2	$$⊢\phi \to F\in \left(\mathrm{II}\mathrm{Cn}J\right)$$
	pcoval.3	$$⊢\phi \to G\in \left(\mathrm{II}\mathrm{Cn}J\right)$$
Assertion	pco0	$$⊢\phi \to \left(F{*}_{𝑝}\left(J\right)G\right)\left(0\right)=F\left(0\right)$$

Proof

Step	Hyp	Ref	Expression
1		pcoval.2	$$⊢\phi \to F\in \left(\mathrm{II}\mathrm{Cn}J\right)$$
2		pcoval.3	$$⊢\phi \to G\in \left(\mathrm{II}\mathrm{Cn}J\right)$$
3		0re	$$⊢0\in ℝ$$
4		0le0	$$⊢0\le 0$$
5		halfge0	$$⊢0\le \frac{1}{2}$$
6		halfre	$$⊢\frac{1}{2}\in ℝ$$
7	3 6	elicc2i	$$⊢0\in \left[0,\frac{1}{2}\right]\leftrightarrow \left(0\in ℝ\wedge 0\le 0\wedge 0\le \frac{1}{2}\right)$$
8	3 4 5 7	mpbir3an	$$⊢0\in \left[0,\frac{1}{2}\right]$$
9	1 2	pcoval1	$$⊢\left(\phi \wedge 0\in \left[0,\frac{1}{2}\right]\right)\to \left(F{*}_{𝑝}\left(J\right)G\right)\left(0\right)=F\left(2\cdot 0\right)$$
10	8 9	mpan2	$$⊢\phi \to \left(F{*}_{𝑝}\left(J\right)G\right)\left(0\right)=F\left(2\cdot 0\right)$$
11		2t0e0	$$⊢2\cdot 0=0$$
12	11	fveq2i	$$⊢F\left(2\cdot 0\right)=F\left(0\right)$$
13	10 12	syl6eq	$$⊢\phi \to \left(F{*}_{𝑝}\left(J\right)G\right)\left(0\right)=F\left(0\right)$$