Description: Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | cotrclrtrcl | ⊢ ( t+ ∘ t* ) = t* |
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* |