Metamath Proof Explorer


Theorem xpsxmetlem

Description: Lemma for xpsxmet . (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses xpsds.t T = R × 𝑠 S
xpsds.x X = Base R
xpsds.y Y = Base S
xpsds.1 φ R V
xpsds.2 φ S W
xpsds.p P = dist T
xpsds.m M = dist R X × X
xpsds.n N = dist S Y × Y
xpsds.3 φ M ∞Met X
xpsds.4 φ N ∞Met Y
Assertion xpsxmetlem φ dist Scalar R 𝑠 R 1 𝑜 S ∞Met ran x X , y Y x 1 𝑜 y

Proof

Step Hyp Ref Expression
1 xpsds.t T = R × 𝑠 S
2 xpsds.x X = Base R
3 xpsds.y Y = Base S
4 xpsds.1 φ R V
5 xpsds.2 φ S W
6 xpsds.p P = dist T
7 xpsds.m M = dist R X × X
8 xpsds.n N = dist S Y × Y
9 xpsds.3 φ M ∞Met X
10 xpsds.4 φ N ∞Met Y
11 eqid Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k = Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
12 eqid Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k = Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
13 eqid Base R 1 𝑜 S k = Base R 1 𝑜 S k
14 eqid dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k
15 eqid dist Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k = dist Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
16 fvexd φ Scalar R V
17 2on 2 𝑜 On
18 17 a1i φ 2 𝑜 On
19 fvexd φ k 2 𝑜 R 1 𝑜 S k V
20 elpri k 1 𝑜 k = k = 1 𝑜
21 df2o3 2 𝑜 = 1 𝑜
22 20 21 eleq2s k 2 𝑜 k = k = 1 𝑜
23 9 adantr φ k = M ∞Met X
24 fveq2 k = R 1 𝑜 S k = R 1 𝑜 S
25 fvpr0o R V R 1 𝑜 S = R
26 4 25 syl φ R 1 𝑜 S = R
27 24 26 sylan9eqr φ k = R 1 𝑜 S k = R
28 27 fveq2d φ k = dist R 1 𝑜 S k = dist R
29 27 fveq2d φ k = Base R 1 𝑜 S k = Base R
30 29 2 eqtr4di φ k = Base R 1 𝑜 S k = X
31 30 sqxpeqd φ k = Base R 1 𝑜 S k × Base R 1 𝑜 S k = X × X
32 28 31 reseq12d φ k = dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = dist R X × X
33 32 7 eqtr4di φ k = dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = M
34 30 fveq2d φ k = ∞Met Base R 1 𝑜 S k = ∞Met X
35 23 33 34 3eltr4d φ k = dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k ∞Met Base R 1 𝑜 S k
36 10 adantr φ k = 1 𝑜 N ∞Met Y
37 fveq2 k = 1 𝑜 R 1 𝑜 S k = R 1 𝑜 S 1 𝑜
38 fvpr1o S W R 1 𝑜 S 1 𝑜 = S
39 5 38 syl φ R 1 𝑜 S 1 𝑜 = S
40 37 39 sylan9eqr φ k = 1 𝑜 R 1 𝑜 S k = S
41 40 fveq2d φ k = 1 𝑜 dist R 1 𝑜 S k = dist S
42 40 fveq2d φ k = 1 𝑜 Base R 1 𝑜 S k = Base S
43 42 3 eqtr4di φ k = 1 𝑜 Base R 1 𝑜 S k = Y
44 43 sqxpeqd φ k = 1 𝑜 Base R 1 𝑜 S k × Base R 1 𝑜 S k = Y × Y
45 41 44 reseq12d φ k = 1 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = dist S Y × Y
46 45 8 eqtr4di φ k = 1 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k = N
47 43 fveq2d φ k = 1 𝑜 ∞Met Base R 1 𝑜 S k = ∞Met Y
48 36 46 47 3eltr4d φ k = 1 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k ∞Met Base R 1 𝑜 S k
49 35 48 jaodan φ k = k = 1 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k ∞Met Base R 1 𝑜 S k
50 22 49 sylan2 φ k 2 𝑜 dist R 1 𝑜 S k Base R 1 𝑜 S k × Base R 1 𝑜 S k ∞Met Base R 1 𝑜 S k
51 11 12 13 14 15 16 18 19 50 prdsxmet φ dist Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k ∞Met Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
52 fnpr2o R V S W R 1 𝑜 S Fn 2 𝑜
53 4 5 52 syl2anc φ R 1 𝑜 S Fn 2 𝑜
54 dffn5 R 1 𝑜 S Fn 2 𝑜 R 1 𝑜 S = k 2 𝑜 R 1 𝑜 S k
55 53 54 sylib φ R 1 𝑜 S = k 2 𝑜 R 1 𝑜 S k
56 55 oveq2d φ Scalar R 𝑠 R 1 𝑜 S = Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
57 56 fveq2d φ dist Scalar R 𝑠 R 1 𝑜 S = dist Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
58 eqid x X , y Y x 1 𝑜 y = x X , y Y x 1 𝑜 y
59 eqid Scalar R = Scalar R
60 eqid Scalar R 𝑠 R 1 𝑜 S = Scalar R 𝑠 R 1 𝑜 S
61 1 2 3 4 5 58 59 60 xpsrnbas φ ran x X , y Y x 1 𝑜 y = Base Scalar R 𝑠 R 1 𝑜 S
62 56 fveq2d φ Base Scalar R 𝑠 R 1 𝑜 S = Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
63 61 62 eqtrd φ ran x X , y Y x 1 𝑜 y = Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
64 63 fveq2d φ ∞Met ran x X , y Y x 1 𝑜 y = ∞Met Base Scalar R 𝑠 k 2 𝑜 R 1 𝑜 S k
65 51 57 64 3eltr4d φ dist Scalar R 𝑠 R 1 𝑜 S ∞Met ran x X , y Y x 1 𝑜 y