Theorem pcorev

Description: Concatenation with the reverse path. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 20-Dec-2013)

	Ref	Expression
Hypotheses	pcorev.1	$$⊢G=\left(x\in \left[0,1\right]⟼F\left(1-x\right)\right)$$
	pcorev.2	$$⊢P=\left[0,1\right]\times \left\{F\left(1\right)\right\}$$
Assertion	pcorev	$$⊢F\in \left(\mathrm{II}\mathrm{Cn}J\right)\to \left(G{*}_{𝑝}\left(J\right)F\right){\simeq }_{\mathrm{ph}}\left(J\right)P$$

Proof

Step	Hyp	Ref	Expression
1		pcorev.1	$$⊢G=\left(x\in \left[0,1\right]⟼F\left(1-x\right)\right)$$
2		pcorev.2	$$⊢P=\left[0,1\right]\times \left\{F\left(1\right)\right\}$$
3		eqid	$$⊢\left(s\in \left[0,1\right],t\in \left[0,1\right]⟼F\left(if\left(s\le \frac{1}{2},1-\left(1-t\right)2s,1-\left(1-t\right)\left(1-\left(2s-1\right)\right)\right)\right)\right)=\left(s\in \left[0,1\right],t\in \left[0,1\right]⟼F\left(if\left(s\le \frac{1}{2},1-\left(1-t\right)2s,1-\left(1-t\right)\left(1-\left(2s-1\right)\right)\right)\right)\right)$$
4	1 2 3	pcorevlem	$$⊢F\in \left(\mathrm{II}\mathrm{Cn}J\right)\to \left(\left(s\in \left[0,1\right],t\in \left[0,1\right]⟼F\left(if\left(s\le \frac{1}{2},1-\left(1-t\right)2s,1-\left(1-t\right)\left(1-\left(2s-1\right)\right)\right)\right)\right)\in \left(\left(G{*}_{𝑝}\left(J\right)F\right)\mathrm{PHtpy}\left(J\right)P\right)\wedge \left(G{*}_{𝑝}\left(J\right)F\right){\simeq }_{\mathrm{ph}}\left(J\right)P\right)$$
5	4	simprd	$$⊢F\in \left(\mathrm{II}\mathrm{Cn}J\right)\to \left(G{*}_{𝑝}\left(J\right)F\right){\simeq }_{\mathrm{ph}}\left(J\right)P$$