Theorem cortrclrcl

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

	Ref	Expression
Assertion	cortrclrcl	⊢ ( t* ∘ r* ) = t*

Proof

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