Theorem cortrclrtrcl

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

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

Proof

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