This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 xmspropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 xmspropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 xmspropd.3 ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) )
4 xmspropd.4 ⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐿 ) )
5 1 2 eqtr3d ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
6 5 4 tpspropd ⊢ ( 𝜑 → ( 𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp ) )
7 1 sqxpeqd ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
8 7 reseq2d ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
9 3 8 eqtr3d ⊢ ( 𝜑 → ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
10 2 sqxpeqd ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) )
11 10 reseq2d ⊢ ( 𝜑 → ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) )
12 9 11 eqtr3d ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) )
13 12 fveq2d ⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) )
14 4 13 eqeq12d ⊢ ( 𝜑 → ( ( TopOpen ‘ 𝐾 ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ↔ ( TopOpen ‘ 𝐿 ) = ( MetOpen ‘ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) )
15 6 14 anbi12d ⊢ ( 𝜑 → ( ( 𝐾 ∈ TopSp ∧ ( TopOpen ‘ 𝐾 ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ) ↔ ( 𝐿 ∈ TopSp ∧ ( TopOpen ‘ 𝐿 ) = ( MetOpen ‘ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) ) )
16 eqid ⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
17 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
18 eqid ⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
19 16 17 18 isxms ⊢ ( 𝐾 ∈ ∞MetSp ↔ ( 𝐾 ∈ TopSp ∧ ( TopOpen ‘ 𝐾 ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ) )
20 eqid ⊢ ( TopOpen ‘ 𝐿 ) = ( TopOpen ‘ 𝐿 )
21 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
22 eqid ⊢ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) )
23 20 21 22 isxms ⊢ ( 𝐿 ∈ ∞MetSp ↔ ( 𝐿 ∈ TopSp ∧ ( TopOpen ‘ 𝐿 ) = ( MetOpen ‘ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) )
24 15 19 23 3bitr4g ⊢ ( 𝜑 → ( 𝐾 ∈ ∞MetSp ↔ 𝐿 ∈ ∞MetSp ) )