Metamath Proof Explorer

Theorem prdsxmet

Description: The product metric is an extended metric. Eliminate disjoint variable conditions from prdsxmetlem . (Contributed by Mario Carneiro, 26-Sep-2015)

Ref Expression
Hypotheses prdsdsf.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
prdsdsf.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsdsf.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
prdsdsf.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
prdsdsf.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
prdsdsf.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
prdsdsf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
prdsdsf.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑍 )
prdsdsf.m ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
Assertion prdsxmet ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 prdsdsf.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2 prdsdsf.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsdsf.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
4 prdsdsf.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
5 prdsdsf.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
6 prdsdsf.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
7 prdsdsf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
8 prdsdsf.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑍 )
9 prdsdsf.m ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
10 nfcv ⊢ Ⅎ 𝑦 𝑅
11 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝑅
12 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝑅 = ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
13 10 11 12 cbvmpt ⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = ( 𝑦 ∈ 𝐼 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
14 13 oveq2i ⊢ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) = ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
15 1 14 eqtri ⊢ 𝑌 = ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
16 eqid ⊢ ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) = ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
17 eqid ⊢ ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) ) = ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) )
18 8 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ V )
19 18 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ V )
20 11 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ∈ V
21 12 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝑅 ∈ V ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ∈ V ) )
22 20 21 rspc ⊢ ( 𝑦 ∈ 𝐼 → ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ V → ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ∈ V ) )
23 19 22 mpan9 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ∈ V )
24 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
25 nfcv ⊢ Ⅎ 𝑥 dist
26 25 11 nffv ⊢ Ⅎ 𝑥 ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
27 nfcv ⊢ Ⅎ 𝑥 Base
28 27 11 nffv ⊢ Ⅎ 𝑥 ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
29 28 28 nfxp ⊢ Ⅎ 𝑥 ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
30 26 29 nfres ⊢ Ⅎ 𝑥 ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) )
31 nfcv ⊢ Ⅎ 𝑥 ∞Met
32 31 28 nffv ⊢ Ⅎ 𝑥 ( ∞Met ‘ ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
33 30 32 nfel ⊢ Ⅎ 𝑥 ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
34 12 fveq2d ⊢ ( 𝑥 = 𝑦 → ( dist ‘ 𝑅 ) = ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
35 12 fveq2d ⊢ ( 𝑥 = 𝑦 → ( Base ‘ 𝑅 ) = ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
36 3 35 syl5eq ⊢ ( 𝑥 = 𝑦 → 𝑉 = ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
37 36 sqxpeqd ⊢ ( 𝑥 = 𝑦 → ( 𝑉 × 𝑉 ) = ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) )
38 34 37 reseq12d ⊢ ( 𝑥 = 𝑦 → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) = ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) ) )
39 4 38 syl5eq ⊢ ( 𝑥 = 𝑦 → 𝐸 = ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) ) )
40 36 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ∞Met ‘ 𝑉 ) = ( ∞Met ‘ ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) )
41 39 40 eleq12d ⊢ ( 𝑥 = 𝑦 → ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ↔ ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) ) )
42 33 41 rspc ⊢ ( 𝑦 ∈ 𝐼 → ( ∀ 𝑥 ∈ 𝐼 𝐸 ∈ ( ∞Met ‘ 𝑉 ) → ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) ) )
43 24 42 mpan9 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) × ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ) )
44 15 2 16 17 5 6 7 23 43 prdsxmetlem ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )