ressprdsds

Description: Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015)

	Ref	Expression
Hypotheses	ressprdsds.y	$⊢ φ \to Y = S ⨉_{𝑠} (x \in I ⟼ R)$
	ressprdsds.h	$⊢ φ \to H = T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A)$
	ressprdsds.b	$⊢ B = {Base}_{H}$
	ressprdsds.d	$⊢ D = dist (Y)$
	ressprdsds.e	$⊢ E = dist (H)$
	ressprdsds.s	$⊢ φ \to S \in U$
	ressprdsds.t	$⊢ φ \to T \in V$
	ressprdsds.i	$⊢ φ \to I \in W$
	ressprdsds.r	$⊢ (φ \land x \in I) \to R \in X$
	ressprdsds.a	$⊢ (φ \land x \in I) \to A \in Z$
Assertion	ressprdsds	$⊢ φ \to E = {D ↾}_{(B \times B)}$

Proof

Step	Hyp	Ref	Expression
1		ressprdsds.y	$⊢ φ \to Y = S ⨉_{𝑠} (x \in I ⟼ R)$
2		ressprdsds.h	$⊢ φ \to H = T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A)$
3		ressprdsds.b	$⊢ B = {Base}_{H}$
4		ressprdsds.d	$⊢ D = dist (Y)$
5		ressprdsds.e	$⊢ E = dist (H)$
6		ressprdsds.s	$⊢ φ \to S \in U$
7		ressprdsds.t	$⊢ φ \to T \in V$
8		ressprdsds.i	$⊢ φ \to I \in W$
9		ressprdsds.r	$⊢ (φ \land x \in I) \to R \in X$
10		ressprdsds.a	$⊢ (φ \land x \in I) \to A \in Z$
11		ovres	$⊢ (f \in B \land g \in B) \to f ({D ↾}_{(B \times B)}) g = f D g$
12	11	adantl	$⊢ (φ \land (f \in B \land g \in B)) \to f ({D ↾}_{(B \times B)}) g = f D g$
13		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
14		eqid	$⊢ dist (R) = dist (R)$
15	13 14	ressds	$⊢ A \in Z \to dist (R) = dist (R ↾_{𝑠} A)$
16	10 15	syl	$⊢ (φ \land x \in I) \to dist (R) = dist (R ↾_{𝑠} A)$
17	16	oveqd	$⊢ (φ \land x \in I) \to f (x) dist (R) g (x) = f (x) dist (R ↾_{𝑠} A) g (x)$
18	17	mpteq2dva	$⊢ φ \to (x \in I ⟼ f (x) dist (R) g (x)) = (x \in I ⟼ f (x) dist (R ↾_{𝑠} A) g (x))$
19	18	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to (x \in I ⟼ f (x) dist (R) g (x)) = (x \in I ⟼ f (x) dist (R ↾_{𝑠} A) g (x))$
20	19	rneqd	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) dist (R) g (x)) = ran (x \in I ⟼ f (x) dist (R ↾_{𝑠} A) g (x))$
21	20	uneq1d	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) dist (R) g (x)) \cup \{0\} = ran (x \in I ⟼ f (x) dist (R ↾_{𝑠} A) g (x)) \cup \{0\}$
22	21	supeq1d	$⊢ (φ \land (f \in B \land g \in B)) \to sup (ran (x \in I ⟼ f (x) dist (R) g (x)) \cup \{0\} ℝ^{} <) = sup (ran (x \in I ⟼ f (x) dist (R ↾_{𝑠} A) g (x)) \cup \{0\} ℝ^{} <)$
23		eqid	$⊢ S ⨉_{𝑠} (x \in I ⟼ R) = S ⨉_{𝑠} (x \in I ⟼ R)$
24		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))}$
25	6	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to S \in U$
26	8	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to I \in W$
27	9	ralrimiva	$⊢ φ \to \forall x \in I R \in X$
28	27	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I R \in X$
29		eqid	$⊢ {Base}_{R} = {Base}_{R}$
30	13 29	ressbasss	$⊢ {Base}_{(R ↾_{𝑠} A)} \subseteq {Base}_{R}$
31	30	a1i	$⊢ (φ \land x \in I) \to {Base}_{(R ↾_{𝑠} A)} \subseteq {Base}_{R}$
32	31	ralrimiva	$⊢ φ \to \forall x \in I {Base}_{(R ↾_{𝑠} A)} \subseteq {Base}_{R}$
33		ss2ixp	$⊢ \forall x \in I {Base}_{(R ↾_{𝑠} A)} \subseteq {Base}_{R} \to \underset{x \in I}{⨉} {Base}_{(R ↾_{𝑠} A)} \subseteq \underset{x \in I}{⨉} {Base}_{R}$
34	32 33	syl	$⊢ φ \to \underset{x \in I}{⨉} {Base}_{(R ↾_{𝑠} A)} \subseteq \underset{x \in I}{⨉} {Base}_{R}$
35		eqid	$⊢ T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A) = T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A)$
36		eqid	$⊢ {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))} = {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))}$
37		ovex	$⊢ R ↾_{𝑠} A \in V$
38	37	rgenw	$⊢ \forall x \in I R ↾_{𝑠} A \in V$
39	38	a1i	$⊢ φ \to \forall x \in I R ↾_{𝑠} A \in V$
40		eqid	$⊢ {Base}_{(R ↾_{𝑠} A)} = {Base}_{(R ↾_{𝑠} A)}$
41	35 36 7 8 39 40	prdsbas3	$⊢ φ \to {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))} = \underset{x \in I}{⨉} {Base}_{(R ↾_{𝑠} A)}$
42	23 24 6 8 27 29	prdsbas3	$⊢ φ \to {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))} = \underset{x \in I}{⨉} {Base}_{R}$
43	34 41 42	3sstr4d	$⊢ φ \to {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))} \subseteq {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))}$
44	2	fveq2d	$⊢ φ \to {Base}_{H} = {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))}$
45	3 44	syl5eq	$⊢ φ \to B = {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))}$
46	1	fveq2d	$⊢ φ \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))}$
47	43 45 46	3sstr4d	$⊢ φ \to B \subseteq {Base}_{Y}$
48	47	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to B \subseteq {Base}_{Y}$
49	46	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))}$
50	48 49	sseqtrd	$⊢ (φ \land (f \in B \land g \in B)) \to B \subseteq {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))}$
51		simprl	$⊢ (φ \land (f \in B \land g \in B)) \to f \in B$
52	50 51	sseldd	$⊢ (φ \land (f \in B \land g \in B)) \to f \in {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))}$
53		simprr	$⊢ (φ \land (f \in B \land g \in B)) \to g \in B$
54	50 53	sseldd	$⊢ (φ \land (f \in B \land g \in B)) \to g \in {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))}$
55		eqid	$⊢ dist (S ⨉_{𝑠} (x \in I ⟼ R)) = dist (S ⨉_{𝑠} (x \in I ⟼ R))$
56	23 24 25 26 28 52 54 14 55	prdsdsval2	$⊢ (φ \land (f \in B \land g \in B)) \to f dist (S ⨉_{𝑠} (x \in I ⟼ R)) g = sup (ran (x \in I ⟼ f (x) dist (R) g (x)) \cup \{0\} ℝ^{*} <)$
57	7	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to T \in V$
58	38	a1i	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I R ↾_{𝑠} A \in V$
59	45	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to B = {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))}$
60	51 59	eleqtrd	$⊢ (φ \land (f \in B \land g \in B)) \to f \in {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))}$
61	53 59	eleqtrd	$⊢ (φ \land (f \in B \land g \in B)) \to g \in {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))}$
62		eqid	$⊢ dist (R ↾_{𝑠} A) = dist (R ↾_{𝑠} A)$
63		eqid	$⊢ dist (T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A)) = dist (T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))$
64	35 36 57 26 58 60 61 62 63	prdsdsval2	$⊢ (φ \land (f \in B \land g \in B)) \to f dist (T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A)) g = sup (ran (x \in I ⟼ f (x) dist (R ↾_{𝑠} A) g (x)) \cup \{0\} ℝ^{*} <)$
65	22 56 64	3eqtr4d	$⊢ (φ \land (f \in B \land g \in B)) \to f dist (S ⨉_{𝑠} (x \in I ⟼ R)) g = f dist (T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A)) g$
66	1	fveq2d	$⊢ φ \to dist (Y) = dist (S ⨉_{𝑠} (x \in I ⟼ R))$
67	4 66	syl5eq	$⊢ φ \to D = dist (S ⨉_{𝑠} (x \in I ⟼ R))$
68	67	oveqdr	$⊢ (φ \land (f \in B \land g \in B)) \to f D g = f dist (S ⨉_{𝑠} (x \in I ⟼ R)) g$
69	2	fveq2d	$⊢ φ \to dist (H) = dist (T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))$
70	5 69	syl5eq	$⊢ φ \to E = dist (T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))$
71	70	oveqdr	$⊢ (φ \land (f \in B \land g \in B)) \to f E g = f dist (T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A)) g$
72	65 68 71	3eqtr4d	$⊢ (φ \land (f \in B \land g \in B)) \to f D g = f E g$
73	12 72	eqtr2d	$⊢ (φ \land (f \in B \land g \in B)) \to f E g = f ({D ↾}_{(B \times B)}) g$
74	73	ralrimivva	$⊢ φ \to \forall f \in B \forall g \in B f E g = f ({D ↾}_{(B \times B)}) g$
75	8	mptexd	$⊢ φ \to (x \in I ⟼ R ↾_{𝑠} A) \in V$
76		eqid	$⊢ (x \in I ⟼ R ↾_{𝑠} A) = (x \in I ⟼ R ↾_{𝑠} A)$
77	37 76	dmmpti	$⊢ dom (x \in I ⟼ R ↾_{𝑠} A) = I$
78	77	a1i	$⊢ φ \to dom (x \in I ⟼ R ↾_{𝑠} A) = I$
79	35 7 75 36 78 63	prdsdsfn	$⊢ φ \to dist (T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A)) Fn ({Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))} \times {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))})$
80	45	sqxpeqd	$⊢ φ \to B \times B = {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))} \times {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))}$
81	70 80	fneq12d	$⊢ φ \to (E Fn (B \times B) \leftrightarrow dist (T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A)) Fn ({Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))} \times {Base}_{(T ⨉_{𝑠} (x \in I ⟼ R ↾_{𝑠} A))}))$
82	79 81	mpbird	$⊢ φ \to E Fn (B \times B)$
83	8	mptexd	$⊢ φ \to (x \in I ⟼ R) \in V$
84		dmmptg	$⊢ \forall x \in I R \in X \to dom (x \in I ⟼ R) = I$
85	27 84	syl	$⊢ φ \to dom (x \in I ⟼ R) = I$
86	23 6 83 24 85 55	prdsdsfn	$⊢ φ \to dist (S ⨉_{𝑠} (x \in I ⟼ R)) Fn ({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))} \times {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))})$
87	46	sqxpeqd	$⊢ φ \to {Base}_{Y} \times {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))} \times {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))}$
88	67 87	fneq12d	$⊢ φ \to (D Fn ({Base}_{Y} \times {Base}_{Y}) \leftrightarrow dist (S ⨉_{𝑠} (x \in I ⟼ R)) Fn ({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))} \times {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R))}))$
89	86 88	mpbird	$⊢ φ \to D Fn ({Base}_{Y} \times {Base}_{Y})$
90		xpss12	$⊢ (B \subseteq {Base}_{Y} \land B \subseteq {Base}_{Y}) \to B \times B \subseteq {Base}_{Y} \times {Base}_{Y}$
91	47 47 90	syl2anc	$⊢ φ \to B \times B \subseteq {Base}_{Y} \times {Base}_{Y}$
92		fnssres	$⊢ (D Fn ({Base}_{Y} \times {Base}_{Y}) \land B \times B \subseteq {Base}_{Y} \times {Base}_{Y}) \to ({D ↾}_{(B \times B)}) Fn (B \times B)$
93	89 91 92	syl2anc	$⊢ φ \to ({D ↾}_{(B \times B)}) Fn (B \times B)$
94		eqfnov2	$⊢ (E Fn (B \times B) \land ({D ↾}_{(B \times B)}) Fn (B \times B)) \to (E = {D ↾}_{(B \times B)} \leftrightarrow \forall f \in B \forall g \in B f E g = f ({D ↾}_{(B \times B)}) g)$
95	82 93 94	syl2anc	$⊢ φ \to (E = {D ↾}_{(B \times B)} \leftrightarrow \forall f \in B \forall g \in B f E g = f ({D ↾}_{(B \times B)}) g)$
96	74 95	mpbird	$⊢ φ \to E = {D ↾}_{(B \times B)}$

Metamath Proof Explorer

Theorem ressprdsds

Proof