Theorem prdsxmslem1

Description: Lemma for prdsms . The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	prdsxms.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdsxms.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	prdsxms.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	prdsxms.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
	prdsxms.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsxms.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ ∞MetSp )
Assertion	prdsxmslem1	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		prdsxms.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdsxms.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
3		prdsxms.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
4		prdsxms.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
5		prdsxms.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
6		prdsxms.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ ∞MetSp )
7		eqid	⊢ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
8		eqid	⊢ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
9		eqid	⊢ ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑘 ) )
10		eqid	⊢ ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) = ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
11		eqid	⊢ ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
12	6	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp )
13	9 10	xmsxmet	⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp → ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
14	12 13	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
15	7 8 9 10 11 2 3 12 14	prdsxmet	⊢ ( 𝜑 → ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) ) )
16	6	feqmptd	⊢ ( 𝜑 → 𝑅 = ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
17	16	oveq2d	⊢ ( 𝜑 → ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
18	1 17	syl5eq	⊢ ( 𝜑 → 𝑌 = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
19	18	fveq2d	⊢ ( 𝜑 → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
20	4 19	syl5eq	⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
21	18	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
22	5 21	syl5eq	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
23	22	fveq2d	⊢ ( 𝜑 → ( ∞Met ‘ 𝐵 ) = ( ∞Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) ) )
24	15 20 23	3eltr4d	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )