Metamath Proof Explorer


Theorem metreslem

Description: Lemma for metres . (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion metreslem
|- ( dom D = ( X X. X ) -> ( D |` ( R X. R ) ) = ( D |` ( ( X i^i R ) X. ( X i^i R ) ) ) )

Proof

Step Hyp Ref Expression
1 resdmres
 |-  ( D |` dom ( D |` ( R X. R ) ) ) = ( D |` ( R X. R ) )
2 ineq2
 |-  ( dom D = ( X X. X ) -> ( ( R X. R ) i^i dom D ) = ( ( R X. R ) i^i ( X X. X ) ) )
3 dmres
 |-  dom ( D |` ( R X. R ) ) = ( ( R X. R ) i^i dom D )
4 inxp
 |-  ( ( X X. X ) i^i ( R X. R ) ) = ( ( X i^i R ) X. ( X i^i R ) )
5 incom
 |-  ( ( X X. X ) i^i ( R X. R ) ) = ( ( R X. R ) i^i ( X X. X ) )
6 4 5 eqtr3i
 |-  ( ( X i^i R ) X. ( X i^i R ) ) = ( ( R X. R ) i^i ( X X. X ) )
7 2 3 6 3eqtr4g
 |-  ( dom D = ( X X. X ) -> dom ( D |` ( R X. R ) ) = ( ( X i^i R ) X. ( X i^i R ) ) )
8 7 reseq2d
 |-  ( dom D = ( X X. X ) -> ( D |` dom ( D |` ( R X. R ) ) ) = ( D |` ( ( X i^i R ) X. ( X i^i R ) ) ) )
9 1 8 eqtr3id
 |-  ( dom D = ( X X. X ) -> ( D |` ( R X. R ) ) = ( D |` ( ( X i^i R ) X. ( X i^i R ) ) ) )