Metamath Proof Explorer


Theorem cortrclrtrcl

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

Ref Expression
Assertion cortrclrtrcl ( t* ∘ t* ) = t*

Proof

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