Theorem metreslem

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

	Ref	Expression
Assertion	metreslem	⊢ ( dom 𝐷 = ( 𝑋 × 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) = ( 𝐷 ↾ ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		resdmres	⊢ ( 𝐷 ↾ dom ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ) = ( 𝐷 ↾ ( 𝑅 × 𝑅 ) )
2		ineq2	⊢ ( dom 𝐷 = ( 𝑋 × 𝑋 ) → ( ( 𝑅 × 𝑅 ) ∩ dom 𝐷 ) = ( ( 𝑅 × 𝑅 ) ∩ ( 𝑋 × 𝑋 ) ) )
3		dmres	⊢ dom ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) = ( ( 𝑅 × 𝑅 ) ∩ dom 𝐷 )
4		inxp	⊢ ( ( 𝑋 × 𝑋 ) ∩ ( 𝑅 × 𝑅 ) ) = ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) )
5		incom	⊢ ( ( 𝑋 × 𝑋 ) ∩ ( 𝑅 × 𝑅 ) ) = ( ( 𝑅 × 𝑅 ) ∩ ( 𝑋 × 𝑋 ) )
6	4 5	eqtr3i	⊢ ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) ) = ( ( 𝑅 × 𝑅 ) ∩ ( 𝑋 × 𝑋 ) )
7	2 3 6	3eqtr4g	⊢ ( dom 𝐷 = ( 𝑋 × 𝑋 ) → dom ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) = ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) ) )
8	7	reseq2d	⊢ ( dom 𝐷 = ( 𝑋 × 𝑋 ) → ( 𝐷 ↾ dom ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) ) = ( 𝐷 ↾ ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) ) ) )
9	1 8	eqtr3id	⊢ ( dom 𝐷 = ( 𝑋 × 𝑋 ) → ( 𝐷 ↾ ( 𝑅 × 𝑅 ) ) = ( 𝐷 ↾ ( ( 𝑋 ∩ 𝑅 ) × ( 𝑋 ∩ 𝑅 ) ) ) )