Metamath Proof Explorer

Theorem bfp

Description: Banach fixed point theorem, also known as contraction mapping theorem. A contraction on a complete metric space has a unique fixed point. We show existence in the lemmas, and uniqueness here - if F has two fixed points, then the distance between them is less than K times itself, a contradiction. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses bfp.2 
|- ( ph -> D e. ( CMet ` X ) )
bfp.3 
|- ( ph -> X =/= (/) )
bfp.4 
|- ( ph -> K e. RR+ )
bfp.5 
|- ( ph -> K < 1 )
bfp.6 
|- ( ph -> F : X --> X )
bfp.7 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
Assertion bfp 
|- ( ph -> E! z e. X ( F ` z ) = z )

Proof

Step Hyp Ref Expression
1 bfp.2 
 |-  ( ph -> D e. ( CMet ` X ) )
2 bfp.3 
 |-  ( ph -> X =/= (/) )
3 bfp.4 
 |-  ( ph -> K e. RR+ )
4 bfp.5 
 |-  ( ph -> K < 1 )
5 bfp.6 
 |-  ( ph -> F : X --> X )
6 bfp.7 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
7 n0 
 |-  ( X =/= (/) <-> E. w w e. X )
8 2 7 sylib 
 |-  ( ph -> E. w w e. X )
9 1 adantr 
 |-  ( ( ph /\ w e. X ) -> D e. ( CMet ` X ) )
10 2 adantr 
 |-  ( ( ph /\ w e. X ) -> X =/= (/) )
11 3 adantr 
 |-  ( ( ph /\ w e. X ) -> K e. RR+ )
12 4 adantr 
 |-  ( ( ph /\ w e. X ) -> K < 1 )
13 5 adantr 
 |-  ( ( ph /\ w e. X ) -> F : X --> X )
14 6 adantlr 
 |-  ( ( ( ph /\ w e. X ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
15 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
16 simpr 
 |-  ( ( ph /\ w e. X ) -> w e. X )
17 eqid 
 |-  seq 1 ( ( F o. 1st ) , ( NN X. { w } ) ) = seq 1 ( ( F o. 1st ) , ( NN X. { w } ) )
18 9 10 11 12 13 14 15 16 17 bfplem2 
 |-  ( ( ph /\ w e. X ) -> E. z e. X ( F ` z ) = z )
19 8 18 exlimddv 
 |-  ( ph -> E. z e. X ( F ` z ) = z )
20 oveq12 
 |-  ( ( ( F ` x ) = x /\ ( F ` y ) = y ) -> ( ( F ` x ) D ( F ` y ) ) = ( x D y ) )
21 20 adantl 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( F ` x ) D ( F ` y ) ) = ( x D y ) )
22 6 adantr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
23 21 22 eqbrtrrd 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( x D y ) <_ ( K x. ( x D y ) ) )
24 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
25 1 24 syl 
 |-  ( ph -> D e. ( Met ` X ) )
26 25 ad2antrr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> D e. ( Met ` X ) )
27 simplrl 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> x e. X )
28 simplrr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> y e. X )
29 metcl 
 |-  ( ( D e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x D y ) e. RR )
30 26 27 28 29 syl3anc 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( x D y ) e. RR )
31 3 rpred 
 |-  ( ph -> K e. RR )
32 31 ad2antrr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> K e. RR )
33 32 30 remulcld 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( K x. ( x D y ) ) e. RR )
34 30 33 suble0d 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( ( x D y ) - ( K x. ( x D y ) ) ) <_ 0 <-> ( x D y ) <_ ( K x. ( x D y ) ) ) )
35 23 34 mpbird 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( x D y ) - ( K x. ( x D y ) ) ) <_ 0 )
36 1cnd 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> 1 e. CC )
37 32 recnd 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> K e. CC )
38 30 recnd 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( x D y ) e. CC )
39 36 37 38 subdird 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( 1 - K ) x. ( x D y ) ) = ( ( 1 x. ( x D y ) ) - ( K x. ( x D y ) ) ) )
40 38 mullidd 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( 1 x. ( x D y ) ) = ( x D y ) )
41 40 oveq1d 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( 1 x. ( x D y ) ) - ( K x. ( x D y ) ) ) = ( ( x D y ) - ( K x. ( x D y ) ) ) )
42 39 41 eqtrd 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( 1 - K ) x. ( x D y ) ) = ( ( x D y ) - ( K x. ( x D y ) ) ) )
43 1re 
 |-  1 e. RR
44 resubcl 
 |-  ( ( 1 e. RR /\ K e. RR ) -> ( 1 - K ) e. RR )
45 43 31 44 sylancr 
 |-  ( ph -> ( 1 - K ) e. RR )
46 45 ad2antrr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( 1 - K ) e. RR )
47 46 recnd 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( 1 - K ) e. CC )
48 47 mul01d 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( 1 - K ) x. 0 ) = 0 )
49 35 42 48 3brtr4d 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( 1 - K ) x. ( x D y ) ) <_ ( ( 1 - K ) x. 0 ) )
50 0red 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> 0 e. RR )
51 posdif 
 |-  ( ( K e. RR /\ 1 e. RR ) -> ( K < 1 <-> 0 < ( 1 - K ) ) )
52 31 43 51 sylancl 
 |-  ( ph -> ( K < 1 <-> 0 < ( 1 - K ) ) )
53 4 52 mpbid 
 |-  ( ph -> 0 < ( 1 - K ) )
54 53 ad2antrr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> 0 < ( 1 - K ) )
55 lemul2 
 |-  ( ( ( x D y ) e. RR /\ 0 e. RR /\ ( ( 1 - K ) e. RR /\ 0 < ( 1 - K ) ) ) -> ( ( x D y ) <_ 0 <-> ( ( 1 - K ) x. ( x D y ) ) <_ ( ( 1 - K ) x. 0 ) ) )
56 30 50 46 54 55 syl112anc 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( x D y ) <_ 0 <-> ( ( 1 - K ) x. ( x D y ) ) <_ ( ( 1 - K ) x. 0 ) ) )
57 49 56 mpbird 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( x D y ) <_ 0 )
58 metge0 
 |-  ( ( D e. ( Met ` X ) /\ x e. X /\ y e. X ) -> 0 <_ ( x D y ) )
59 26 27 28 58 syl3anc 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> 0 <_ ( x D y ) )
60 0re 
 |-  0 e. RR
61 letri3 
 |-  ( ( ( x D y ) e. RR /\ 0 e. RR ) -> ( ( x D y ) = 0 <-> ( ( x D y ) <_ 0 /\ 0 <_ ( x D y ) ) ) )
62 30 60 61 sylancl 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( x D y ) = 0 <-> ( ( x D y ) <_ 0 /\ 0 <_ ( x D y ) ) ) )
63 57 59 62 mpbir2and 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( x D y ) = 0 )
64 meteq0 
 |-  ( ( D e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( ( x D y ) = 0 <-> x = y ) )
65 26 27 28 64 syl3anc 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> ( ( x D y ) = 0 <-> x = y ) )
66 63 65 mpbid 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X ) ) /\ ( ( F ` x ) = x /\ ( F ` y ) = y ) ) -> x = y )
67 66 ex 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( ( F ` x ) = x /\ ( F ` y ) = y ) -> x = y ) )
68 67 ralrimivva 
 |-  ( ph -> A. x e. X A. y e. X ( ( ( F ` x ) = x /\ ( F ` y ) = y ) -> x = y ) )
69 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
70 id 
 |-  ( x = z -> x = z )
71 69 70 eqeq12d 
 |-  ( x = z -> ( ( F ` x ) = x <-> ( F ` z ) = z ) )
72 71 anbi1d 
 |-  ( x = z -> ( ( ( F ` x ) = x /\ ( F ` y ) = y ) <-> ( ( F ` z ) = z /\ ( F ` y ) = y ) ) )
73 equequ1 
 |-  ( x = z -> ( x = y <-> z = y ) )
74 72 73 imbi12d 
 |-  ( x = z -> ( ( ( ( F ` x ) = x /\ ( F ` y ) = y ) -> x = y ) <-> ( ( ( F ` z ) = z /\ ( F ` y ) = y ) -> z = y ) ) )
75 74 ralbidv 
 |-  ( x = z -> ( A. y e. X ( ( ( F ` x ) = x /\ ( F ` y ) = y ) -> x = y ) <-> A. y e. X ( ( ( F ` z ) = z /\ ( F ` y ) = y ) -> z = y ) ) )
76 75 cbvralvw 
 |-  ( A. x e. X A. y e. X ( ( ( F ` x ) = x /\ ( F ` y ) = y ) -> x = y ) <-> A. z e. X A. y e. X ( ( ( F ` z ) = z /\ ( F ` y ) = y ) -> z = y ) )
77 68 76 sylib 
 |-  ( ph -> A. z e. X A. y e. X ( ( ( F ` z ) = z /\ ( F ` y ) = y ) -> z = y ) )
78 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
79 id 
 |-  ( z = y -> z = y )
80 78 79 eqeq12d 
 |-  ( z = y -> ( ( F ` z ) = z <-> ( F ` y ) = y ) )
81 80 reu4 
 |-  ( E! z e. X ( F ` z ) = z <-> ( E. z e. X ( F ` z ) = z /\ A. z e. X A. y e. X ( ( ( F ` z ) = z /\ ( F ` y ) = y ) -> z = y ) ) )
82 19 77 81 sylanbrc 
 |-  ( ph -> E! z e. X ( F ` z ) = z )