Description: The reflexive-transitive closure is idempotent. (Contributed by RP, 13-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | cortrclrtrcl | ⊢ ( t* ∘ t* ) = t* |
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* |