Metamath Proof Explorer

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]×\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]×\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)2{s},1-\left(1-{t}\right)\left(1-\left(2{s}-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)2{s},1-\left(1-{t}\right)\left(1-\left(2{s}-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)2{s},1-\left(1-{t}\right)\left(1-\left(2{s}-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}$