Metamath Proof Explorer

Theorem mspropd

Description: Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses xmspropd.1 ⊢ φ → B = Base K
xmspropd.2 ⊢ φ → B = Base L
xmspropd.3 ⊢ φ → dist ⁡ K ↾ B × B = dist ⁡ L ↾ B × B
xmspropd.4 ⊢ φ → TopOpen ⁡ K = TopOpen ⁡ L
Assertion mspropd ⊢ φ → K ∈ MetSp ↔ L ∈ MetSp

Proof

Step Hyp Ref Expression
1 xmspropd.1 ⊢ φ → B = Base K
2 xmspropd.2 ⊢ φ → B = Base L
3 xmspropd.3 ⊢ φ → dist ⁡ K ↾ B × B = dist ⁡ L ↾ B × B
4 xmspropd.4 ⊢ φ → TopOpen ⁡ K = TopOpen ⁡ L
5 1 2 3 4 xmspropd ⊢ φ → K ∈ ∞MetSp ↔ L ∈ ∞MetSp
6 1 sqxpeqd ⊢ φ → B × B = Base K × Base K
7 6 reseq2d ⊢ φ → dist ⁡ K ↾ B × B = dist ⁡ K ↾ Base K × Base K
8 3 7 eqtr3d ⊢ φ → dist ⁡ L ↾ B × B = dist ⁡ K ↾ Base K × Base K
9 2 sqxpeqd ⊢ φ → B × B = Base L × Base L
10 9 reseq2d ⊢ φ → dist ⁡ L ↾ B × B = dist ⁡ L ↾ Base L × Base L
11 8 10 eqtr3d ⊢ φ → dist ⁡ K ↾ Base K × Base K = dist ⁡ L ↾ Base L × Base L
12 1 2 eqtr3d ⊢ φ → Base K = Base L
13 12 fveq2d ⊢ φ → Met ⁡ Base K = Met ⁡ Base L
14 11 13 eleq12d ⊢ φ → dist ⁡ K ↾ Base K × Base K ∈ Met ⁡ Base K ↔ dist ⁡ L ↾ Base L × Base L ∈ Met ⁡ Base L
15 5 14 anbi12d ⊢ φ → K ∈ ∞MetSp ∧ dist ⁡ K ↾ Base K × Base K ∈ Met ⁡ Base K ↔ L ∈ ∞MetSp ∧ dist ⁡ L ↾ Base L × Base L ∈ Met ⁡ Base L
16 eqid ⊢ TopOpen ⁡ K = TopOpen ⁡ K
17 eqid ⊢ Base K = Base K
18 eqid ⊢ dist ⁡ K ↾ Base K × Base K = dist ⁡ K ↾ Base K × Base K
19 16 17 18 isms ⊢ K ∈ MetSp ↔ K ∈ ∞MetSp ∧ dist ⁡ K ↾ Base K × Base K ∈ Met ⁡ Base K
20 eqid ⊢ TopOpen ⁡ L = TopOpen ⁡ L
21 eqid ⊢ Base L = Base L
22 eqid ⊢ dist ⁡ L ↾ Base L × Base L = dist ⁡ L ↾ Base L × Base L
23 20 21 22 isms ⊢ L ∈ MetSp ↔ L ∈ ∞MetSp ∧ dist ⁡ L ↾ Base L × Base L ∈ Met ⁡ Base L
24 15 19 23 3bitr4g ⊢ φ → K ∈ MetSp ↔ L ∈ MetSp