Metamath Proof Explorer

Theorem cmspropd

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

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

Proof

Step Hyp Ref Expression
1 cmspropd.1 ⊢ φ → B = Base K
2 cmspropd.2 ⊢ φ → B = Base L
3 cmspropd.3 ⊢ φ → dist ⁡ K ↾ B × B = dist ⁡ L ↾ B × B
4 cmspropd.4 ⊢ φ → TopOpen ⁡ K = TopOpen ⁡ L
5 1 2 3 4 mspropd ⊢ φ → 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 ⊢ φ → CMet ⁡ Base K = CMet ⁡ Base L
14 11 13 eleq12d ⊢ φ → dist ⁡ K ↾ Base K × Base K ∈ CMet ⁡ Base K ↔ dist ⁡ L ↾ Base L × Base L ∈ CMet ⁡ Base L
15 5 14 anbi12d ⊢ φ → K ∈ MetSp ∧ dist ⁡ K ↾ Base K × Base K ∈ CMet ⁡ Base K ↔ L ∈ MetSp ∧ dist ⁡ L ↾ Base L × Base L ∈ CMet ⁡ Base L
16 eqid ⊢ Base K = Base K
17 eqid ⊢ dist ⁡ K ↾ Base K × Base K = dist ⁡ K ↾ Base K × Base K
18 16 17 iscms ⊢ K ∈ CMetSp ↔ K ∈ MetSp ∧ dist ⁡ K ↾ Base K × Base K ∈ CMet ⁡ Base K
19 eqid ⊢ Base L = Base L
20 eqid ⊢ dist ⁡ L ↾ Base L × Base L = dist ⁡ L ↾ Base L × Base L
21 19 20 iscms ⊢ L ∈ CMetSp ↔ L ∈ MetSp ∧ dist ⁡ L ↾ Base L × Base L ∈ CMet ⁡ Base L
22 15 18 21 3bitr4g ⊢ φ → K ∈ CMetSp ↔ L ∈ CMetSp