Metamath Proof Explorer

Theorem xmspropd

Description: Property deduction for an extended 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 xmspropd ⊢ φ → 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 eqtr3d ⊢ φ → Base K = Base L
6 5 4 tpspropd ⊢ φ → K ∈ TopSp ↔ L ∈ TopSp
7 1 sqxpeqd ⊢ φ → B × B = Base K × Base K
8 7 reseq2d ⊢ φ → dist ⁡ K ↾ B × B = dist ⁡ K ↾ Base K × Base K
9 3 8 eqtr3d ⊢ φ → dist ⁡ L ↾ B × B = dist ⁡ K ↾ Base K × Base K
10 2 sqxpeqd ⊢ φ → B × B = Base L × Base L
11 10 reseq2d ⊢ φ → dist ⁡ L ↾ B × B = dist ⁡ L ↾ Base L × Base L
12 9 11 eqtr3d ⊢ φ → dist ⁡ K ↾ Base K × Base K = dist ⁡ L ↾ Base L × Base L
13 12 fveq2d ⊢ φ → MetOpen ⁡ dist ⁡ K ↾ Base K × Base K = MetOpen ⁡ dist ⁡ L ↾ Base L × Base L
14 4 13 eqeq12d ⊢ φ → TopOpen ⁡ K = MetOpen ⁡ dist ⁡ K ↾ Base K × Base K ↔ TopOpen ⁡ L = MetOpen ⁡ dist ⁡ L ↾ Base L × Base L
15 6 14 anbi12d ⊢ φ → K ∈ TopSp ∧ TopOpen ⁡ K = MetOpen ⁡ dist ⁡ K ↾ Base K × Base K ↔ L ∈ TopSp ∧ TopOpen ⁡ L = MetOpen ⁡ dist ⁡ L ↾ Base L × 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 isxms ⊢ K ∈ ∞MetSp ↔ K ∈ TopSp ∧ TopOpen ⁡ K = MetOpen ⁡ dist ⁡ K ↾ Base K × 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 isxms ⊢ L ∈ ∞MetSp ↔ L ∈ TopSp ∧ TopOpen ⁡ L = MetOpen ⁡ dist ⁡ L ↾ Base L × Base L
24 15 19 23 3bitr4g ⊢ φ → K ∈ ∞MetSp ↔ L ∈ ∞MetSp