# Metamath Proof Explorer

## Theorem cortrcltrcl

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

Ref Expression
Assertion cortrcltrcl ${⊢}\mathrm{t*}\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 coeq1i ${⊢}\mathrm{t*}\circ \mathrm{t+}=\left(\mathrm{r*}\circ \mathrm{t+}\right)\circ \mathrm{t+}$
4 coass ${⊢}\left(\mathrm{r*}\circ \mathrm{t+}\right)\circ \mathrm{t+}=\mathrm{r*}\circ \left(\mathrm{t+}\circ \mathrm{t+}\right)$
5 cotrcltrcl ${⊢}\mathrm{t+}\circ \mathrm{t+}=\mathrm{t+}$
6 5 coeq2i ${⊢}\mathrm{r*}\circ \left(\mathrm{t+}\circ \mathrm{t+}\right)=\mathrm{r*}\circ \mathrm{t+}$
7 6 1 eqtri ${⊢}\mathrm{r*}\circ \left(\mathrm{t+}\circ \mathrm{t+}\right)=\mathrm{t*}$
8 4 7 eqtri ${⊢}\left(\mathrm{r*}\circ \mathrm{t+}\right)\circ \mathrm{t+}=\mathrm{t*}$
9 3 8 eqtri ${⊢}\mathrm{t*}\circ \mathrm{t+}=\mathrm{t*}$