prdsdsval

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

	Ref	Expression
Hypotheses	prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
	prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsbasmpt.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsbasmpt.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsbasmpt.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
	prdsplusgval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	prdsplusgval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	prdsdsval.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
Assertion	prdsdsval	⊢ ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
2		prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		prdsbasmpt.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdsbasmpt.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		prdsbasmpt.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
6		prdsplusgval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		prdsplusgval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8		prdsdsval.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
9		fnex	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
10	5 4 9	syl2anc	⊢ ( 𝜑 → 𝑅 ∈ V )
11		fndm	⊢ ( 𝑅 Fn 𝐼 → dom 𝑅 = 𝐼 )
12	5 11	syl	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
13	1 3 10 2 12 8	prdsds	⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) )
14		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
15		fveq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
16	14 15	oveqan12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
18	17	mpteq2dv	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
19	18	rneqd	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
20	19	uneq1d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) = ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
21	20	supeq1d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )
22		xrltso	⊢ < Or ℝ^*
23	22	supex	⊢ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ∈ V
24	23	a1i	⊢ ( 𝜑 → sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ∈ V )
25	13 21 6 7 24	ovmpod	⊢ ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )

Metamath Proof Explorer

Theorem prdsdsval

Proof