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 ) )

Metamath Proof Explorer

Theorem xmspropd

Proof