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 ( 𝐴𝑉 → ( UnifSt ‘ ( 𝑊s 𝐴 ) ) = ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
2 eqid ( UnifSet ‘ 𝑊 ) = ( UnifSet ‘ 𝑊 )
3 1 2 ussval ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) = ( UnifSt ‘ 𝑊 )
4 3 oveq1i ( ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ↾t ( 𝐴 × 𝐴 ) ) = ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) )
5 fvex ( UnifSet ‘ 𝑊 ) ∈ V
6 fvex ( Base ‘ 𝑊 ) ∈ V
7 6 6 xpex ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ∈ V
8 sqxpexg ( 𝐴𝑉 → ( 𝐴 × 𝐴 ) ∈ V )
9 restco ( ( ( UnifSet ‘ 𝑊 ) ∈ V ∧ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ∈ V ∧ ( 𝐴 × 𝐴 ) ∈ V ) → ( ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ↾t ( 𝐴 × 𝐴 ) ) = ( ( UnifSet ‘ 𝑊 ) ↾t ( ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) )
10 5 7 8 9 mp3an12i ( 𝐴𝑉 → ( ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ↾t ( 𝐴 × 𝐴 ) ) = ( ( UnifSet ‘ 𝑊 ) ↾t ( ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) )
11 4 10 eqtr3id ( 𝐴𝑉 → ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) = ( ( UnifSet ‘ 𝑊 ) ↾t ( ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) )
12 inxp ( ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( Base ‘ 𝑊 ) ∩ 𝐴 ) × ( ( Base ‘ 𝑊 ) ∩ 𝐴 ) )
13 incom ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) = ( ( Base ‘ 𝑊 ) ∩ 𝐴 )
14 eqid ( 𝑊s 𝐴 ) = ( 𝑊s 𝐴 )
15 14 1 ressbas ( 𝐴𝑉 → ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) = ( Base ‘ ( 𝑊s 𝐴 ) ) )
16 13 15 eqtr3id ( 𝐴𝑉 → ( ( Base ‘ 𝑊 ) ∩ 𝐴 ) = ( Base ‘ ( 𝑊s 𝐴 ) ) )
17 16 sqxpeqd ( 𝐴𝑉 → ( ( ( Base ‘ 𝑊 ) ∩ 𝐴 ) × ( ( Base ‘ 𝑊 ) ∩ 𝐴 ) ) = ( ( Base ‘ ( 𝑊s 𝐴 ) ) × ( Base ‘ ( 𝑊s 𝐴 ) ) ) )
18 12 17 syl5eq ( 𝐴𝑉 → ( ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( Base ‘ ( 𝑊s 𝐴 ) ) × ( Base ‘ ( 𝑊s 𝐴 ) ) ) )
19 18 oveq2d ( 𝐴𝑉 → ( ( UnifSet ‘ 𝑊 ) ↾t ( ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ ( 𝑊s 𝐴 ) ) × ( Base ‘ ( 𝑊s 𝐴 ) ) ) ) )
20 14 2 ressunif ( 𝐴𝑉 → ( UnifSet ‘ 𝑊 ) = ( UnifSet ‘ ( 𝑊s 𝐴 ) ) )
21 20 oveq1d ( 𝐴𝑉 → ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ ( 𝑊s 𝐴 ) ) × ( Base ‘ ( 𝑊s 𝐴 ) ) ) ) = ( ( UnifSet ‘ ( 𝑊s 𝐴 ) ) ↾t ( ( Base ‘ ( 𝑊s 𝐴 ) ) × ( Base ‘ ( 𝑊s 𝐴 ) ) ) ) )
22 eqid ( Base ‘ ( 𝑊s 𝐴 ) ) = ( Base ‘ ( 𝑊s 𝐴 ) )
23 eqid ( UnifSet ‘ ( 𝑊s 𝐴 ) ) = ( UnifSet ‘ ( 𝑊s 𝐴 ) )
24 22 23 ussval ( ( UnifSet ‘ ( 𝑊s 𝐴 ) ) ↾t ( ( Base ‘ ( 𝑊s 𝐴 ) ) × ( Base ‘ ( 𝑊s 𝐴 ) ) ) ) = ( UnifSt ‘ ( 𝑊s 𝐴 ) )
25 24 a1i ( 𝐴𝑉 → ( ( UnifSet ‘ ( 𝑊s 𝐴 ) ) ↾t ( ( Base ‘ ( 𝑊s 𝐴 ) ) × ( Base ‘ ( 𝑊s 𝐴 ) ) ) ) = ( UnifSt ‘ ( 𝑊s 𝐴 ) ) )
26 19 21 25 3eqtrd ( 𝐴𝑉 → ( ( UnifSet ‘ 𝑊 ) ↾t ( ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) = ( UnifSt ‘ ( 𝑊s 𝐴 ) ) )
27 11 26 eqtr2d ( 𝐴𝑉 → ( UnifSt ‘ ( 𝑊s 𝐴 ) ) = ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) )