Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  resspwsds Structured version   Unicode version

Theorem resspwsds 18402
 Description: Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015.)
Hypotheses
Ref Expression
resspwsds.y s
resspwsds.h s s
resspwsds.b
resspwsds.d
resspwsds.e
resspwsds.i
resspwsds.r
resspwsds.a
Assertion
Ref Expression
resspwsds

Proof of Theorem resspwsds
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 resspwsds.y . . 3 s
2 resspwsds.r . . . . 5
3 resspwsds.i . . . . 5
4 eqid 2436 . . . . . 6 s s
5 eqid 2436 . . . . . 6 Scalar Scalar
64, 5pwsval 13708 . . . . 5 s Scalars
72, 3, 6syl2anc 643 . . . 4 s Scalars
8 fconstmpt 4921 . . . . 5
98oveq2i 6092 . . . 4 Scalars Scalars
107, 9syl6eq 2484 . . 3 s Scalars
111, 10eqtrd 2468 . 2 Scalars
12 resspwsds.h . . 3 s s
13 ovex 6106 . . . . 5 s
14 eqid 2436 . . . . . 6 s s s s
15 eqid 2436 . . . . . 6 Scalars Scalars
1614, 15pwsval 13708 . . . . 5 s s s Scalars s s
1713, 3, 16sylancr 645 . . . 4 s s Scalars s s
18 fconstmpt 4921 . . . . 5 s s
1918oveq2i 6092 . . . 4 Scalars s s Scalars s s
2017, 19syl6eq 2484 . . 3 s s Scalars s s
2112, 20eqtrd 2468 . 2 Scalars s s
22 resspwsds.b . 2
23 resspwsds.d . 2
24 resspwsds.e . 2
25 fvex 5742 . . 3 Scalar
2625a1i 11 . 2 Scalar
27 fvex 5742 . . 3 Scalars
2827a1i 11 . 2 Scalars