Metamath Proof Explorer


Theorem resspwsds

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

Ref Expression
Hypotheses resspwsds.y φ Y = R 𝑠 I
resspwsds.h φ H = R 𝑠 A 𝑠 I
resspwsds.b B = Base H
resspwsds.d D = dist Y
resspwsds.e E = dist H
resspwsds.i φ I V
resspwsds.r φ R W
resspwsds.a φ A X
Assertion resspwsds φ E = D B × B

Proof

Step Hyp Ref Expression
1 resspwsds.y φ Y = R 𝑠 I
2 resspwsds.h φ H = R 𝑠 A 𝑠 I
3 resspwsds.b B = Base H
4 resspwsds.d D = dist Y
5 resspwsds.e E = dist H
6 resspwsds.i φ I V
7 resspwsds.r φ R W
8 resspwsds.a φ A X
9 eqid R 𝑠 I = R 𝑠 I
10 eqid Scalar R = Scalar R
11 9 10 pwsval R W I V R 𝑠 I = Scalar R 𝑠 I × R
12 7 6 11 syl2anc φ R 𝑠 I = Scalar R 𝑠 I × R
13 fconstmpt I × R = x I R
14 13 oveq2i Scalar R 𝑠 I × R = Scalar R 𝑠 x I R
15 12 14 eqtrdi φ R 𝑠 I = Scalar R 𝑠 x I R
16 1 15 eqtrd φ Y = Scalar R 𝑠 x I R
17 ovex R 𝑠 A V
18 eqid R 𝑠 A 𝑠 I = R 𝑠 A 𝑠 I
19 eqid Scalar R 𝑠 A = Scalar R 𝑠 A
20 18 19 pwsval R 𝑠 A V I V R 𝑠 A 𝑠 I = Scalar R 𝑠 A 𝑠 I × R 𝑠 A
21 17 6 20 sylancr φ R 𝑠 A 𝑠 I = Scalar R 𝑠 A 𝑠 I × R 𝑠 A
22 fconstmpt I × R 𝑠 A = x I R 𝑠 A
23 22 oveq2i Scalar R 𝑠 A 𝑠 I × R 𝑠 A = Scalar R 𝑠 A 𝑠 x I R 𝑠 A
24 21 23 eqtrdi φ R 𝑠 A 𝑠 I = Scalar R 𝑠 A 𝑠 x I R 𝑠 A
25 2 24 eqtrd φ H = Scalar R 𝑠 A 𝑠 x I R 𝑠 A
26 fvexd φ Scalar R V
27 fvexd φ Scalar R 𝑠 A V
28 7 adantr φ x I R W
29 8 adantr φ x I A X
30 16 25 3 4 5 26 27 6 28 29 ressprdsds φ E = D B × B