Metamath Proof Explorer

Theorem xmspropd

Description: Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses xmspropd.1 
|- ( ph -> B = ( Base ` K ) )
xmspropd.2 
|- ( ph -> B = ( Base ` L ) )
xmspropd.3 
|- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )
xmspropd.4 
|- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
Assertion xmspropd 
|- ( ph -> ( K e. *MetSp <-> L e. *MetSp ) )

Proof

Step Hyp Ref Expression
1 xmspropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 xmspropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 xmspropd.3 
 |-  ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )
4 xmspropd.4 
 |-  ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
5 1 2 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
6 5 4 tpspropd 
 |-  ( ph -> ( K e. TopSp <-> L e. TopSp ) )
7 1 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( ( Base ` K ) X. ( Base ` K ) ) )
8 7 reseq2d 
 |-  ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
9 3 8 eqtr3d 
 |-  ( ph -> ( ( dist ` L ) |` ( B X. B ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
10 2 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( ( Base ` L ) X. ( Base ` L ) ) )
11 10 reseq2d 
 |-  ( ph -> ( ( dist ` L ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) )
12 9 11 eqtr3d 
 |-  ( ph -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) )
13 12 fveq2d 
 |-  ( ph -> ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) = ( MetOpen ` ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) )
14 4 13 eqeq12d 
 |-  ( ph -> ( ( TopOpen ` K ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) <-> ( TopOpen ` L ) = ( MetOpen ` ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) )
15 6 14 anbi12d 
 |-  ( ph -> ( ( K e. TopSp /\ ( TopOpen ` K ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) ) <-> ( L e. TopSp /\ ( TopOpen ` L ) = ( MetOpen ` ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) ) )
16 eqid 
 |-  ( TopOpen ` K ) = ( TopOpen ` K )
17 eqid 
 |-  ( Base ` K ) = ( Base ` K )
18 eqid 
 |-  ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
19 16 17 18 isxms 
 |-  ( K e. *MetSp <-> ( K e. TopSp /\ ( TopOpen ` K ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) ) )
20 eqid 
 |-  ( TopOpen ` L ) = ( TopOpen ` L )
21 eqid 
 |-  ( Base ` L ) = ( Base ` L )
22 eqid 
 |-  ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) )
23 20 21 22 isxms 
 |-  ( L e. *MetSp <-> ( L e. TopSp /\ ( TopOpen ` L ) = ( MetOpen ` ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) )
24 15 19 23 3bitr4g 
 |-  ( ph -> ( K e. *MetSp <-> L e. *MetSp ) )