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
|- Y = ( S Xs_ ( x e. I |-> R ) )
prdsdsf.b
|- B = ( Base ` Y )
prdsdsf.v
|- V = ( Base ` R )
prdsdsf.e
|- E = ( ( dist ` R ) |` ( V X. V ) )
prdsdsf.d
|- D = ( dist ` Y )
prdsdsf.s
|- ( ph -> S e. W )
prdsdsf.i
|- ( ph -> I e. X )
prdsdsf.r
|- ( ( ph /\ x e. I ) -> R e. Z )
prdsdsf.m
|- ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
Assertion prdsxmet
|- ( ph -> D e. ( *Met ` B ) )

Proof

Step Hyp Ref Expression
1 prdsdsf.y
 |-  Y = ( S Xs_ ( x e. I |-> R ) )
2 prdsdsf.b
 |-  B = ( Base ` Y )
3 prdsdsf.v
 |-  V = ( Base ` R )
4 prdsdsf.e
 |-  E = ( ( dist ` R ) |` ( V X. V ) )
5 prdsdsf.d
 |-  D = ( dist ` Y )
6 prdsdsf.s
 |-  ( ph -> S e. W )
7 prdsdsf.i
 |-  ( ph -> I e. X )
8 prdsdsf.r
 |-  ( ( ph /\ x e. I ) -> R e. Z )
9 prdsdsf.m
 |-  ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
10 nfcv
 |-  F/_ y R
11 nfcsb1v
 |-  F/_ x [_ y / x ]_ R
12 csbeq1a
 |-  ( x = y -> R = [_ y / x ]_ R )
13 10 11 12 cbvmpt
 |-  ( x e. I |-> R ) = ( y e. I |-> [_ y / x ]_ R )
14 13 oveq2i
 |-  ( S Xs_ ( x e. I |-> R ) ) = ( S Xs_ ( y e. I |-> [_ y / x ]_ R ) )
15 1 14 eqtri
 |-  Y = ( S Xs_ ( y e. I |-> [_ y / x ]_ R ) )
16 eqid
 |-  ( Base ` [_ y / x ]_ R ) = ( Base ` [_ y / x ]_ R )
17 eqid
 |-  ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) = ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) )
18 8 elexd
 |-  ( ( ph /\ x e. I ) -> R e. _V )
19 18 ralrimiva
 |-  ( ph -> A. x e. I R e. _V )
20 11 nfel1
 |-  F/ x [_ y / x ]_ R e. _V
21 12 eleq1d
 |-  ( x = y -> ( R e. _V <-> [_ y / x ]_ R e. _V ) )
22 20 21 rspc
 |-  ( y e. I -> ( A. x e. I R e. _V -> [_ y / x ]_ R e. _V ) )
23 19 22 mpan9
 |-  ( ( ph /\ y e. I ) -> [_ y / x ]_ R e. _V )
24 9 ralrimiva
 |-  ( ph -> A. x e. I E e. ( *Met ` V ) )
25 nfcv
 |-  F/_ x dist
26 25 11 nffv
 |-  F/_ x ( dist ` [_ y / x ]_ R )
27 nfcv
 |-  F/_ x Base
28 27 11 nffv
 |-  F/_ x ( Base ` [_ y / x ]_ R )
29 28 28 nfxp
 |-  F/_ x ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) )
30 26 29 nfres
 |-  F/_ x ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) )
31 nfcv
 |-  F/_ x *Met
32 31 28 nffv
 |-  F/_ x ( *Met ` ( Base ` [_ y / x ]_ R ) )
33 30 32 nfel
 |-  F/ x ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) e. ( *Met ` ( Base ` [_ y / x ]_ R ) )
34 12 fveq2d
 |-  ( x = y -> ( dist ` R ) = ( dist ` [_ y / x ]_ R ) )
35 12 fveq2d
 |-  ( x = y -> ( Base ` R ) = ( Base ` [_ y / x ]_ R ) )
36 3 35 syl5eq
 |-  ( x = y -> V = ( Base ` [_ y / x ]_ R ) )
37 36 sqxpeqd
 |-  ( x = y -> ( V X. V ) = ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) )
38 34 37 reseq12d
 |-  ( x = y -> ( ( dist ` R ) |` ( V X. V ) ) = ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) )
39 4 38 syl5eq
 |-  ( x = y -> E = ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) )
40 36 fveq2d
 |-  ( x = y -> ( *Met ` V ) = ( *Met ` ( Base ` [_ y / x ]_ R ) ) )
41 39 40 eleq12d
 |-  ( x = y -> ( E e. ( *Met ` V ) <-> ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) e. ( *Met ` ( Base ` [_ y / x ]_ R ) ) ) )
42 33 41 rspc
 |-  ( y e. I -> ( A. x e. I E e. ( *Met ` V ) -> ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) e. ( *Met ` ( Base ` [_ y / x ]_ R ) ) ) )
43 24 42 mpan9
 |-  ( ( ph /\ y e. I ) -> ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) e. ( *Met ` ( Base ` [_ y / x ]_ R ) ) )
44 15 2 16 17 5 6 7 23 43 prdsxmetlem
 |-  ( ph -> D e. ( *Met ` B ) )