cnmpt2ds

Description: Continuity of the metric function; analogue of cnmpt22f which cannot be used directly because D is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	cnmpt1ds.d	\|- D = ( dist ` G )
	cnmpt1ds.j	\|- J = ( TopOpen ` G )
	cnmpt1ds.r	\|- R = ( topGen ` ran (,) )
	cnmpt1ds.g	\|- ( ph -> G e. MetSp )
	cnmpt1ds.k	\|- ( ph -> K e. ( TopOn ` X ) )
	cnmpt2ds.l	\|- ( ph -> L e. ( TopOn ` Y ) )
	cnmpt2ds.a	\|- ( ph -> ( x e. X , y e. Y \|-> A ) e. ( ( K tX L ) Cn J ) )
	cnmpt2ds.b	\|- ( ph -> ( x e. X , y e. Y \|-> B ) e. ( ( K tX L ) Cn J ) )
Assertion	cnmpt2ds	\|- ( ph -> ( x e. X , y e. Y \|-> ( A D B ) ) e. ( ( K tX L ) Cn R ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt1ds.d	\|- D = ( dist ` G )
2		cnmpt1ds.j	\|- J = ( TopOpen ` G )
3		cnmpt1ds.r	\|- R = ( topGen ` ran (,) )
4		cnmpt1ds.g	\|- ( ph -> G e. MetSp )
5		cnmpt1ds.k	\|- ( ph -> K e. ( TopOn ` X ) )
6		cnmpt2ds.l	\|- ( ph -> L e. ( TopOn ` Y ) )
7		cnmpt2ds.a	\|- ( ph -> ( x e. X , y e. Y \|-> A ) e. ( ( K tX L ) Cn J ) )
8		cnmpt2ds.b	\|- ( ph -> ( x e. X , y e. Y \|-> B ) e. ( ( K tX L ) Cn J ) )
9		txtopon	\|- ( ( K e. ( TopOn ` X ) /\ L e. ( TopOn ` Y ) ) -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )
10	5 6 9	syl2anc	\|- ( ph -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )
11		mstps	\|- ( G e. MetSp -> G e. TopSp )
12	4 11	syl	\|- ( ph -> G e. TopSp )
13		eqid	\|- ( Base ` G ) = ( Base ` G )
14	13 2	istps	\|- ( G e. TopSp <-> J e. ( TopOn ` ( Base ` G ) ) )
15	12 14	sylib	\|- ( ph -> J e. ( TopOn ` ( Base ` G ) ) )
16		cnf2	\|- ( ( ( K tX L ) e. ( TopOn ` ( X X. Y ) ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X , y e. Y \|-> A ) e. ( ( K tX L ) Cn J ) ) -> ( x e. X , y e. Y \|-> A ) : ( X X. Y ) --> ( Base ` G ) )
17	10 15 7 16	syl3anc	\|- ( ph -> ( x e. X , y e. Y \|-> A ) : ( X X. Y ) --> ( Base ` G ) )
18		eqid	\|- ( x e. X , y e. Y \|-> A ) = ( x e. X , y e. Y \|-> A )
19	18	fmpo	\|- ( A. x e. X A. y e. Y A e. ( Base ` G ) <-> ( x e. X , y e. Y \|-> A ) : ( X X. Y ) --> ( Base ` G ) )
20	17 19	sylibr	\|- ( ph -> A. x e. X A. y e. Y A e. ( Base ` G ) )
21	20	r19.21bi	\|- ( ( ph /\ x e. X ) -> A. y e. Y A e. ( Base ` G ) )
22	21	r19.21bi	\|- ( ( ( ph /\ x e. X ) /\ y e. Y ) -> A e. ( Base ` G ) )
23		cnf2	\|- ( ( ( K tX L ) e. ( TopOn ` ( X X. Y ) ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X , y e. Y \|-> B ) e. ( ( K tX L ) Cn J ) ) -> ( x e. X , y e. Y \|-> B ) : ( X X. Y ) --> ( Base ` G ) )
24	10 15 8 23	syl3anc	\|- ( ph -> ( x e. X , y e. Y \|-> B ) : ( X X. Y ) --> ( Base ` G ) )
25		eqid	\|- ( x e. X , y e. Y \|-> B ) = ( x e. X , y e. Y \|-> B )
26	25	fmpo	\|- ( A. x e. X A. y e. Y B e. ( Base ` G ) <-> ( x e. X , y e. Y \|-> B ) : ( X X. Y ) --> ( Base ` G ) )
27	24 26	sylibr	\|- ( ph -> A. x e. X A. y e. Y B e. ( Base ` G ) )
28	27	r19.21bi	\|- ( ( ph /\ x e. X ) -> A. y e. Y B e. ( Base ` G ) )
29	28	r19.21bi	\|- ( ( ( ph /\ x e. X ) /\ y e. Y ) -> B e. ( Base ` G ) )
30	22 29	ovresd	\|- ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( A ( D \|` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) = ( A D B ) )
31	30	3impa	\|- ( ( ph /\ x e. X /\ y e. Y ) -> ( A ( D \|` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) = ( A D B ) )
32	31	mpoeq3dva	\|- ( ph -> ( x e. X , y e. Y \|-> ( A ( D \|` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) ) = ( x e. X , y e. Y \|-> ( A D B ) ) )
33	13 1 2 3	msdcn	\|- ( G e. MetSp -> ( D \|` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( ( J tX J ) Cn R ) )
34	4 33	syl	\|- ( ph -> ( D \|` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( ( J tX J ) Cn R ) )
35	5 6 7 8 34	cnmpt22f	\|- ( ph -> ( x e. X , y e. Y \|-> ( A ( D \|` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) ) e. ( ( K tX L ) Cn R ) )
36	32 35	eqeltrrd	\|- ( ph -> ( x e. X , y e. Y \|-> ( A D B ) ) e. ( ( K tX L ) Cn R ) )

Metamath Proof Explorer

Theorem cnmpt2ds

Proof