Metamath Proof Explorer

Theorem ressuss

Description: Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017)

Ref Expression
Assertion ressuss 
|- ( A e. V -> ( UnifSt ` ( W |`s A ) ) = ( ( UnifSt ` W ) |`t ( A X. A ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` W ) = ( Base ` W )
2 eqid 
 |-  ( UnifSet ` W ) = ( UnifSet ` W )
3 1 2 ussval 
 |-  ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) = ( UnifSt ` W )
4 3 oveq1i 
 |-  ( ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) |`t ( A X. A ) ) = ( ( UnifSt ` W ) |`t ( A X. A ) )
5 fvex 
 |-  ( UnifSet ` W ) e. _V
6 fvex 
 |-  ( Base ` W ) e. _V
7 6 6 xpex 
 |-  ( ( Base ` W ) X. ( Base ` W ) ) e. _V
8 sqxpexg 
 |-  ( A e. V -> ( A X. A ) e. _V )
9 restco 
 |-  ( ( ( UnifSet ` W ) e. _V /\ ( ( Base ` W ) X. ( Base ` W ) ) e. _V /\ ( A X. A ) e. _V ) -> ( ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) |`t ( A X. A ) ) = ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) )
10 5 7 8 9 mp3an12i 
 |-  ( A e. V -> ( ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) |`t ( A X. A ) ) = ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) )
11 4 10 eqtr3id 
 |-  ( A e. V -> ( ( UnifSt ` W ) |`t ( A X. A ) ) = ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) )
12 inxp 
 |-  ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) = ( ( ( Base ` W ) i^i A ) X. ( ( Base ` W ) i^i A ) )
13 incom 
 |-  ( A i^i ( Base ` W ) ) = ( ( Base ` W ) i^i A )
14 eqid 
 |-  ( W |`s A ) = ( W |`s A )
15 14 1 ressbas 
 |-  ( A e. V -> ( A i^i ( Base ` W ) ) = ( Base ` ( W |`s A ) ) )
16 13 15 eqtr3id 
 |-  ( A e. V -> ( ( Base ` W ) i^i A ) = ( Base ` ( W |`s A ) ) )
17 16 sqxpeqd 
 |-  ( A e. V -> ( ( ( Base ` W ) i^i A ) X. ( ( Base ` W ) i^i A ) ) = ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) )
18 12 17 eqtrid 
 |-  ( A e. V -> ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) = ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) )
19 18 oveq2d 
 |-  ( A e. V -> ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) = ( ( UnifSet ` W ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) )
20 14 2 ressunif 
 |-  ( A e. V -> ( UnifSet ` W ) = ( UnifSet ` ( W |`s A ) ) )
21 20 oveq1d 
 |-  ( A e. V -> ( ( UnifSet ` W ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) = ( ( UnifSet ` ( W |`s A ) ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) )
22 eqid 
 |-  ( Base ` ( W |`s A ) ) = ( Base ` ( W |`s A ) )
23 eqid 
 |-  ( UnifSet ` ( W |`s A ) ) = ( UnifSet ` ( W |`s A ) )
24 22 23 ussval 
 |-  ( ( UnifSet ` ( W |`s A ) ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) = ( UnifSt ` ( W |`s A ) )
25 24 a1i 
 |-  ( A e. V -> ( ( UnifSet ` ( W |`s A ) ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) = ( UnifSt ` ( W |`s A ) ) )
26 19 21 25 3eqtrd 
 |-  ( A e. V -> ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) = ( UnifSt ` ( W |`s A ) ) )
27 11 26 eqtr2d 
 |-  ( A e. V -> ( UnifSt ` ( W |`s A ) ) = ( ( UnifSt ` W ) |`t ( A X. A ) ) )