Metamath Proof Explorer

Theorem mspropd

Description: Property deduction for a 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 mspropd 
|- ( 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 3 4 xmspropd 
 |-  ( ph -> ( K e. *MetSp <-> L e. *MetSp ) )
6 1 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( ( Base ` K ) X. ( Base ` K ) ) )
7 6 reseq2d 
 |-  ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
8 3 7 eqtr3d 
 |-  ( ph -> ( ( dist ` L ) |` ( B X. B ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
9 2 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( ( Base ` L ) X. ( Base ` L ) ) )
10 9 reseq2d 
 |-  ( ph -> ( ( dist ` L ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) )
11 8 10 eqtr3d 
 |-  ( ph -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) )
12 1 2 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
13 12 fveq2d 
 |-  ( ph -> ( Met ` ( Base ` K ) ) = ( Met ` ( Base ` L ) ) )
14 11 13 eleq12d 
 |-  ( ph -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) <-> ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) e. ( Met ` ( Base ` L ) ) ) )
15 5 14 anbi12d 
 |-  ( ph -> ( ( K e. *MetSp /\ ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) ) <-> ( L e. *MetSp /\ ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) e. ( Met ` ( 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 isms 
 |-  ( K e. MetSp <-> ( K e. *MetSp /\ ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( 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 isms 
 |-  ( L e. MetSp <-> ( L e. *MetSp /\ ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) e. ( Met ` ( Base ` L ) ) ) )
24 15 19 23 3bitr4g 
 |-  ( ph -> ( K e. MetSp <-> L e. MetSp ) )