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 ) )