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 |
⊢ ( 𝜑 → 𝐸 = ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) ) |