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 eqtrid ( 𝜑𝐵 = ( 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 eqtrid ( 𝜑𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑥𝐼𝑅 ) ) ) )
68 67 oveqdr ( ( 𝜑 ∧ ( 𝑓𝐵𝑔𝐵 ) ) → ( 𝑓 𝐷 𝑔 ) = ( 𝑓 ( dist ‘ ( 𝑆 Xs ( 𝑥𝐼𝑅 ) ) ) 𝑔 ) )
69 2 fveq2d ( 𝜑 → ( dist ‘ 𝐻 ) = ( dist ‘ ( 𝑇 Xs ( 𝑥𝐼 ↦ ( 𝑅s 𝐴 ) ) ) ) )
70 5 69 eqtrid ( 𝜑𝐸 = ( 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 ( 𝜑𝐸 = ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) )