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 ) ) ) )