Theorem cortrcltrcl

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

	Ref	Expression
Assertion	cortrcltrcl	|- ( t* o. t+ ) = t*

Proof

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