Metamath Proof Explorer


Theorem cotrclrtrcl

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

Ref Expression
Assertion cotrclrtrcl ( t+ ∘ t* ) = t*

Proof

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