Metamath Proof Explorer


Theorem tususs

Description: The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017)

Ref Expression
Hypothesis tuslem.k K = toUnifSp U
Assertion tususs U UnifOn X U = UnifSt K

Proof

Step Hyp Ref Expression
1 tuslem.k K = toUnifSp U
2 1 tusunif U UnifOn X U = UnifSet K
3 ustuni U UnifOn X U = X × X
4 2 unieqd U UnifOn X U = UnifSet K
5 1 tusbas U UnifOn X X = Base K
6 5 sqxpeqd U UnifOn X X × X = Base K × Base K
7 3 4 6 3eqtr3rd U UnifOn X Base K × Base K = UnifSet K
8 eqid Base K = Base K
9 eqid UnifSet K = UnifSet K
10 8 9 ussid Base K × Base K = UnifSet K UnifSet K = UnifSt K
11 7 10 syl U UnifOn X UnifSet K = UnifSt K
12 2 11 eqtrd U UnifOn X U = UnifSt K