Metamath Proof Explorer


Theorem corclrtrcl

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

Ref Expression
Assertion corclrtrcl r* t* = t*

Proof

Step Hyp Ref Expression
1 corcltrcl r* t+ = t*
2 1 eqcomi t* = r* t+
3 2 coeq2i r* t* = r* r* t+
4 coass r* r* t+ = r* r* t+
5 4 eqcomi r* r* t+ = r* r* t+
6 corclrcl r* r* = r*
7 6 coeq1i r* r* t+ = r* t+
8 7 1 eqtri r* r* t+ = t*
9 5 8 eqtri r* r* t+ = t*
10 3 9 eqtri r* t* = t*