prdsdsval3

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

	Ref	Expression
Hypotheses	prdsbasmpt2.y	⊢ 𝑌 = ( 𝑆 X_s ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
	prdsbasmpt2.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsbasmpt2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsbasmpt2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsbasmpt2.r	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
	prdsdsval2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	prdsdsval2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	prdsdsval3.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	prdsdsval3.e	⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐾 × 𝐾 ) )
	prdsdsval3.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
Assertion	prdsdsval3	⊢ ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	⊢ 𝑌 = ( 𝑆 X_s ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2		prdsbasmpt2.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		prdsbasmpt2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdsbasmpt2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		prdsbasmpt2.r	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
6		prdsdsval2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		prdsdsval2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8		prdsdsval3.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
9		prdsdsval3.e	⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐾 × 𝐾 ) )
10		prdsdsval3.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
11		eqid	⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
12	1 2 3 4 5 6 7 11 10	prdsdsval2	⊢ ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )
13		eqidd	⊢ ( 𝜑 → 𝐼 = 𝐼 )
14	1 2 3 4 5 8 6	prdsbascl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 )
15	1 2 3 4 5 8 7	prdsbascl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 )
16	9	oveqi	⊢ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐾 × 𝐾 ) ) ( 𝐺 ‘ 𝑥 ) )
17		ovres	⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝑥 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐾 × 𝐾 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) )
18	16 17	eqtrid	⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) )
19	18	ex	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 → ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
20	19	ral2imi	⊢ ( ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 → ( ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
21	14 15 20	sylc	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) )
22		mpteq12	⊢ ( ( 𝐼 = 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
23	13 21 22	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
24	23	rneqd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
25	24	uneq1d	⊢ ( 𝜑 → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) = ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
26	25	supeq1d	⊢ ( 𝜑 → sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )
27	12 26	eqtr4d	⊢ ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )

Metamath Proof Explorer

Theorem prdsdsval3

Proof