Metamath Proof Explorer

Theorem ressprdsds

Description: Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypotheses ressprdsds.y ⊢ ( 𝜑 → 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) )
ressprdsds.h ⊢ ( 𝜑 → 𝐻 = ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) )
ressprdsds.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
ressprdsds.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
ressprdsds.e ⊢ 𝐸 = ( dist ‘ 𝐻 )
ressprdsds.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
ressprdsds.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
ressprdsds.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
ressprdsds.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑋 )
ressprdsds.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐴 ∈ 𝑍 )
Assertion ressprdsds ( 𝜑 → 𝐸 = ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ressprdsds.y ⊢ ( 𝜑 → 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) )
2 ressprdsds.h ⊢ ( 𝜑 → 𝐻 = ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) )
3 ressprdsds.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
4 ressprdsds.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
5 ressprdsds.e ⊢ 𝐸 = ( dist ‘ 𝐻 )
6 ressprdsds.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
7 ressprdsds.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
8 ressprdsds.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
9 ressprdsds.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑋 )
10 ressprdsds.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐴 ∈ 𝑍 )
11 ovres ⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑓 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑔 ) = ( 𝑓 𝐷 𝑔 ) )
12 11 adantl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑔 ) = ( 𝑓 𝐷 𝑔 ) )
13 eqid ⊢ ( 𝑅 ↾s 𝐴 ) = ( 𝑅 ↾s 𝐴 )
14 eqid ⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
15 13 14 ressds ⊢ ( 𝐴 ∈ 𝑍 → ( dist ‘ 𝑅 ) = ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) )
16 10 15 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( dist ‘ 𝑅 ) = ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) )
17 16 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) ( 𝑔 ‘ 𝑥 ) ) )
18 17 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
20 19 rneqd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
21 20 uneq1d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) = ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
22 21 supeq1d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
23 eqid ⊢ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
24 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) )
25 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑆 ∈ 𝑈 )
26 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑊 )
27 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
29 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
30 13 29 ressbasss ⊢ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝑅 )
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝑅 ) )
32 31 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝑅 ) )
33 ss2ixp ⊢ ( ∀ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝑅 ) → X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ⊆ X 𝑥 ∈ 𝐼 ( Base ‘ 𝑅 ) )
34 32 33 syl ⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ⊆ X 𝑥 ∈ 𝐼 ( Base ‘ 𝑅 ) )
35 eqid ⊢ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) = ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) )
36 eqid ⊢ ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) = ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) )
37 ovex ⊢ ( 𝑅 ↾s 𝐴 ) ∈ V
38 37 rgenw ⊢ ∀ 𝑥 ∈ 𝐼 ( 𝑅 ↾s 𝐴 ) ∈ V
39 38 a1i ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝑅 ↾s 𝐴 ) ∈ V )
40 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) = ( Base ‘ ( 𝑅 ↾s 𝐴 ) )
41 35 36 7 8 39 40 prdsbas3 ⊢ ( 𝜑 → ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
42 23 24 6 8 27 29 prdsbas3 ⊢ ( 𝜑 → ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ 𝑅 ) )
43 34 41 42 3sstr4d ⊢ ( 𝜑 → ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) ⊆ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) )
44 2 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐻 ) = ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) )
45 3 44 syl5eq ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) )
46 1 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) )
47 43 45 46 3sstr4d ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑌 ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐵 ⊆ ( Base ‘ 𝑌 ) )
49 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) )
50 48 49 sseqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐵 ⊆ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) )
51 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ 𝐵 )
52 50 51 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) )
53 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ 𝐵 )
54 50 53 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) )
55 eqid ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) )
56 23 24 25 26 28 52 54 14 55 prdsdsval2 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) 𝑔 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
57 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑇 ∈ 𝑉 )
58 38 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑅 ↾s 𝐴 ) ∈ V )
59 45 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) )
60 51 59 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) )
61 53 59 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) )
62 eqid ⊢ ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) = ( dist ‘ ( 𝑅 ↾s 𝐴 ) )
63 eqid ⊢ ( dist ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) = ( dist ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) )
64 35 36 57 26 58 60 61 62 63 prdsdsval2 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 ( dist ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) 𝑔 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ↾s 𝐴 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
65 22 56 64 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) 𝑔 ) = ( 𝑓 ( dist ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) 𝑔 ) )
66 1 fveq2d ⊢ ( 𝜑 → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) )
67 4 66 syl5eq ⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) )
68 67 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 𝐷 𝑔 ) = ( 𝑓 ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) 𝑔 ) )
69 2 fveq2d ⊢ ( 𝜑 → ( dist ‘ 𝐻 ) = ( dist ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) )
70 5 69 syl5eq ⊢ ( 𝜑 → 𝐸 = ( dist ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) )
71 70 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 𝐸 𝑔 ) = ( 𝑓 ( dist ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) 𝑔 ) )
72 65 68 71 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 𝐷 𝑔 ) = ( 𝑓 𝐸 𝑔 ) )
73 12 72 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 𝐸 𝑔 ) = ( 𝑓 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑔 ) )
74 73 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ( 𝑓 𝐸 𝑔 ) = ( 𝑓 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑔 ) )
75 8 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ∈ V )
76 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) )
77 37 76 dmmpti ⊢ dom ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) = 𝐼
78 77 a1i ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) = 𝐼 )
79 35 7 75 36 78 63 prdsdsfn ⊢ ( 𝜑 → ( dist ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) Fn ( ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) × ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) ) )
80 45 sqxpeqd ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) × ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) ) )
81 70 80 fneq12d ⊢ ( 𝜑 → ( 𝐸 Fn ( 𝐵 × 𝐵 ) ↔ ( dist ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) Fn ( ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) × ( Base ‘ ( 𝑇 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) ) ) ) )
82 79 81 mpbird ⊢ ( 𝜑 → 𝐸 Fn ( 𝐵 × 𝐵 ) )
83 8 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ∈ V )
84 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 → dom ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = 𝐼 )
85 27 84 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = 𝐼 )
86 23 6 83 24 85 55 prdsdsfn ⊢ ( 𝜑 → ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) Fn ( ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) × ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) ) )
87 46 sqxpeqd ⊢ ( 𝜑 → ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) = ( ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) × ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) ) )
88 67 87 fneq12d ⊢ ( 𝜑 → ( 𝐷 Fn ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↔ ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) Fn ( ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) × ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) ) ) ) )
89 86 88 mpbird ⊢ ( 𝜑 → 𝐷 Fn ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) )
90 xpss12 ⊢ ( ( 𝐵 ⊆ ( Base ‘ 𝑌 ) ∧ 𝐵 ⊆ ( Base ‘ 𝑌 ) ) → ( 𝐵 × 𝐵 ) ⊆ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) )
91 47 47 90 syl2anc ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ⊆ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) )
92 fnssres ⊢ ( ( 𝐷 Fn ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ∧ ( 𝐵 × 𝐵 ) ⊆ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) → ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
93 89 91 92 syl2anc ⊢ ( 𝜑 → ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
94 eqfnov2 ⊢ ( ( 𝐸 Fn ( 𝐵 × 𝐵 ) ∧ ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) ) → ( 𝐸 = ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) ↔ ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ( 𝑓 𝐸 𝑔 ) = ( 𝑓 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑔 ) ) )
95 82 93 94 syl2anc ⊢ ( 𝜑 → ( 𝐸 = ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) ↔ ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ( 𝑓 𝐸 𝑔 ) = ( 𝑓 ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) 𝑔 ) ) )
96 74 95 mpbird ⊢ ( 𝜑 → 𝐸 = ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) )