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 syl5eqr ⊢ ( 𝐴 ∈ 𝑉 → ( ( 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 syl5eqr ⊢ ( 𝐴 ∈ 𝑉 → ( ( 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 ( 𝐴 × 𝐴 ) ) )