Metamath Proof Explorer

Theorem ismtyres

Description: A restriction of an isometry is an isometry. The condition A C_ X is not necessary but makes the proof easier. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypotheses ismtyres.2 ⊢ 𝐵 = ( 𝐹 “ 𝐴 )
ismtyres.3 ⊢ 𝑆 = ( 𝑀 ↾ ( 𝐴 × 𝐴 ) )
ismtyres.4 ⊢ 𝑇 = ( 𝑁 ↾ ( 𝐵 × 𝐵 ) )
Assertion ismtyres ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → ( 𝐹 ↾ 𝐴 ) ∈ ( 𝑆 Ismty 𝑇 ) )

Proof

Step Hyp Ref Expression
1 ismtyres.2 ⊢ 𝐵 = ( 𝐹 “ 𝐴 )
2 ismtyres.3 ⊢ 𝑆 = ( 𝑀 ↾ ( 𝐴 × 𝐴 ) )
3 ismtyres.4 ⊢ 𝑇 = ( 𝑁 ↾ ( 𝐵 × 𝐵 ) )
4 isismty ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )
5 4 simprbda ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
6 5 adantrr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
7 f1of1 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –1-1→ 𝑌 )
8 6 7 syl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
9 simprr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → 𝐴 ⊆ 𝑋 )
10 f1ores ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) )
11 8 9 10 syl2anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) )
12 4 biimpa ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
13 12 adantrr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
14 ssel ⊢ ( 𝐴 ⊆ 𝑋 → ( 𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑋 ) )
15 ssel ⊢ ( 𝐴 ⊆ 𝑋 → ( 𝑣 ∈ 𝐴 → 𝑣 ∈ 𝑋 ) )
16 14 15 anim12d ⊢ ( 𝐴 ⊆ 𝑋 → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) )
17 16 imp ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) )
18 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 𝑀 𝑦 ) = ( 𝑢 𝑀 𝑦 ) )
19 fveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑢 ) )
20 19 oveq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) )
21 18 20 eqeq12d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑢 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
22 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝑢 𝑀 𝑦 ) = ( 𝑢 𝑀 𝑣 ) )
23 fveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑣 ) )
24 23 oveq2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
25 22 24 eqeq12d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑢 𝑀 𝑣 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) ) )
26 21 25 rspc2v ⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑢 𝑀 𝑣 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) ) )
27 17 26 syl ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑢 𝑀 𝑣 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) ) )
28 27 imp ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑢 𝑀 𝑣 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
29 28 an32s ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑢 𝑀 𝑣 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
30 29 adantlrl ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑢 𝑀 𝑣 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
31 30 adantlll ⊢ ( ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑢 𝑀 𝑣 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
32 2 oveqi ⊢ ( 𝑢 𝑆 𝑣 ) = ( 𝑢 ( 𝑀 ↾ ( 𝐴 × 𝐴 ) ) 𝑣 )
33 ovres ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑢 ( 𝑀 ↾ ( 𝐴 × 𝐴 ) ) 𝑣 ) = ( 𝑢 𝑀 𝑣 ) )
34 32 33 syl5eq ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑢 𝑆 𝑣 ) = ( 𝑢 𝑀 𝑣 ) )
35 34 adantl ⊢ ( ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑢 𝑆 𝑣 ) = ( 𝑢 𝑀 𝑣 ) )
36 fvres ⊢ ( 𝑢 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) )
37 36 ad2antrl ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) )
38 fvres ⊢ ( 𝑣 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) = ( 𝐹 ‘ 𝑣 ) )
39 38 ad2antll ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) = ( 𝐹 ‘ 𝑣 ) )
40 37 39 oveq12d ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑇 ( 𝐹 ‘ 𝑣 ) ) )
41 3 oveqi ⊢ ( ( 𝐹 ‘ 𝑢 ) 𝑇 ( 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ( 𝑁 ↾ ( 𝐵 × 𝐵 ) ) ( 𝐹 ‘ 𝑣 ) )
42 f1ofun ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → Fun 𝐹 )
43 42 adantl ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → Fun 𝐹 )
44 f1odm ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → dom 𝐹 = 𝑋 )
45 44 sseq2d ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ( 𝐴 ⊆ dom 𝐹 ↔ 𝐴 ⊆ 𝑋 ) )
46 45 biimparc ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → 𝐴 ⊆ dom 𝐹 )
47 funfvima2 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑢 ∈ 𝐴 → ( 𝐹 ‘ 𝑢 ) ∈ ( 𝐹 “ 𝐴 ) ) )
48 43 46 47 syl2anc ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑢 ∈ 𝐴 → ( 𝐹 ‘ 𝑢 ) ∈ ( 𝐹 “ 𝐴 ) ) )
49 48 imp ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑢 ) ∈ ( 𝐹 “ 𝐴 ) )
50 49 1 eleqtrrdi ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑢 ) ∈ 𝐵 )
51 50 adantrr ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ 𝐵 )
52 funfvima2 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑣 ∈ 𝐴 → ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 “ 𝐴 ) ) )
53 43 46 52 syl2anc ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑣 ∈ 𝐴 → ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 “ 𝐴 ) ) )
54 53 imp ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 “ 𝐴 ) )
55 54 1 eleqtrrdi ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝐵 )
56 55 adantrl ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝐵 )
57 51 56 ovresd ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑢 ) ( 𝑁 ↾ ( 𝐵 × 𝐵 ) ) ( 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
58 41 57 syl5eq ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑢 ) 𝑇 ( 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
59 40 58 eqtrd ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
60 59 adantlrr ⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
61 60 adantlll ⊢ ( ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑁 ( 𝐹 ‘ 𝑣 ) ) )
62 31 35 61 3eqtr4d ⊢ ( ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑢 𝑆 𝑣 ) = ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) )
63 62 ralrimivva ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 𝑆 𝑣 ) = ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) )
64 63 adantlrl ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 𝑆 𝑣 ) = ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) )
65 13 64 mpdan ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 𝑆 𝑣 ) = ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) )
66 xmetres2 ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑀 ↾ ( 𝐴 × 𝐴 ) ) ∈ ( ∞Met ‘ 𝐴 ) )
67 2 66 eqeltrid ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝑆 ∈ ( ∞Met ‘ 𝐴 ) )
68 67 ad2ant2rl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → 𝑆 ∈ ( ∞Met ‘ 𝐴 ) )
69 simplr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
70 imassrn ⊢ ( 𝐹 “ 𝐴 ) ⊆ ran 𝐹
71 1 70 eqsstri ⊢ 𝐵 ⊆ ran 𝐹
72 f1ofo ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –onto→ 𝑌 )
73 forn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ran 𝐹 = 𝑌 )
74 6 72 73 3syl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → ran 𝐹 = 𝑌 )
75 71 74 sseqtrid ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → 𝐵 ⊆ 𝑌 )
76 xmetres2 ⊢ ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐵 ⊆ 𝑌 ) → ( 𝑁 ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) )
77 69 75 76 syl2anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → ( 𝑁 ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) )
78 3 77 eqeltrid ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → 𝑇 ∈ ( ∞Met ‘ 𝐵 ) )
79 1 fveq2i ⊢ ( ∞Met ‘ 𝐵 ) = ( ∞Met ‘ ( 𝐹 “ 𝐴 ) )
80 78 79 eleqtrdi ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → 𝑇 ∈ ( ∞Met ‘ ( 𝐹 “ 𝐴 ) ) )
81 isismty ⊢ ( ( 𝑆 ∈ ( ∞Met ‘ 𝐴 ) ∧ 𝑇 ∈ ( ∞Met ‘ ( 𝐹 “ 𝐴 ) ) ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( 𝑆 Ismty 𝑇 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 𝑆 𝑣 ) = ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) ) ) )
82 68 80 81 syl2anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( 𝑆 Ismty 𝑇 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 𝑆 𝑣 ) = ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑢 ) 𝑇 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑣 ) ) ) ) )
83 11 65 82 mpbir2and ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ∧ 𝐴 ⊆ 𝑋 ) ) → ( 𝐹 ↾ 𝐴 ) ∈ ( 𝑆 Ismty 𝑇 ) )