Metamath Proof Explorer

Theorem repwsmet

Description: The supremum metric on RR ^ I is a metric. (Contributed by Jeff Madsen, 15-Sep-2015)

Ref Expression
Hypotheses rrnequiv.y 
|- Y = ( ( CCfld |`s RR ) ^s I )
rrnequiv.d 
|- D = ( dist ` Y )
rrnequiv.1 
|- X = ( RR ^m I )
Assertion repwsmet 
|- ( I e. Fin -> D e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 rrnequiv.y 
 |-  Y = ( ( CCfld |`s RR ) ^s I )
2 rrnequiv.d 
 |-  D = ( dist ` Y )
3 rrnequiv.1 
 |-  X = ( RR ^m I )
4 fconstmpt 
 |-  ( I X. { ( CCfld |`s RR ) } ) = ( k e. I |-> ( CCfld |`s RR ) )
5 4 oveq2i 
 |-  ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) = ( ( Scalar ` CCfld ) Xs_ ( k e. I |-> ( CCfld |`s RR ) ) )
6 eqid 
 |-  ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) = ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) )
7 ax-resscn 
 |-  RR C_ CC
8 eqid 
 |-  ( CCfld |`s RR ) = ( CCfld |`s RR )
9 cnfldbas 
 |-  CC = ( Base ` CCfld )
10 8 9 ressbas2 
 |-  ( RR C_ CC -> RR = ( Base ` ( CCfld |`s RR ) ) )
11 7 10 ax-mp 
 |-  RR = ( Base ` ( CCfld |`s RR ) )
12 reex 
 |-  RR e. _V
13 cnfldds 
 |-  ( abs o. - ) = ( dist ` CCfld )
14 8 13 ressds 
 |-  ( RR e. _V -> ( abs o. - ) = ( dist ` ( CCfld |`s RR ) ) )
15 12 14 ax-mp 
 |-  ( abs o. - ) = ( dist ` ( CCfld |`s RR ) )
16 15 reseq1i 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( dist ` ( CCfld |`s RR ) ) |` ( RR X. RR ) )
17 eqid 
 |-  ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) = ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) )
18 fvexd 
 |-  ( I e. Fin -> ( Scalar ` CCfld ) e. _V )
19 id 
 |-  ( I e. Fin -> I e. Fin )
20 ovex 
 |-  ( CCfld |`s RR ) e. _V
21 20 a1i 
 |-  ( ( I e. Fin /\ k e. I ) -> ( CCfld |`s RR ) e. _V )
22 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
23 22 remet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR )
24 23 a1i 
 |-  ( ( I e. Fin /\ k e. I ) -> ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR ) )
25 5 6 11 16 17 18 19 21 24 prdsmet 
 |-  ( I e. Fin -> ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) e. ( Met ` ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) ) )
26 eqid 
 |-  ( Scalar ` CCfld ) = ( Scalar ` CCfld )
27 8 26 resssca 
 |-  ( RR e. _V -> ( Scalar ` CCfld ) = ( Scalar ` ( CCfld |`s RR ) ) )
28 12 27 ax-mp 
 |-  ( Scalar ` CCfld ) = ( Scalar ` ( CCfld |`s RR ) )
29 1 28 pwsval 
 |-  ( ( ( CCfld |`s RR ) e. _V /\ I e. Fin ) -> Y = ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) )
30 20 29 mpan 
 |-  ( I e. Fin -> Y = ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) )
31 30 fveq2d 
 |-  ( I e. Fin -> ( dist ` Y ) = ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
32 2 31 syl5eq 
 |-  ( I e. Fin -> D = ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
33 1 11 pwsbas 
 |-  ( ( ( CCfld |`s RR ) e. _V /\ I e. Fin ) -> ( RR ^m I ) = ( Base ` Y ) )
34 20 33 mpan 
 |-  ( I e. Fin -> ( RR ^m I ) = ( Base ` Y ) )
35 30 fveq2d 
 |-  ( I e. Fin -> ( Base ` Y ) = ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
36 34 35 eqtrd 
 |-  ( I e. Fin -> ( RR ^m I ) = ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
37 3 36 syl5eq 
 |-  ( I e. Fin -> X = ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
38 37 fveq2d 
 |-  ( I e. Fin -> ( Met ` X ) = ( Met ` ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) ) )
39 25 32 38 3eltr4d 
 |-  ( I e. Fin -> D e. ( Met ` X ) )