Metamath Proof Explorer

Theorem imasf1omet

Description: The image of a metric is a metric. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses imasf1oxmet.u 
|- ( ph -> U = ( F "s R ) )
imasf1oxmet.v 
|- ( ph -> V = ( Base ` R ) )
imasf1oxmet.f 
|- ( ph -> F : V -1-1-onto-> B )
imasf1oxmet.r 
|- ( ph -> R e. Z )
imasf1oxmet.e 
|- E = ( ( dist ` R ) |` ( V X. V ) )
imasf1oxmet.d 
|- D = ( dist ` U )
imasf1omet.m 
|- ( ph -> E e. ( Met ` V ) )
Assertion imasf1omet 
|- ( ph -> D e. ( Met ` B ) )

Proof

Step Hyp Ref Expression
1 imasf1oxmet.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasf1oxmet.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasf1oxmet.f 
 |-  ( ph -> F : V -1-1-onto-> B )
4 imasf1oxmet.r 
 |-  ( ph -> R e. Z )
5 imasf1oxmet.e 
 |-  E = ( ( dist ` R ) |` ( V X. V ) )
6 imasf1oxmet.d 
 |-  D = ( dist ` U )
7 imasf1omet.m 
 |-  ( ph -> E e. ( Met ` V ) )
8 metxmet 
 |-  ( E e. ( Met ` V ) -> E e. ( *Met ` V ) )
9 7 8 syl 
 |-  ( ph -> E e. ( *Met ` V ) )
10 1 2 3 4 5 6 9 imasf1oxmet 
 |-  ( ph -> D e. ( *Met ` B ) )
11 f1ofo 
 |-  ( F : V -1-1-onto-> B -> F : V -onto-> B )
12 3 11 syl 
 |-  ( ph -> F : V -onto-> B )
13 eqid 
 |-  ( dist ` R ) = ( dist ` R )
14 1 2 12 4 13 6 imasdsfn 
 |-  ( ph -> D Fn ( B X. B ) )
15 1 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> U = ( F "s R ) )
16 2 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> V = ( Base ` R ) )
17 3 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> F : V -1-1-onto-> B )
18 4 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> R e. Z )
19 9 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> E e. ( *Met ` V ) )
20 simprl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> a e. V )
21 simprr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> b e. V )
22 15 16 17 18 5 6 19 20 21 imasdsf1o 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( F ` a ) D ( F ` b ) ) = ( a E b ) )
23 metcl 
 |-  ( ( E e. ( Met ` V ) /\ a e. V /\ b e. V ) -> ( a E b ) e. RR )
24 23 3expb 
 |-  ( ( E e. ( Met ` V ) /\ ( a e. V /\ b e. V ) ) -> ( a E b ) e. RR )
25 7 24 sylan 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a E b ) e. RR )
26 22 25 eqeltrd 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( F ` a ) D ( F ` b ) ) e. RR )
27 26 ralrimivva 
 |-  ( ph -> A. a e. V A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR )
28 f1ofn 
 |-  ( F : V -1-1-onto-> B -> F Fn V )
29 3 28 syl 
 |-  ( ph -> F Fn V )
30 oveq2 
 |-  ( y = ( F ` b ) -> ( ( F ` a ) D y ) = ( ( F ` a ) D ( F ` b ) ) )
31 30 eleq1d 
 |-  ( y = ( F ` b ) -> ( ( ( F ` a ) D y ) e. RR <-> ( ( F ` a ) D ( F ` b ) ) e. RR ) )
32 31 ralrn 
 |-  ( F Fn V -> ( A. y e. ran F ( ( F ` a ) D y ) e. RR <-> A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR ) )
33 29 32 syl 
 |-  ( ph -> ( A. y e. ran F ( ( F ` a ) D y ) e. RR <-> A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR ) )
34 forn 
 |-  ( F : V -onto-> B -> ran F = B )
35 12 34 syl 
 |-  ( ph -> ran F = B )
36 35 raleqdv 
 |-  ( ph -> ( A. y e. ran F ( ( F ` a ) D y ) e. RR <-> A. y e. B ( ( F ` a ) D y ) e. RR ) )
37 33 36 bitr3d 
 |-  ( ph -> ( A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR <-> A. y e. B ( ( F ` a ) D y ) e. RR ) )
38 37 ralbidv 
 |-  ( ph -> ( A. a e. V A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR <-> A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR ) )
39 27 38 mpbid 
 |-  ( ph -> A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR )
40 oveq1 
 |-  ( x = ( F ` a ) -> ( x D y ) = ( ( F ` a ) D y ) )
41 40 eleq1d 
 |-  ( x = ( F ` a ) -> ( ( x D y ) e. RR <-> ( ( F ` a ) D y ) e. RR ) )
42 41 ralbidv 
 |-  ( x = ( F ` a ) -> ( A. y e. B ( x D y ) e. RR <-> A. y e. B ( ( F ` a ) D y ) e. RR ) )
43 42 ralrn 
 |-  ( F Fn V -> ( A. x e. ran F A. y e. B ( x D y ) e. RR <-> A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR ) )
44 29 43 syl 
 |-  ( ph -> ( A. x e. ran F A. y e. B ( x D y ) e. RR <-> A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR ) )
45 35 raleqdv 
 |-  ( ph -> ( A. x e. ran F A. y e. B ( x D y ) e. RR <-> A. x e. B A. y e. B ( x D y ) e. RR ) )
46 44 45 bitr3d 
 |-  ( ph -> ( A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR <-> A. x e. B A. y e. B ( x D y ) e. RR ) )
47 39 46 mpbid 
 |-  ( ph -> A. x e. B A. y e. B ( x D y ) e. RR )
48 ffnov 
 |-  ( D : ( B X. B ) --> RR <-> ( D Fn ( B X. B ) /\ A. x e. B A. y e. B ( x D y ) e. RR ) )
49 14 47 48 sylanbrc 
 |-  ( ph -> D : ( B X. B ) --> RR )
50 ismet2 
 |-  ( D e. ( Met ` B ) <-> ( D e. ( *Met ` B ) /\ D : ( B X. B ) --> RR ) )
51 10 49 50 sylanbrc 
 |-  ( ph -> D e. ( Met ` B ) )