Theorem cortrclrcl

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

	Ref	Expression
Assertion	cortrclrcl	|- ( t* o. r* ) = t*

Proof

Step	Hyp	Ref	Expression
1		cotrclrcl	|- ( t+ o. r* ) = t*
2	1	eqcomi	|- t* = ( t+ o. r* )
3	2	coeq1i	|- ( t* o. r* ) = ( ( t+ o. r* ) o. r* )
4		coass	|- ( ( t+ o. r* ) o. r* ) = ( t+ o. ( r* o. r* ) )
5		corclrcl	|- ( r* o. r* ) = r*
6	5	coeq2i	|- ( t+ o. ( r* o. r* ) ) = ( t+ o. r* )
7	6 1	eqtri	|- ( t+ o. ( r* o. r* ) ) = t*
8	4 7	eqtri	|- ( ( t+ o. r* ) o. r* ) = t*
9	3 8	eqtri	|- ( t* o. r* ) = t*