Theorem ressxms

Description: The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Assertion	ressxms	|- ( ( K e. *MetSp /\ A e. V ) -> ( K |`s A ) e. *MetSp )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` K ) = ( Base ` K )
2		eqid	|- ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
3	1 2	xmsxmet	|- ( K e. *MetSp -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) )
4	3	adantr	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) )
5		xmetres	|- ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) e. ( *Met ` ( ( Base ` K ) i^i A ) ) )
6	4 5	syl	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) e. ( *Met ` ( ( Base ` K ) i^i A ) ) )
7		resres	|- ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) X. ( Base ` K ) ) i^i ( A X. A ) ) )
8		inxp	|- ( ( ( Base ` K ) X. ( Base ` K ) ) i^i ( A X. A ) ) = ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) )
9	8	reseq2i	|- ( ( dist ` K ) |` ( ( ( Base ` K ) X. ( Base ` K ) ) i^i ( A X. A ) ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) )
10	7 9	eqtri	|- ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) )
11		eqid	|- ( K |`s A ) = ( K |`s A )
12		eqid	|- ( dist ` K ) = ( dist ` K )
13	11 12	ressds	|- ( A e. V -> ( dist ` K ) = ( dist ` ( K |`s A ) ) )
14	13	adantl	|- ( ( K e. *MetSp /\ A e. V ) -> ( dist ` K ) = ( dist ` ( K |`s A ) ) )
15		incom	|- ( ( Base ` K ) i^i A ) = ( A i^i ( Base ` K ) )
16	11 1	ressbas	|- ( A e. V -> ( A i^i ( Base ` K ) ) = ( Base ` ( K |`s A ) ) )
17	16	adantl	|- ( ( K e. *MetSp /\ A e. V ) -> ( A i^i ( Base ` K ) ) = ( Base ` ( K |`s A ) ) )
18	15 17	syl5eq	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( Base ` K ) i^i A ) = ( Base ` ( K |`s A ) ) )
19	18	sqxpeqd	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) = ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) )
20	14 19	reseq12d	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) ) = ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
21	10 20	syl5eq	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
22	18	fveq2d	|- ( ( K e. *MetSp /\ A e. V ) -> ( *Met ` ( ( Base ` K ) i^i A ) ) = ( *Met ` ( Base ` ( K |`s A ) ) ) )
23	6 21 22	3eltr3d	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) e. ( *Met ` ( Base ` ( K |`s A ) ) ) )
24		eqid	|- ( TopOpen ` K ) = ( TopOpen ` K )
25	24 1 2	xmstopn	|- ( K e. *MetSp -> ( TopOpen ` K ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
26	25	adantr	|- ( ( K e. *MetSp /\ A e. V ) -> ( TopOpen ` K ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
27	26	oveq1d	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t ( ( Base ` K ) i^i A ) ) = ( ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) |`t ( ( Base ` K ) i^i A ) ) )
28		inss1	|- ( ( Base ` K ) i^i A ) C_ ( Base ` K )
29		xpss12	|- ( ( ( ( Base ` K ) i^i A ) C_ ( Base ` K ) /\ ( ( Base ` K ) i^i A ) C_ ( Base ` K ) ) -> ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) C_ ( ( Base ` K ) X. ( Base ` K ) ) )
30	28 28 29	mp2an	|- ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) C_ ( ( Base ` K ) X. ( Base ` K ) )
31		resabs1	|- ( ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) C_ ( ( Base ` K ) X. ( Base ` K ) ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) ) )
32	30 31	ax-mp	|- ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) )
33	10 32	eqtr4i	|- ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) )
34		eqid	|- ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
35		eqid	|- ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) = ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) )
36	33 34 35	metrest	|- ( ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) /\ ( ( Base ` K ) i^i A ) C_ ( Base ` K ) ) -> ( ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) |`t ( ( Base ` K ) i^i A ) ) = ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) )
37	4 28 36	sylancl	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) |`t ( ( Base ` K ) i^i A ) ) = ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) )
38	27 37	eqtrd	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t ( ( Base ` K ) i^i A ) ) = ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) )
39		xmstps	|- ( K e. *MetSp -> K e. TopSp )
40	1 24	tpsuni	|- ( K e. TopSp -> ( Base ` K ) = U. ( TopOpen ` K ) )
41	39 40	syl	|- ( K e. *MetSp -> ( Base ` K ) = U. ( TopOpen ` K ) )
42	41	adantr	|- ( ( K e. *MetSp /\ A e. V ) -> ( Base ` K ) = U. ( TopOpen ` K ) )
43	42	ineq2d	|- ( ( K e. *MetSp /\ A e. V ) -> ( A i^i ( Base ` K ) ) = ( A i^i U. ( TopOpen ` K ) ) )
44	15 43	syl5eq	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( Base ` K ) i^i A ) = ( A i^i U. ( TopOpen ` K ) ) )
45	44	oveq2d	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t ( ( Base ` K ) i^i A ) ) = ( ( TopOpen ` K ) |`t ( A i^i U. ( TopOpen ` K ) ) ) )
46	1 24	istps	|- ( K e. TopSp <-> ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) )
47	39 46	sylib	|- ( K e. *MetSp -> ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) )
48		eqid	|- U. ( TopOpen ` K ) = U. ( TopOpen ` K )
49	48	restin	|- ( ( ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) /\ A e. V ) -> ( ( TopOpen ` K ) |`t A ) = ( ( TopOpen ` K ) |`t ( A i^i U. ( TopOpen ` K ) ) ) )
50	47 49	sylan	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t A ) = ( ( TopOpen ` K ) |`t ( A i^i U. ( TopOpen ` K ) ) ) )
51	45 50	eqtr4d	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t ( ( Base ` K ) i^i A ) ) = ( ( TopOpen ` K ) |`t A ) )
52	21	fveq2d	|- ( ( K e. *MetSp /\ A e. V ) -> ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) = ( MetOpen ` ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) )
53	38 51 52	3eqtr3d	|- ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t A ) = ( MetOpen ` ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) )
54	11 24	resstopn	|- ( ( TopOpen ` K ) |`t A ) = ( TopOpen ` ( K |`s A ) )
55		eqid	|- ( Base ` ( K |`s A ) ) = ( Base ` ( K |`s A ) )
56		eqid	|- ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) = ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) )
57	54 55 56	isxms2	|- ( ( K |`s A ) e. *MetSp <-> ( ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) e. ( *Met ` ( Base ` ( K |`s A ) ) ) /\ ( ( TopOpen ` K ) |`t A ) = ( MetOpen ` ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) ) )
58	23 53 57	sylanbrc	|- ( ( K e. *MetSp /\ A e. V ) -> ( K |`s A ) e. *MetSp )