Theorem cortrclrtrcl

Description: The reflexive-transitive closure is idempotent. (Contributed by RP, 13-Jun-2020)

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

Proof

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