Theorem corclrtrcl

Description: Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020)

	Ref	Expression
Assertion	corclrtrcl	$$⊢\mathrm{r*}\circ \mathrm{t*}=\mathrm{t*}$$

Proof

Step	Hyp	Ref	Expression
1		corcltrcl	$$⊢\mathrm{r*}\circ \mathrm{t+}=\mathrm{t*}$$
2	1	eqcomi	$$⊢\mathrm{t*}=\mathrm{r*}\circ \mathrm{t+}$$
3	2	coeq2i	$$⊢\mathrm{r*}\circ \mathrm{t*}=\mathrm{r*}\circ \left(\mathrm{r*}\circ \mathrm{t+}\right)$$
4		coass	$$⊢\left(\mathrm{r*}\circ \mathrm{r*}\right)\circ \mathrm{t+}=\mathrm{r*}\circ \left(\mathrm{r*}\circ \mathrm{t+}\right)$$
5	4	eqcomi	$$⊢\mathrm{r*}\circ \left(\mathrm{r*}\circ \mathrm{t+}\right)=\left(\mathrm{r*}\circ \mathrm{r*}\right)\circ \mathrm{t+}$$
6		corclrcl	$$⊢\mathrm{r*}\circ \mathrm{r*}=\mathrm{r*}$$
7	6	coeq1i	$$⊢\left(\mathrm{r*}\circ \mathrm{r*}\right)\circ \mathrm{t+}=\mathrm{r*}\circ \mathrm{t+}$$
8	7 1	eqtri	$$⊢\left(\mathrm{r*}\circ \mathrm{r*}\right)\circ \mathrm{t+}=\mathrm{t*}$$
9	5 8	eqtri	$$⊢\mathrm{r*}\circ \left(\mathrm{r*}\circ \mathrm{t+}\right)=\mathrm{t*}$$
10	3 9	eqtri	$$⊢\mathrm{r*}\circ \mathrm{t*}=\mathrm{t*}$$