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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
cmspropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
cmspropd.3 ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) )
cmspropd.4 ⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐿 ) )
Assertion cmspropd ( 𝜑 → ( 𝐾 ∈ CMetSp ↔ 𝐿 ∈ CMetSp ) )

Proof

Step Hyp Ref Expression
1 cmspropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 cmspropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 cmspropd.3 ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) )
4 cmspropd.4 ⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐿 ) )
5 1 2 3 4 mspropd ⊢ ( 𝜑 → ( 𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp ) )
6 1 sqxpeqd ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
7 6 reseq2d ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
8 3 7 eqtr3d ⊢ ( 𝜑 → ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
9 2 sqxpeqd ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) )
10 9 reseq2d ⊢ ( 𝜑 → ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) )
11 8 10 eqtr3d ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) )
12 1 2 eqtr3d ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
13 12 fveq2d ⊢ ( 𝜑 → ( CMet ‘ ( Base ‘ 𝐾 ) ) = ( CMet ‘ ( Base ‘ 𝐿 ) ) )
14 11 13 eleq12d ⊢ ( 𝜑 → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ↔ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐿 ) ) ) )
15 5 14 anbi12d ⊢ ( 𝜑 → ( ( 𝐾 ∈ MetSp ∧ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ) ↔ ( 𝐿 ∈ MetSp ∧ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐿 ) ) ) ) )
16 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 eqid ⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
18 16 17 iscms ⊢ ( 𝐾 ∈ CMetSp ↔ ( 𝐾 ∈ MetSp ∧ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ) )
19 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
20 eqid ⊢ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) )
21 19 20 iscms ⊢ ( 𝐿 ∈ CMetSp ↔ ( 𝐿 ∈ MetSp ∧ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐿 ) ) ) )
22 15 18 21 3bitr4g ⊢ ( 𝜑 → ( 𝐾 ∈ CMetSp ↔ 𝐿 ∈ CMetSp ) )