bfplem1

Description: Lemma for bfp . The sequence G , which simply starts from any point in the space and iterates F , satisfies the property that the distance from G ( n ) to G ( n + 1 ) decreases by at least K after each step. Thus, the total distance from any G ( i ) to G ( j ) is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point ( ( ~>tJ )G ) since the space is complete. (Contributed by Jeff Madsen, 17-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)$
	bfp.8	$⊢ J = MetOpen (D)$
	bfp.9	$⊢ φ \to A \in X$
	bfp.10	$⊢ G = seq 1 ((F \circ 1^{st}), (ℕ \times \{A\}))$
Assertion	bfplem1	$⊢ φ \to G \underset{t}{⇝} (J) \underset{t}{⇝} (J) (G)$

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		bfp.8	$⊢ J = MetOpen (D)$
8		bfp.9	$⊢ φ \to A \in X$
9		bfp.10	$⊢ G = seq 1 ((F \circ 1^{st}), (ℕ \times \{A\}))$
10		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
11	1 10	syl	$⊢ φ \to D \in Met (X)$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13		1zzd	$⊢ φ \to 1 \in ℤ$
14	12 9 13 8 5	algrf	$⊢ φ \to G : ℕ ⟶ X$
15	5 8	ffvelrnd	$⊢ φ \to F (A) \in X$
16		metcl	$⊢ (D \in Met (X) \land A \in X \land F (A) \in X) \to A D F (A) \in ℝ$
17	11 8 15 16	syl3anc	$⊢ φ \to A D F (A) \in ℝ$
18	17 3	rerpdivcld	$⊢ φ \to \frac{A D F (A)}{K} \in ℝ$
19		fveq2	$⊢ j = 1 \to G (j) = G (1)$
20		fvoveq1	$⊢ j = 1 \to G (j + 1) = G (1 + 1)$
21	19 20	oveq12d	$⊢ j = 1 \to G (j) D G (j + 1) = G (1) D G (1 + 1)$
22		oveq2	$⊢ j = 1 \to K^{j} = K^{1}$
23	22	oveq2d	$⊢ j = 1 \to (\frac{A D F (A)}{K}) K^{j} = (\frac{A D F (A)}{K}) K^{1}$
24	21 23	breq12d	$⊢ j = 1 \to (G (j) D G (j + 1) \leq (\frac{A D F (A)}{K}) K^{j} \leftrightarrow G (1) D G (1 + 1) \leq (\frac{A D F (A)}{K}) K^{1})$
25	24	imbi2d	$⊢ j = 1 \to ((φ \to G (j) D G (j + 1) \leq (\frac{A D F (A)}{K}) K^{j}) \leftrightarrow (φ \to G (1) D G (1 + 1) \leq (\frac{A D F (A)}{K}) K^{1}))$
26		fveq2	$⊢ j = k \to G (j) = G (k)$
27		fvoveq1	$⊢ j = k \to G (j + 1) = G (k + 1)$
28	26 27	oveq12d	$⊢ j = k \to G (j) D G (j + 1) = G (k) D G (k + 1)$
29		oveq2	$⊢ j = k \to K^{j} = K^{k}$
30	29	oveq2d	$⊢ j = k \to (\frac{A D F (A)}{K}) K^{j} = (\frac{A D F (A)}{K}) K^{k}$
31	28 30	breq12d	$⊢ j = k \to (G (j) D G (j + 1) \leq (\frac{A D F (A)}{K}) K^{j} \leftrightarrow G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k})$
32	31	imbi2d	$⊢ j = k \to ((φ \to G (j) D G (j + 1) \leq (\frac{A D F (A)}{K}) K^{j}) \leftrightarrow (φ \to G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k}))$
33		fveq2	$⊢ j = k + 1 \to G (j) = G (k + 1)$
34		fvoveq1	$⊢ j = k + 1 \to G (j + 1) = G (k + 1 + 1)$
35	33 34	oveq12d	$⊢ j = k + 1 \to G (j) D G (j + 1) = G (k + 1) D G (k + 1 + 1)$
36		oveq2	$⊢ j = k + 1 \to K^{j} = K^{k + 1}$
37	36	oveq2d	$⊢ j = k + 1 \to (\frac{A D F (A)}{K}) K^{j} = (\frac{A D F (A)}{K}) K^{k + 1}$
38	35 37	breq12d	$⊢ j = k + 1 \to (G (j) D G (j + 1) \leq (\frac{A D F (A)}{K}) K^{j} \leftrightarrow G (k + 1) D G (k + 1 + 1) \leq (\frac{A D F (A)}{K}) K^{k + 1})$
39	38	imbi2d	$⊢ j = k + 1 \to ((φ \to G (j) D G (j + 1) \leq (\frac{A D F (A)}{K}) K^{j}) \leftrightarrow (φ \to G (k + 1) D G (k + 1 + 1) \leq (\frac{A D F (A)}{K}) K^{k + 1}))$
40	17	leidd	$⊢ φ \to A D F (A) \leq A D F (A)$
41	12 9 13 8	algr0	$⊢ φ \to G (1) = A$
42		1nn	$⊢ 1 \in ℕ$
43	12 9 13 8 5	algrp1	$⊢ (φ \land 1 \in ℕ) \to G (1 + 1) = F (G (1))$
44	42 43	mpan2	$⊢ φ \to G (1 + 1) = F (G (1))$
45	41	fveq2d	$⊢ φ \to F (G (1)) = F (A)$
46	44 45	eqtrd	$⊢ φ \to G (1 + 1) = F (A)$
47	41 46	oveq12d	$⊢ φ \to G (1) D G (1 + 1) = A D F (A)$
48	3	rpred	$⊢ φ \to K \in ℝ$
49	48	recnd	$⊢ φ \to K \in ℂ$
50	49	exp1d	$⊢ φ \to K^{1} = K$
51	50	oveq2d	$⊢ φ \to (\frac{A D F (A)}{K}) K^{1} = (\frac{A D F (A)}{K}) K$
52	17	recnd	$⊢ φ \to A D F (A) \in ℂ$
53	3	rpne0d	$⊢ φ \to K \neq 0$
54	52 49 53	divcan1d	$⊢ φ \to (\frac{A D F (A)}{K}) K = A D F (A)$
55	51 54	eqtrd	$⊢ φ \to (\frac{A D F (A)}{K}) K^{1} = A D F (A)$
56	40 47 55	3brtr4d	$⊢ φ \to G (1) D G (1 + 1) \leq (\frac{A D F (A)}{K}) K^{1}$
57	14	ffvelrnda	$⊢ (φ \land k \in ℕ) \to G (k) \in X$
58		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
59		ffvelrn	$⊢ (G : ℕ ⟶ X \land k + 1 \in ℕ) \to G (k + 1) \in X$
60	14 58 59	syl2an	$⊢ (φ \land k \in ℕ) \to G (k + 1) \in X$
61	57 60	jca	$⊢ (φ \land k \in ℕ) \to (G (k) \in X \land G (k + 1) \in X)$
62	6	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in X F (x) D F (y) \leq K (x D y)$
63	62	adantr	$⊢ (φ \land k \in ℕ) \to \forall x \in X \forall y \in X F (x) D F (y) \leq K (x D y)$
64		fveq2	$⊢ x = G (k) \to F (x) = F (G (k))$
65	64	oveq1d	$⊢ x = G (k) \to F (x) D F (y) = F (G (k)) D F (y)$
66		oveq1	$⊢ x = G (k) \to x D y = G (k) D y$
67	66	oveq2d	$⊢ x = G (k) \to K (x D y) = K (G (k) D y)$
68	65 67	breq12d	$⊢ x = G (k) \to (F (x) D F (y) \leq K (x D y) \leftrightarrow F (G (k)) D F (y) \leq K (G (k) D y))$
69		fveq2	$⊢ y = G (k + 1) \to F (y) = F (G (k + 1))$
70	69	oveq2d	$⊢ y = G (k + 1) \to F (G (k)) D F (y) = F (G (k)) D F (G (k + 1))$
71		oveq2	$⊢ y = G (k + 1) \to G (k) D y = G (k) D G (k + 1)$
72	71	oveq2d	$⊢ y = G (k + 1) \to K (G (k) D y) = K (G (k) D G (k + 1))$
73	70 72	breq12d	$⊢ y = G (k + 1) \to (F (G (k)) D F (y) \leq K (G (k) D y) \leftrightarrow F (G (k)) D F (G (k + 1)) \leq K (G (k) D G (k + 1)))$
74	68 73	rspc2v	$⊢ (G (k) \in X \land G (k + 1) \in X) \to (\forall x \in X \forall y \in X F (x) D F (y) \leq K (x D y) \to F (G (k)) D F (G (k + 1)) \leq K (G (k) D G (k + 1)))$
75	61 63 74	sylc	$⊢ (φ \land k \in ℕ) \to F (G (k)) D F (G (k + 1)) \leq K (G (k) D G (k + 1))$
76	11	adantr	$⊢ (φ \land k \in ℕ) \to D \in Met (X)$
77	5	adantr	$⊢ (φ \land k \in ℕ) \to F : X ⟶ X$
78	77 57	ffvelrnd	$⊢ (φ \land k \in ℕ) \to F (G (k)) \in X$
79	77 60	ffvelrnd	$⊢ (φ \land k \in ℕ) \to F (G (k + 1)) \in X$
80		metcl	$⊢ (D \in Met (X) \land F (G (k)) \in X \land F (G (k + 1)) \in X) \to F (G (k)) D F (G (k + 1)) \in ℝ$
81	76 78 79 80	syl3anc	$⊢ (φ \land k \in ℕ) \to F (G (k)) D F (G (k + 1)) \in ℝ$
82	48	adantr	$⊢ (φ \land k \in ℕ) \to K \in ℝ$
83		metcl	$⊢ (D \in Met (X) \land G (k) \in X \land G (k + 1) \in X) \to G (k) D G (k + 1) \in ℝ$
84	76 57 60 83	syl3anc	$⊢ (φ \land k \in ℕ) \to G (k) D G (k + 1) \in ℝ$
85	82 84	remulcld	$⊢ (φ \land k \in ℕ) \to K (G (k) D G (k + 1)) \in ℝ$
86	18	adantr	$⊢ (φ \land k \in ℕ) \to \frac{A D F (A)}{K} \in ℝ$
87	58	adantl	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℕ$
88	87	nnnn0d	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℕ_{0}$
89	82 88	reexpcld	$⊢ (φ \land k \in ℕ) \to K^{k + 1} \in ℝ$
90	86 89	remulcld	$⊢ (φ \land k \in ℕ) \to (\frac{A D F (A)}{K}) K^{k + 1} \in ℝ$
91		letr	$⊢ (F (G (k)) D F (G (k + 1)) \in ℝ \land K (G (k) D G (k + 1)) \in ℝ \land (\frac{A D F (A)}{K}) K^{k + 1} \in ℝ) \to ((F (G (k)) D F (G (k + 1)) \leq K (G (k) D G (k + 1)) \land K (G (k) D G (k + 1)) \leq (\frac{A D F (A)}{K}) K^{k + 1}) \to F (G (k)) D F (G (k + 1)) \leq (\frac{A D F (A)}{K}) K^{k + 1})$
92	81 85 90 91	syl3anc	$⊢ (φ \land k \in ℕ) \to ((F (G (k)) D F (G (k + 1)) \leq K (G (k) D G (k + 1)) \land K (G (k) D G (k + 1)) \leq (\frac{A D F (A)}{K}) K^{k + 1}) \to F (G (k)) D F (G (k + 1)) \leq (\frac{A D F (A)}{K}) K^{k + 1})$
93	75 92	mpand	$⊢ (φ \land k \in ℕ) \to (K (G (k) D G (k + 1)) \leq (\frac{A D F (A)}{K}) K^{k + 1} \to F (G (k)) D F (G (k + 1)) \leq (\frac{A D F (A)}{K}) K^{k + 1})$
94		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
95		reexpcl	$⊢ (K \in ℝ \land k \in ℕ_{0}) \to K^{k} \in ℝ$
96	48 94 95	syl2an	$⊢ (φ \land k \in ℕ) \to K^{k} \in ℝ$
97	86 96	remulcld	$⊢ (φ \land k \in ℕ) \to (\frac{A D F (A)}{K}) K^{k} \in ℝ$
98	3	rpgt0d	$⊢ φ \to 0 < K$
99	98	adantr	$⊢ (φ \land k \in ℕ) \to 0 < K$
100		lemul1	$⊢ (G (k) D G (k + 1) \in ℝ \land (\frac{A D F (A)}{K}) K^{k} \in ℝ \land (K \in ℝ \land 0 < K)) \to (G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k} \leftrightarrow (G (k) D G (k + 1)) K \leq (\frac{A D F (A)}{K}) K^{k} K)$
101	84 97 82 99 100	syl112anc	$⊢ (φ \land k \in ℕ) \to (G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k} \leftrightarrow (G (k) D G (k + 1)) K \leq (\frac{A D F (A)}{K}) K^{k} K)$
102	84	recnd	$⊢ (φ \land k \in ℕ) \to G (k) D G (k + 1) \in ℂ$
103	49	adantr	$⊢ (φ \land k \in ℕ) \to K \in ℂ$
104	102 103	mulcomd	$⊢ (φ \land k \in ℕ) \to (G (k) D G (k + 1)) K = K (G (k) D G (k + 1))$
105	86	recnd	$⊢ (φ \land k \in ℕ) \to \frac{A D F (A)}{K} \in ℂ$
106	96	recnd	$⊢ (φ \land k \in ℕ) \to K^{k} \in ℂ$
107	105 106 103	mulassd	$⊢ (φ \land k \in ℕ) \to (\frac{A D F (A)}{K}) K^{k} K = (\frac{A D F (A)}{K}) K^{k} K$
108		expp1	$⊢ (K \in ℂ \land k \in ℕ_{0}) \to K^{k + 1} = K^{k} K$
109	49 94 108	syl2an	$⊢ (φ \land k \in ℕ) \to K^{k + 1} = K^{k} K$
110	109	oveq2d	$⊢ (φ \land k \in ℕ) \to (\frac{A D F (A)}{K}) K^{k + 1} = (\frac{A D F (A)}{K}) K^{k} K$
111	107 110	eqtr4d	$⊢ (φ \land k \in ℕ) \to (\frac{A D F (A)}{K}) K^{k} K = (\frac{A D F (A)}{K}) K^{k + 1}$
112	104 111	breq12d	$⊢ (φ \land k \in ℕ) \to ((G (k) D G (k + 1)) K \leq (\frac{A D F (A)}{K}) K^{k} K \leftrightarrow K (G (k) D G (k + 1)) \leq (\frac{A D F (A)}{K}) K^{k + 1})$
113	101 112	bitrd	$⊢ (φ \land k \in ℕ) \to (G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k} \leftrightarrow K (G (k) D G (k + 1)) \leq (\frac{A D F (A)}{K}) K^{k + 1})$
114	12 9 13 8 5	algrp1	$⊢ (φ \land k \in ℕ) \to G (k + 1) = F (G (k))$
115	12 9 13 8 5	algrp1	$⊢ (φ \land k + 1 \in ℕ) \to G (k + 1 + 1) = F (G (k + 1))$
116	58 115	sylan2	$⊢ (φ \land k \in ℕ) \to G (k + 1 + 1) = F (G (k + 1))$
117	114 116	oveq12d	$⊢ (φ \land k \in ℕ) \to G (k + 1) D G (k + 1 + 1) = F (G (k)) D F (G (k + 1))$
118	117	breq1d	$⊢ (φ \land k \in ℕ) \to (G (k + 1) D G (k + 1 + 1) \leq (\frac{A D F (A)}{K}) K^{k + 1} \leftrightarrow F (G (k)) D F (G (k + 1)) \leq (\frac{A D F (A)}{K}) K^{k + 1})$
119	93 113 118	3imtr4d	$⊢ (φ \land k \in ℕ) \to (G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k} \to G (k + 1) D G (k + 1 + 1) \leq (\frac{A D F (A)}{K}) K^{k + 1})$
120	119	expcom	$⊢ k \in ℕ \to (φ \to (G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k} \to G (k + 1) D G (k + 1 + 1) \leq (\frac{A D F (A)}{K}) K^{k + 1}))$
121	120	a2d	$⊢ k \in ℕ \to ((φ \to G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k}) \to (φ \to G (k + 1) D G (k + 1 + 1) \leq (\frac{A D F (A)}{K}) K^{k + 1}))$
122	25 32 39 32 56 121	nnind	$⊢ k \in ℕ \to (φ \to G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k})$
123	122	impcom	$⊢ (φ \land k \in ℕ) \to G (k) D G (k + 1) \leq (\frac{A D F (A)}{K}) K^{k}$
124	11 14 18 3 4 123	geomcau	$⊢ φ \to G \in Cau (D)$
125	7	cmetcau	$⊢ (D \in CMet (X) \land G \in Cau (D)) \to G \in dom \underset{t}{⇝} (J)$
126	1 124 125	syl2anc	$⊢ φ \to G \in dom \underset{t}{⇝} (J)$
127		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
128	7	methaus	$⊢ D \in ∞Met (X) \to J \in Haus$
129	11 127 128	3syl	$⊢ φ \to J \in Haus$
130		lmfun	$⊢ J \in Haus \to Fun \underset{t}{⇝} (J)$
131		funfvbrb	$⊢ Fun \underset{t}{⇝} (J) \to (G \in dom \underset{t}{⇝} (J) \leftrightarrow G \underset{t}{⇝} (J) \underset{t}{⇝} (J) (G))$
132	129 130 131	3syl	$⊢ φ \to (G \in dom \underset{t}{⇝} (J) \leftrightarrow G \underset{t}{⇝} (J) \underset{t}{⇝} (J) (G))$
133	126 132	mpbid	$⊢ φ \to G \underset{t}{⇝} (J) \underset{t}{⇝} (J) (G)$

Metamath Proof Explorer

Theorem bfplem1

Proof