This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid 
 |-  ( 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 eqtrid 
 |-  ( 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 ) )