Metamath Proof Explorer

Theorem resspwsds

Description: Restriction of a power metric. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypotheses resspwsds.y 
|- ( ph -> Y = ( R ^s I ) )
resspwsds.h 
|- ( ph -> H = ( ( R |`s A ) ^s I ) )
resspwsds.b 
|- B = ( Base ` H )
resspwsds.d 
|- D = ( dist ` Y )
resspwsds.e 
|- E = ( dist ` H )
resspwsds.i 
|- ( ph -> I e. V )
resspwsds.r 
|- ( ph -> R e. W )
resspwsds.a 
|- ( ph -> A e. X )
Assertion resspwsds 
|- ( ph -> E = ( D |` ( B X. B ) ) )

Proof

Step Hyp Ref Expression
1 resspwsds.y 
 |-  ( ph -> Y = ( R ^s I ) )
2 resspwsds.h 
 |-  ( ph -> H = ( ( R |`s A ) ^s I ) )
3 resspwsds.b 
 |-  B = ( Base ` H )
4 resspwsds.d 
 |-  D = ( dist ` Y )
5 resspwsds.e 
 |-  E = ( dist ` H )
6 resspwsds.i 
 |-  ( ph -> I e. V )
7 resspwsds.r 
 |-  ( ph -> R e. W )
8 resspwsds.a 
 |-  ( ph -> A e. X )
9 eqid 
 |-  ( R ^s I ) = ( R ^s I )
10 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
11 9 10 pwsval 
 |-  ( ( R e. W /\ I e. V ) -> ( R ^s I ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
12 7 6 11 syl2anc 
 |-  ( ph -> ( R ^s I ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
13 fconstmpt 
 |-  ( I X. { R } ) = ( x e. I |-> R )
14 13 oveq2i 
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( x e. I |-> R ) )
15 12 14 eqtrdi 
 |-  ( ph -> ( R ^s I ) = ( ( Scalar ` R ) Xs_ ( x e. I |-> R ) ) )
16 1 15 eqtrd 
 |-  ( ph -> Y = ( ( Scalar ` R ) Xs_ ( x e. I |-> R ) ) )
17 ovex 
 |-  ( R |`s A ) e. _V
18 eqid 
 |-  ( ( R |`s A ) ^s I ) = ( ( R |`s A ) ^s I )
19 eqid 
 |-  ( Scalar ` ( R |`s A ) ) = ( Scalar ` ( R |`s A ) )
20 18 19 pwsval 
 |-  ( ( ( R |`s A ) e. _V /\ I e. V ) -> ( ( R |`s A ) ^s I ) = ( ( Scalar ` ( R |`s A ) ) Xs_ ( I X. { ( R |`s A ) } ) ) )
21 17 6 20 sylancr 
 |-  ( ph -> ( ( R |`s A ) ^s I ) = ( ( Scalar ` ( R |`s A ) ) Xs_ ( I X. { ( R |`s A ) } ) ) )
22 fconstmpt 
 |-  ( I X. { ( R |`s A ) } ) = ( x e. I |-> ( R |`s A ) )
23 22 oveq2i 
 |-  ( ( Scalar ` ( R |`s A ) ) Xs_ ( I X. { ( R |`s A ) } ) ) = ( ( Scalar ` ( R |`s A ) ) Xs_ ( x e. I |-> ( R |`s A ) ) )
24 21 23 eqtrdi 
 |-  ( ph -> ( ( R |`s A ) ^s I ) = ( ( Scalar ` ( R |`s A ) ) Xs_ ( x e. I |-> ( R |`s A ) ) ) )
25 2 24 eqtrd 
 |-  ( ph -> H = ( ( Scalar ` ( R |`s A ) ) Xs_ ( x e. I |-> ( R |`s A ) ) ) )
26 fvexd 
 |-  ( ph -> ( Scalar ` R ) e. _V )
27 fvexd 
 |-  ( ph -> ( Scalar ` ( R |`s A ) ) e. _V )
28 7 adantr 
 |-  ( ( ph /\ x e. I ) -> R e. W )
29 8 adantr 
 |-  ( ( ph /\ x e. I ) -> A e. X )
30 16 25 3 4 5 26 27 6 28 29 ressprdsds 
 |-  ( ph -> E = ( D |` ( B X. B ) ) )