Theorem ressprdsds

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

	Ref	Expression
Hypotheses	ressprdsds.y	|- ( ph -> Y = ( S Xs_ ( x e. I |-> R ) ) )
	ressprdsds.h	|- ( ph -> H = ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) )
	ressprdsds.b	|- B = ( Base ` H )
	ressprdsds.d	|- D = ( dist ` Y )
	ressprdsds.e	|- E = ( dist ` H )
	ressprdsds.s	|- ( ph -> S e. U )
	ressprdsds.t	|- ( ph -> T e. V )
	ressprdsds.i	|- ( ph -> I e. W )
	ressprdsds.r	|- ( ( ph /\ x e. I ) -> R e. X )
	ressprdsds.a	|- ( ( ph /\ x e. I ) -> A e. Z )
Assertion	ressprdsds	|- ( ph -> E = ( D |` ( B X. B ) ) )

Proof

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