Metamath Proof Explorer

Theorem tmsxps

Description: Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tmsxps.p 
|- P = ( dist ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) )
tmsxps.1 
|- ( ph -> M e. ( *Met ` X ) )
tmsxps.2 
|- ( ph -> N e. ( *Met ` Y ) )
Assertion tmsxps 
|- ( ph -> P e. ( *Met ` ( X X. Y ) ) )

Proof

Step Hyp Ref Expression
1 tmsxps.p 
 |-  P = ( dist ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) )
2 tmsxps.1 
 |-  ( ph -> M e. ( *Met ` X ) )
3 tmsxps.2 
 |-  ( ph -> N e. ( *Met ` Y ) )
4 eqid 
 |-  ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) = ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) )
5 eqid 
 |-  ( Base ` ( toMetSp ` M ) ) = ( Base ` ( toMetSp ` M ) )
6 eqid 
 |-  ( Base ` ( toMetSp ` N ) ) = ( Base ` ( toMetSp ` N ) )
7 eqid 
 |-  ( toMetSp ` M ) = ( toMetSp ` M )
8 7 tmsxms 
 |-  ( M e. ( *Met ` X ) -> ( toMetSp ` M ) e. *MetSp )
9 2 8 syl 
 |-  ( ph -> ( toMetSp ` M ) e. *MetSp )
10 eqid 
 |-  ( toMetSp ` N ) = ( toMetSp ` N )
11 10 tmsxms 
 |-  ( N e. ( *Met ` Y ) -> ( toMetSp ` N ) e. *MetSp )
12 3 11 syl 
 |-  ( ph -> ( toMetSp ` N ) e. *MetSp )
13 4 5 6 9 12 1 xpsdsfn2 
 |-  ( ph -> P Fn ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) )
14 fnresdm 
 |-  ( P Fn ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) -> ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) = P )
15 13 14 syl 
 |-  ( ph -> ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) = P )
16 4 xpsxms 
 |-  ( ( ( toMetSp ` M ) e. *MetSp /\ ( toMetSp ` N ) e. *MetSp ) -> ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) e. *MetSp )
17 9 12 16 syl2anc 
 |-  ( ph -> ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) e. *MetSp )
18 eqid 
 |-  ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) )
19 18 1 xmsxmet2 
 |-  ( ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) e. *MetSp -> ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) e. ( *Met ` ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) )
20 17 19 syl 
 |-  ( ph -> ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) e. ( *Met ` ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) )
21 15 20 eqeltrrd 
 |-  ( ph -> P e. ( *Met ` ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) )
22 7 tmsbas 
 |-  ( M e. ( *Met ` X ) -> X = ( Base ` ( toMetSp ` M ) ) )
23 2 22 syl 
 |-  ( ph -> X = ( Base ` ( toMetSp ` M ) ) )
24 10 tmsbas 
 |-  ( N e. ( *Met ` Y ) -> Y = ( Base ` ( toMetSp ` N ) ) )
25 3 24 syl 
 |-  ( ph -> Y = ( Base ` ( toMetSp ` N ) ) )
26 23 25 xpeq12d 
 |-  ( ph -> ( X X. Y ) = ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` N ) ) ) )
27 4 5 6 9 12 xpsbas 
 |-  ( ph -> ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` N ) ) ) = ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) )
28 26 27 eqtrd 
 |-  ( ph -> ( X X. Y ) = ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) )
29 28 fveq2d 
 |-  ( ph -> ( *Met ` ( X X. Y ) ) = ( *Met ` ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) )
30 21 29 eleqtrrd 
 |-  ( ph -> P e. ( *Met ` ( X X. Y ) ) )