Metamath Proof Explorer

Theorem cmspropd

Description: Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 cmspropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 cmspropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 cmspropd.3 
 |-  ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )
4 cmspropd.4 
 |-  ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
5 1 2 3 4 mspropd 
 |-  ( 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 -> ( CMet ` ( Base ` K ) ) = ( CMet ` ( Base ` L ) ) )
14 11 13 eleq12d 
 |-  ( ph -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( CMet ` ( Base ` K ) ) <-> ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) e. ( CMet ` ( Base ` L ) ) ) )
15 5 14 anbi12d 
 |-  ( ph -> ( ( K e. MetSp /\ ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( CMet ` ( Base ` K ) ) ) <-> ( L e. MetSp /\ ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) e. ( CMet ` ( Base ` L ) ) ) ) )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 eqid 
 |-  ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
18 16 17 iscms 
 |-  ( K e. CMetSp <-> ( K e. MetSp /\ ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( CMet ` ( Base ` K ) ) ) )
19 eqid 
 |-  ( Base ` L ) = ( Base ` L )
20 eqid 
 |-  ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) )
21 19 20 iscms 
 |-  ( L e. CMetSp <-> ( L e. MetSp /\ ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) e. ( CMet ` ( Base ` L ) ) ) )
22 15 18 21 3bitr4g 
 |-  ( ph -> ( K e. CMetSp <-> L e. CMetSp ) )