prdsdsval3

Description: Value of the metric in a structure product. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	prdsbasmpt2.y	\|- Y = ( S Xs_ ( x e. I \|-> R ) )
	prdsbasmpt2.b	\|- B = ( Base ` Y )
	prdsbasmpt2.s	\|- ( ph -> S e. V )
	prdsbasmpt2.i	\|- ( ph -> I e. W )
	prdsbasmpt2.r	\|- ( ph -> A. x e. I R e. X )
	prdsdsval2.f	\|- ( ph -> F e. B )
	prdsdsval2.g	\|- ( ph -> G e. B )
	prdsdsval3.k	\|- K = ( Base ` R )
	prdsdsval3.e	\|- E = ( ( dist ` R ) \|` ( K X. K ) )
	prdsdsval3.d	\|- D = ( dist ` Y )
Assertion	prdsdsval3	\|- ( ph -> ( F D G ) = sup ( ( ran ( x e. I \|-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	\|- Y = ( S Xs_ ( x e. I \|-> R ) )
2		prdsbasmpt2.b	\|- B = ( Base ` Y )
3		prdsbasmpt2.s	\|- ( ph -> S e. V )
4		prdsbasmpt2.i	\|- ( ph -> I e. W )
5		prdsbasmpt2.r	\|- ( ph -> A. x e. I R e. X )
6		prdsdsval2.f	\|- ( ph -> F e. B )
7		prdsdsval2.g	\|- ( ph -> G e. B )
8		prdsdsval3.k	\|- K = ( Base ` R )
9		prdsdsval3.e	\|- E = ( ( dist ` R ) \|` ( K X. K ) )
10		prdsdsval3.d	\|- D = ( dist ` Y )
11		eqid	\|- ( dist ` R ) = ( dist ` R )
12	1 2 3 4 5 6 7 11 10	prdsdsval2	\|- ( ph -> ( F D G ) = sup ( ( ran ( x e. I \|-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )
13		eqidd	\|- ( ph -> I = I )
14	1 2 3 4 5 8 6	prdsbascl	\|- ( ph -> A. x e. I ( F ` x ) e. K )
15	1 2 3 4 5 8 7	prdsbascl	\|- ( ph -> A. x e. I ( G ` x ) e. K )
16	9	oveqi	\|- ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( ( dist ` R ) \|` ( K X. K ) ) ( G ` x ) )
17		ovres	\|- ( ( ( F ` x ) e. K /\ ( G ` x ) e. K ) -> ( ( F ` x ) ( ( dist ` R ) \|` ( K X. K ) ) ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) )
18	16 17	eqtrid	\|- ( ( ( F ` x ) e. K /\ ( G ` x ) e. K ) -> ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) )
19	18	ex	\|- ( ( F ` x ) e. K -> ( ( G ` x ) e. K -> ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
20	19	ral2imi	\|- ( A. x e. I ( F ` x ) e. K -> ( A. x e. I ( G ` x ) e. K -> A. x e. I ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
21	14 15 20	sylc	\|- ( ph -> A. x e. I ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) )
22		mpteq12	\|- ( ( I = I /\ A. x e. I ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) -> ( x e. I \|-> ( ( F ` x ) E ( G ` x ) ) ) = ( x e. I \|-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
23	13 21 22	syl2anc	\|- ( ph -> ( x e. I \|-> ( ( F ` x ) E ( G ` x ) ) ) = ( x e. I \|-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
24	23	rneqd	\|- ( ph -> ran ( x e. I \|-> ( ( F ` x ) E ( G ` x ) ) ) = ran ( x e. I \|-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
25	24	uneq1d	\|- ( ph -> ( ran ( x e. I \|-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) = ( ran ( x e. I \|-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) u. { 0 } ) )
26	25	supeq1d	\|- ( ph -> sup ( ( ran ( x e. I \|-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) = sup ( ( ran ( x e. I \|-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )
27	12 26	eqtr4d	\|- ( ph -> ( F D G ) = sup ( ( ran ( x e. I \|-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )

Metamath Proof Explorer

Theorem prdsdsval3

Proof