ressxms

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

		Ref	Expression
	Assertion	ressxms	$⊢ (K \in ∞MetSp \land A \in V) \to K ↾_{𝑠} A \in ∞MetSp$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{K} = {Base}_{K}$
2		eqid	$⊢ {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} = {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}$
3	1 2	xmsxmet	$⊢ K \in ∞MetSp \to {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in ∞Met ({Base}_{K})$
4	3	adantr	$⊢ (K \in ∞MetSp \land A \in V) \to {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in ∞Met ({Base}_{K})$
5		xmetres	$⊢ {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in ∞Met ({Base}_{K}) \to {({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)} \in ∞Met ({Base}_{K} \cap A)$
6	4 5	syl	$⊢ (K \in ∞MetSp \land A \in V) \to {({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)} \in ∞Met ({Base}_{K} \cap A)$
7		resres	$⊢ {({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)} = {dist (K) ↾}_{(({Base}_{K} \times {Base}_{K}) \cap (A \times A))}$
8		inxp	$⊢ ({Base}_{K} \times {Base}_{K}) \cap (A \times A) = ({Base}_{K} \cap A) \times ({Base}_{K} \cap A)$
9	8	reseq2i	$⊢ {dist (K) ↾}_{(({Base}_{K} \times {Base}_{K}) \cap (A \times A))} = {dist (K) ↾}_{(({Base}_{K} \cap A) \times ({Base}_{K} \cap A))}$
10	7 9	eqtri	$⊢ {({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)} = {dist (K) ↾}_{(({Base}_{K} \cap A) \times ({Base}_{K} \cap A))}$
11		eqid	$⊢ K ↾_{𝑠} A = K ↾_{𝑠} A$
12		eqid	$⊢ dist (K) = dist (K)$
13	11 12	ressds	$⊢ A \in V \to dist (K) = dist (K ↾_{𝑠} A)$
14	13	adantl	$⊢ (K \in ∞MetSp \land A \in V) \to dist (K) = dist (K ↾_{𝑠} A)$
15		incom	$⊢ {Base}_{K} \cap A = A \cap {Base}_{K}$
16	11 1	ressbas	$⊢ A \in V \to A \cap {Base}_{K} = {Base}_{(K ↾_{𝑠} A)}$
17	16	adantl	$⊢ (K \in ∞MetSp \land A \in V) \to A \cap {Base}_{K} = {Base}_{(K ↾_{𝑠} A)}$
18	15 17	eqtrid	$⊢ (K \in ∞MetSp \land A \in V) \to {Base}_{K} \cap A = {Base}_{(K ↾_{𝑠} A)}$
19	18	sqxpeqd	$⊢ (K \in ∞MetSp \land A \in V) \to ({Base}_{K} \cap A) \times ({Base}_{K} \cap A) = {Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)}$
20	14 19	reseq12d	$⊢ (K \in ∞MetSp \land A \in V) \to {dist (K) ↾}_{(({Base}_{K} \cap A) \times ({Base}_{K} \cap A))} = {dist (K ↾_{𝑠} A) ↾}_{({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})}$
21	10 20	eqtrid	$⊢ (K \in ∞MetSp \land A \in V) \to {({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)} = {dist (K ↾_{𝑠} A) ↾}_{({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})}$
22	18	fveq2d	$⊢ (K \in ∞MetSp \land A \in V) \to ∞Met ({Base}_{K} \cap A) = ∞Met ({Base}_{(K ↾_{𝑠} A)})$
23	6 21 22	3eltr3d	$⊢ (K \in ∞MetSp \land A \in V) \to {dist (K ↾_{𝑠} A) ↾}_{({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})} \in ∞Met ({Base}_{(K ↾_{𝑠} A)})$
24		eqid	$⊢ TopOpen (K) = TopOpen (K)$
25	24 1 2	xmstopn	$⊢ K \in ∞MetSp \to TopOpen (K) = MetOpen ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})})$
26	25	adantr	$⊢ (K \in ∞MetSp \land A \in V) \to TopOpen (K) = MetOpen ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})})$
27	26	oveq1d	$⊢ (K \in ∞MetSp \land A \in V) \to TopOpen (K) ↾_{𝑡} ({Base}_{K} \cap A) = MetOpen ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾_{𝑡} ({Base}_{K} \cap A)$
28		inss1	$⊢ {Base}_{K} \cap A \subseteq {Base}_{K}$
29		xpss12	$⊢ ({Base}_{K} \cap A \subseteq {Base}_{K} \land {Base}_{K} \cap A \subseteq {Base}_{K}) \to ({Base}_{K} \cap A) \times ({Base}_{K} \cap A) \subseteq {Base}_{K} \times {Base}_{K}$
30	28 28 29	mp2an	$⊢ ({Base}_{K} \cap A) \times ({Base}_{K} \cap A) \subseteq {Base}_{K} \times {Base}_{K}$
31		resabs1	$⊢ ({Base}_{K} \cap A) \times ({Base}_{K} \cap A) \subseteq {Base}_{K} \times {Base}_{K} \to {({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(({Base}_{K} \cap A) \times ({Base}_{K} \cap A))} = {dist (K) ↾}_{(({Base}_{K} \cap A) \times ({Base}_{K} \cap A))}$
32	30 31	ax-mp	$⊢ {({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(({Base}_{K} \cap A) \times ({Base}_{K} \cap A))} = {dist (K) ↾}_{(({Base}_{K} \cap A) \times ({Base}_{K} \cap A))}$
33	10 32	eqtr4i	$⊢ {({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)} = {({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(({Base}_{K} \cap A) \times ({Base}_{K} \cap A))}$
34		eqid	$⊢ MetOpen ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) = MetOpen ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})})$
35		eqid	$⊢ MetOpen ({({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)}) = MetOpen ({({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)})$
36	33 34 35	metrest	$⊢ ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in ∞Met ({Base}_{K}) \land {Base}_{K} \cap A \subseteq {Base}_{K}) \to MetOpen ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾_{𝑡} ({Base}_{K} \cap A) = MetOpen ({({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)})$
37	4 28 36	sylancl	$⊢ (K \in ∞MetSp \land A \in V) \to MetOpen ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾_{𝑡} ({Base}_{K} \cap A) = MetOpen ({({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)})$
38	27 37	eqtrd	$⊢ (K \in ∞MetSp \land A \in V) \to TopOpen (K) ↾_{𝑡} ({Base}_{K} \cap A) = MetOpen ({({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)})$
39		xmstps	$⊢ K \in ∞MetSp \to K \in TopSp$
40	1 24	tpsuni	$⊢ K \in TopSp \to {Base}_{K} = ⋃ TopOpen (K)$
41	39 40	syl	$⊢ K \in ∞MetSp \to {Base}_{K} = ⋃ TopOpen (K)$
42	41	adantr	$⊢ (K \in ∞MetSp \land A \in V) \to {Base}_{K} = ⋃ TopOpen (K)$
43	42	ineq2d	$⊢ (K \in ∞MetSp \land A \in V) \to A \cap {Base}_{K} = A \cap ⋃ TopOpen (K)$
44	15 43	eqtrid	$⊢ (K \in ∞MetSp \land A \in V) \to {Base}_{K} \cap A = A \cap ⋃ TopOpen (K)$
45	44	oveq2d	$⊢ (K \in ∞MetSp \land A \in V) \to TopOpen (K) ↾_{𝑡} ({Base}_{K} \cap A) = TopOpen (K) ↾_{𝑡} (A \cap ⋃ TopOpen (K))$
46	1 24	istps	$⊢ K \in TopSp \leftrightarrow TopOpen (K) \in TopOn ({Base}_{K})$
47	39 46	sylib	$⊢ K \in ∞MetSp \to TopOpen (K) \in TopOn ({Base}_{K})$
48		eqid	$⊢ ⋃ TopOpen (K) = ⋃ TopOpen (K)$
49	48	restin	$⊢ (TopOpen (K) \in TopOn ({Base}_{K}) \land A \in V) \to TopOpen (K) ↾_{𝑡} A = TopOpen (K) ↾_{𝑡} (A \cap ⋃ TopOpen (K))$
50	47 49	sylan	$⊢ (K \in ∞MetSp \land A \in V) \to TopOpen (K) ↾_{𝑡} A = TopOpen (K) ↾_{𝑡} (A \cap ⋃ TopOpen (K))$
51	45 50	eqtr4d	$⊢ (K \in ∞MetSp \land A \in V) \to TopOpen (K) ↾_{𝑡} ({Base}_{K} \cap A) = TopOpen (K) ↾_{𝑡} A$
52	21	fveq2d	$⊢ (K \in ∞MetSp \land A \in V) \to MetOpen ({({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}) ↾}_{(A \times A)}) = MetOpen ({dist (K ↾_{𝑠} A) ↾}_{({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})})$
53	38 51 52	3eqtr3d	$⊢ (K \in ∞MetSp \land A \in V) \to TopOpen (K) ↾_{𝑡} A = MetOpen ({dist (K ↾_{𝑠} A) ↾}_{({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})})$
54	11 24	resstopn	$⊢ TopOpen (K) ↾_{𝑡} A = TopOpen (K ↾_{𝑠} A)$
55		eqid	$⊢ {Base}_{(K ↾_{𝑠} A)} = {Base}_{(K ↾_{𝑠} A)}$
56		eqid	$⊢ {dist (K ↾_{𝑠} A) ↾}_{({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})} = {dist (K ↾_{𝑠} A) ↾}_{({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})}$
57	54 55 56	isxms2	$⊢ K ↾_{𝑠} A \in ∞MetSp \leftrightarrow ({dist (K ↾_{𝑠} A) ↾}_{({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})} \in ∞Met ({Base}_{(K ↾_{𝑠} A)}) \land TopOpen (K) ↾_{𝑡} A = MetOpen ({dist (K ↾_{𝑠} A) ↾}_{({Base}_{(K ↾_{𝑠} A)} \times {Base}_{(K ↾_{𝑠} A)})}))$
58	23 53 57	sylanbrc	$⊢ (K \in ∞MetSp \land A \in V) \to K ↾_{𝑠} A \in ∞MetSp$

Metamath Proof Explorer

Theorem ressxms

Proof