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*