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	$⊢ φ \to D \in CMet (X)$
	bfp.3	$⊢ φ \to X \neq \emptyset$
	bfp.4	$⊢ φ \to K \in ℝ^{+}$
	bfp.5	$⊢ φ \to K < 1$
	bfp.6	$⊢ φ \to F : X ⟶ X$
	bfp.7	$⊢ (φ \land (x \in X \land y \in X)) \to F (x) D F (y) \leq K (x D y)$
Assertion	bfp	$⊢ φ \to \exists! z \in X F (z) = z$

Proof

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

Metamath Proof Explorer

Theorem bfp

Proof