# 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 ${⊢}{\phi }\to {D}\in \mathrm{CMet}\left({X}\right)$
bfp.3 ${⊢}{\phi }\to {X}\ne \varnothing$
bfp.4 ${⊢}{\phi }\to {K}\in {ℝ}^{+}$
bfp.5 ${⊢}{\phi }\to {K}<1$
bfp.6 ${⊢}{\phi }\to {F}:{X}⟶{X}$
bfp.7 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}\left({x}\right){D}{F}\left({y}\right)\le {K}\left({x}{D}{y}\right)$
Assertion bfp ${⊢}{\phi }\to \exists !{z}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={z}$

### Proof

Step Hyp Ref Expression
1 bfp.2 ${⊢}{\phi }\to {D}\in \mathrm{CMet}\left({X}\right)$
2 bfp.3 ${⊢}{\phi }\to {X}\ne \varnothing$
3 bfp.4 ${⊢}{\phi }\to {K}\in {ℝ}^{+}$
4 bfp.5 ${⊢}{\phi }\to {K}<1$
5 bfp.6 ${⊢}{\phi }\to {F}:{X}⟶{X}$
6 bfp.7 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}\left({x}\right){D}{F}\left({y}\right)\le {K}\left({x}{D}{y}\right)$
7 n0 ${⊢}{X}\ne \varnothing ↔\exists {w}\phantom{\rule{.4em}{0ex}}{w}\in {X}$
8 2 7 sylib ${⊢}{\phi }\to \exists {w}\phantom{\rule{.4em}{0ex}}{w}\in {X}$
9 1 adantr ${⊢}\left({\phi }\wedge {w}\in {X}\right)\to {D}\in \mathrm{CMet}\left({X}\right)$
10 2 adantr ${⊢}\left({\phi }\wedge {w}\in {X}\right)\to {X}\ne \varnothing$
11 3 adantr ${⊢}\left({\phi }\wedge {w}\in {X}\right)\to {K}\in {ℝ}^{+}$
12 4 adantr ${⊢}\left({\phi }\wedge {w}\in {X}\right)\to {K}<1$
13 5 adantr ${⊢}\left({\phi }\wedge {w}\in {X}\right)\to {F}:{X}⟶{X}$
14 6 adantlr ${⊢}\left(\left({\phi }\wedge {w}\in {X}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}\left({x}\right){D}{F}\left({y}\right)\le {K}\left({x}{D}{y}\right)$
15 eqid ${⊢}\mathrm{MetOpen}\left({D}\right)=\mathrm{MetOpen}\left({D}\right)$
16 simpr ${⊢}\left({\phi }\wedge {w}\in {X}\right)\to {w}\in {X}$
17 eqid ${⊢}seq1\left(\left({F}\circ {1}^{st}\right),\left(ℕ×\left\{{w}\right\}\right)\right)=seq1\left(\left({F}\circ {1}^{st}\right),\left(ℕ×\left\{{w}\right\}\right)\right)$
18 9 10 11 12 13 14 15 16 17 bfplem2 ${⊢}\left({\phi }\wedge {w}\in {X}\right)\to \exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={z}$
19 8 18 exlimddv ${⊢}{\phi }\to \exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={z}$
20 oveq12 ${⊢}\left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\to {F}\left({x}\right){D}{F}\left({y}\right)={x}{D}{y}$
21 20 adantl ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {F}\left({x}\right){D}{F}\left({y}\right)={x}{D}{y}$
22 6 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {F}\left({x}\right){D}{F}\left({y}\right)\le {K}\left({x}{D}{y}\right)$
23 21 22 eqbrtrrd ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {x}{D}{y}\le {K}\left({x}{D}{y}\right)$
24 cmetmet ${⊢}{D}\in \mathrm{CMet}\left({X}\right)\to {D}\in \mathrm{Met}\left({X}\right)$
25 1 24 syl ${⊢}{\phi }\to {D}\in \mathrm{Met}\left({X}\right)$
26 25 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {D}\in \mathrm{Met}\left({X}\right)$
27 simplrl ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {x}\in {X}$
28 simplrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {y}\in {X}$
29 metcl ${⊢}\left({D}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to {x}{D}{y}\in ℝ$
30 26 27 28 29 syl3anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {x}{D}{y}\in ℝ$
31 3 rpred ${⊢}{\phi }\to {K}\in ℝ$
32 31 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {K}\in ℝ$
33 32 30 remulcld ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {K}\left({x}{D}{y}\right)\in ℝ$
34 30 33 suble0d ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to \left(\left({x}{D}{y}\right)-{K}\left({x}{D}{y}\right)\le 0↔{x}{D}{y}\le {K}\left({x}{D}{y}\right)\right)$
35 23 34 mpbird ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to \left({x}{D}{y}\right)-{K}\left({x}{D}{y}\right)\le 0$
36 1cnd ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to 1\in ℂ$
37 32 recnd ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {K}\in ℂ$
38 30 recnd ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {x}{D}{y}\in ℂ$
39 36 37 38 subdird ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to \left(1-{K}\right)\left({x}{D}{y}\right)=1\left({x}{D}{y}\right)-{K}\left({x}{D}{y}\right)$
40 38 mulid2d ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to 1\left({x}{D}{y}\right)={x}{D}{y}$
41 40 oveq1d ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to 1\left({x}{D}{y}\right)-{K}\left({x}{D}{y}\right)=\left({x}{D}{y}\right)-{K}\left({x}{D}{y}\right)$
42 39 41 eqtrd ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to \left(1-{K}\right)\left({x}{D}{y}\right)=\left({x}{D}{y}\right)-{K}\left({x}{D}{y}\right)$
43 1re ${⊢}1\in ℝ$
44 resubcl ${⊢}\left(1\in ℝ\wedge {K}\in ℝ\right)\to 1-{K}\in ℝ$
45 43 31 44 sylancr ${⊢}{\phi }\to 1-{K}\in ℝ$
46 45 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to 1-{K}\in ℝ$
47 46 recnd ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to 1-{K}\in ℂ$
48 47 mul01d ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to \left(1-{K}\right)\cdot 0=0$
49 35 42 48 3brtr4d ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to \left(1-{K}\right)\left({x}{D}{y}\right)\le \left(1-{K}\right)\cdot 0$
50 0red ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to 0\in ℝ$
51 posdif ${⊢}\left({K}\in ℝ\wedge 1\in ℝ\right)\to \left({K}<1↔0<1-{K}\right)$
52 31 43 51 sylancl ${⊢}{\phi }\to \left({K}<1↔0<1-{K}\right)$
53 4 52 mpbid ${⊢}{\phi }\to 0<1-{K}$
54 53 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to 0<1-{K}$
55 lemul2 ${⊢}\left({x}{D}{y}\in ℝ\wedge 0\in ℝ\wedge \left(1-{K}\in ℝ\wedge 0<1-{K}\right)\right)\to \left({x}{D}{y}\le 0↔\left(1-{K}\right)\left({x}{D}{y}\right)\le \left(1-{K}\right)\cdot 0\right)$
56 30 50 46 54 55 syl112anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to \left({x}{D}{y}\le 0↔\left(1-{K}\right)\left({x}{D}{y}\right)\le \left(1-{K}\right)\cdot 0\right)$
57 49 56 mpbird ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {x}{D}{y}\le 0$
58 metge0 ${⊢}\left({D}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to 0\le {x}{D}{y}$
59 26 27 28 58 syl3anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to 0\le {x}{D}{y}$
60 0re ${⊢}0\in ℝ$
61 letri3 ${⊢}\left({x}{D}{y}\in ℝ\wedge 0\in ℝ\right)\to \left({x}{D}{y}=0↔\left({x}{D}{y}\le 0\wedge 0\le {x}{D}{y}\right)\right)$
62 30 60 61 sylancl ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to \left({x}{D}{y}=0↔\left({x}{D}{y}\le 0\wedge 0\le {x}{D}{y}\right)\right)$
63 57 59 62 mpbir2and ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {x}{D}{y}=0$
64 meteq0 ${⊢}\left({D}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to \left({x}{D}{y}=0↔{x}={y}\right)$
65 26 27 28 64 syl3anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to \left({x}{D}{y}=0↔{x}={y}\right)$
66 63 65 mpbid ${⊢}\left(\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\right)\to {x}={y}$
67 66 ex ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left(\left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\to {x}={y}\right)$
68 67 ralrimivva ${⊢}{\phi }\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\to {x}={y}\right)$
69 fveq2 ${⊢}{x}={z}\to {F}\left({x}\right)={F}\left({z}\right)$
70 id ${⊢}{x}={z}\to {x}={z}$
71 69 70 eqeq12d ${⊢}{x}={z}\to \left({F}\left({x}\right)={x}↔{F}\left({z}\right)={z}\right)$
72 71 anbi1d ${⊢}{x}={z}\to \left(\left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)↔\left({F}\left({z}\right)={z}\wedge {F}\left({y}\right)={y}\right)\right)$
73 equequ1 ${⊢}{x}={z}\to \left({x}={y}↔{z}={y}\right)$
74 72 73 imbi12d ${⊢}{x}={z}\to \left(\left(\left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\to {x}={y}\right)↔\left(\left({F}\left({z}\right)={z}\wedge {F}\left({y}\right)={y}\right)\to {z}={y}\right)\right)$
75 74 ralbidv ${⊢}{x}={z}\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\to {x}={y}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({z}\right)={z}\wedge {F}\left({y}\right)={y}\right)\to {z}={y}\right)\right)$
76 75 cbvralvw ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({x}\right)={x}\wedge {F}\left({y}\right)={y}\right)\to {x}={y}\right)↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({z}\right)={z}\wedge {F}\left({y}\right)={y}\right)\to {z}={y}\right)$
77 68 76 sylib ${⊢}{\phi }\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({z}\right)={z}\wedge {F}\left({y}\right)={y}\right)\to {z}={y}\right)$
78 fveq2 ${⊢}{z}={y}\to {F}\left({z}\right)={F}\left({y}\right)$
79 id ${⊢}{z}={y}\to {z}={y}$
80 78 79 eqeq12d ${⊢}{z}={y}\to \left({F}\left({z}\right)={z}↔{F}\left({y}\right)={y}\right)$
81 80 reu4 ${⊢}\exists !{z}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={z}↔\left(\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={z}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({z}\right)={z}\wedge {F}\left({y}\right)={y}\right)\to {z}={y}\right)\right)$
82 19 77 81 sylanbrc ${⊢}{\phi }\to \exists !{z}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={z}$