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 eqtrid ⊒ ( π‘₯ = 𝑦 β†’ 𝑉 = ( Base β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) )
37 36 sqxpeqd ⊒ ( π‘₯ = 𝑦 β†’ ( 𝑉 Γ— 𝑉 ) = ( ( Base β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) Γ— ( Base β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) ) )
38 34 37 reseq12d ⊒ ( π‘₯ = 𝑦 β†’ ( ( dist β€˜ 𝑅 ) β†Ύ ( 𝑉 Γ— 𝑉 ) ) = ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ( Base β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) Γ— ( Base β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) ) ) )
39 4 38 eqtrid ⊒ ( π‘₯ = 𝑦 β†’ 𝐸 = ( ( 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 β€˜ 𝐡 ) )