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 e. ( UnifOn ` X ) -> U = ( UnifSt ` K ) )

Proof

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