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