View source for Homotopy invariance of path concatenation

{{Stub page|grade=A*|msg=Really not in the mood for this, done it anyway, check first and flesh out}}
__TOC__
==Statement==
[[File:HomotopyInvarianceOfPathConcatenation.JPG|thumb|{{XXX|This caption}}]]
Let {{M|p_1,p_2,p_1',p_2'\in}}{{C(I,X)}} be given. Suppose {{M|H_1:\ p_1\simeq p_1'\ (\text{rel }\{0,1\})}} and {{M|H_2:\ p_2\simeq p_2'\ (\text{rel }\{0,1\})}} are {{plural|end point preserving homotop|y|ies}} (where {{M|H_1,H_2:[0,1]\times [0,1]\rightarrow X}} are the specific {{plural|homotop|y|ies}} of the {{link|path|topology|s}}) then{{rITTMJML}}:
* {{M|H:p_1*p_2\simeq p_1'*p_2'\ (\text{rel }\{0,1\})}} where
** {{M|p_1*p_2}} denotes {{link|path concatenation|topology}}, explicitly:
*** {{M|1=p_1*p_2:[0,1]\rightarrow X}} by {{M|p_1*p_2:t\mapsto\left\{\begin{array}{lr}p_1(2t)&\text{for }t\in[0,\frac{1}{2}]\\p_2(2t-1)&\text{for }t\in[\frac{1}{2},1]\end{array}\right. }}
**** Note that the fact {{M|1=t=\frac{1}{2} }} is in both parts is a nod towards the use of the [[pasting lemma]]
** {{M|1=H:=H_1*H_2}} - the [[homotopy concatenation]], explicitly:
*** {{M|1=H:[0,1]\times[0,1]\rightarrow X}} by {{M|1=H:(s,t)\mapsto\left\{\begin{array}{lr}H_1(s,2t)&\text{for }t\in[0,\frac{1}{2}]\\ H_2(s,2t-1)&\text{for }t\in[\frac{1}{2},1]\end{array}\right.}} 
**** Note that the fact {{M|1=t=\frac{1}{2} }} is in both parts is a nod towards the use of the [[pasting lemma]]
<div style="clear:both;"><div>
==Proof==
{{Requires proof|grade=A*|msg=It's basically already done. All we have to show is that the homotopy concatenation, {{M|H}}, fits the requirements}}
==See also==
* [[The fundamental group]]
==References==
<references/>
{{Theorem Of|Topology|Algebraic Topology|Homotopy Theory}}