Metamath Proof Explorer

Theorem 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 ⊒ ( πœ‘ β†’ 𝐷 ∈ ( CMet β€˜ 𝑋 ) )
bfp.3 ⊒ ( πœ‘ β†’ 𝑋 β‰  βˆ… )
bfp.4 ⊒ ( πœ‘ β†’ 𝐾 ∈ ℝ+ )
bfp.5 ⊒ ( πœ‘ β†’ 𝐾 < 1 )
bfp.6 ⊒ ( πœ‘ β†’ 𝐹 : 𝑋 ⟢ 𝑋 )
bfp.7 ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) ≀ ( 𝐾 Β· ( π‘₯ 𝐷 𝑦 ) ) )
bfp.8 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
bfp.9 ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
bfp.10 ⊒ 𝐺 = seq 1 ( ( 𝐹 ∘ 1st ) , ( β„• Γ— { 𝐴 } ) )
Assertion bfplem1 ( πœ‘ β†’ 𝐺 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 bfp.2 ⊒ ( πœ‘ β†’ 𝐷 ∈ ( CMet β€˜ 𝑋 ) )
2 bfp.3 ⊒ ( πœ‘ β†’ 𝑋 β‰  βˆ… )
3 bfp.4 ⊒ ( πœ‘ β†’ 𝐾 ∈ ℝ+ )
4 bfp.5 ⊒ ( πœ‘ β†’ 𝐾 < 1 )
5 bfp.6 ⊒ ( πœ‘ β†’ 𝐹 : 𝑋 ⟢ 𝑋 )
6 bfp.7 ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) ≀ ( 𝐾 Β· ( π‘₯ 𝐷 𝑦 ) ) )
7 bfp.8 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
8 bfp.9 ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
9 bfp.10 ⊒ 𝐺 = seq 1 ( ( 𝐹 ∘ 1st ) , ( β„• Γ— { 𝐴 } ) )
10 cmetmet ⊒ ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
11 1 10 syl ⊒ ( πœ‘ β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
12 nnuz ⊒ β„• = ( β„€β‰₯ β€˜ 1 )
13 1zzd ⊒ ( πœ‘ β†’ 1 ∈ β„€ )
14 12 9 13 8 5 algrf ⊒ ( πœ‘ β†’ 𝐺 : β„• ⟢ 𝑋 )
15 5 8 ffvelcdmd ⊒ ( πœ‘ β†’ ( 𝐹 β€˜ 𝐴 ) ∈ 𝑋 )
16 metcl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐹 β€˜ 𝐴 ) ∈ 𝑋 ) β†’ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) ∈ ℝ )
17 11 8 15 16 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) ∈ ℝ )
18 17 3 rerpdivcld ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) ∈ ℝ )
19 fveq2 ⊒ ( 𝑗 = 1 β†’ ( 𝐺 β€˜ 𝑗 ) = ( 𝐺 β€˜ 1 ) )
20 fvoveq1 ⊒ ( 𝑗 = 1 β†’ ( 𝐺 β€˜ ( 𝑗 + 1 ) ) = ( 𝐺 β€˜ ( 1 + 1 ) ) )
21 19 20 oveq12d ⊒ ( 𝑗 = 1 β†’ ( ( 𝐺 β€˜ 𝑗 ) 𝐷 ( 𝐺 β€˜ ( 𝑗 + 1 ) ) ) = ( ( 𝐺 β€˜ 1 ) 𝐷 ( 𝐺 β€˜ ( 1 + 1 ) ) ) )
22 oveq2 ⊒ ( 𝑗 = 1 β†’ ( 𝐾 ↑ 𝑗 ) = ( 𝐾 ↑ 1 ) )
23 22 oveq2d ⊒ ( 𝑗 = 1 β†’ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 𝑗 ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 1 ) ) )
24 21 23 breq12d ⊒ ( 𝑗 = 1 β†’ ( ( ( 𝐺 β€˜ 𝑗 ) 𝐷 ( 𝐺 β€˜ ( 𝑗 + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 𝑗 ) ) ↔ ( ( 𝐺 β€˜ 1 ) 𝐷 ( 𝐺 β€˜ ( 1 + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 1 ) ) ) )
25 24 imbi2d ⊒ ( 𝑗 = 1 β†’ ( ( πœ‘ β†’ ( ( 𝐺 β€˜ 𝑗 ) 𝐷 ( 𝐺 β€˜ ( 𝑗 + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 𝑗 ) ) ) ↔ ( πœ‘ β†’ ( ( 𝐺 β€˜ 1 ) 𝐷 ( 𝐺 β€˜ ( 1 + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 1 ) ) ) ) )
26 fveq2 ⊒ ( 𝑗 = π‘˜ β†’ ( 𝐺 β€˜ 𝑗 ) = ( 𝐺 β€˜ π‘˜ ) )
27 fvoveq1 ⊒ ( 𝑗 = π‘˜ β†’ ( 𝐺 β€˜ ( 𝑗 + 1 ) ) = ( 𝐺 β€˜ ( π‘˜ + 1 ) ) )
28 26 27 oveq12d ⊒ ( 𝑗 = π‘˜ β†’ ( ( 𝐺 β€˜ 𝑗 ) 𝐷 ( 𝐺 β€˜ ( 𝑗 + 1 ) ) ) = ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) )
29 oveq2 ⊒ ( 𝑗 = π‘˜ β†’ ( 𝐾 ↑ 𝑗 ) = ( 𝐾 ↑ π‘˜ ) )
30 29 oveq2d ⊒ ( 𝑗 = π‘˜ β†’ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 𝑗 ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) )
31 28 30 breq12d ⊒ ( 𝑗 = π‘˜ β†’ ( ( ( 𝐺 β€˜ 𝑗 ) 𝐷 ( 𝐺 β€˜ ( 𝑗 + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 𝑗 ) ) ↔ ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) ) )
32 31 imbi2d ⊒ ( 𝑗 = π‘˜ β†’ ( ( πœ‘ β†’ ( ( 𝐺 β€˜ 𝑗 ) 𝐷 ( 𝐺 β€˜ ( 𝑗 + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 𝑗 ) ) ) ↔ ( πœ‘ β†’ ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) ) ) )
33 fveq2 ⊒ ( 𝑗 = ( π‘˜ + 1 ) β†’ ( 𝐺 β€˜ 𝑗 ) = ( 𝐺 β€˜ ( π‘˜ + 1 ) ) )
34 fvoveq1 ⊒ ( 𝑗 = ( π‘˜ + 1 ) β†’ ( 𝐺 β€˜ ( 𝑗 + 1 ) ) = ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) )
35 33 34 oveq12d ⊒ ( 𝑗 = ( π‘˜ + 1 ) β†’ ( ( 𝐺 β€˜ 𝑗 ) 𝐷 ( 𝐺 β€˜ ( 𝑗 + 1 ) ) ) = ( ( 𝐺 β€˜ ( π‘˜ + 1 ) ) 𝐷 ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) ) )
36 oveq2 ⊒ ( 𝑗 = ( π‘˜ + 1 ) β†’ ( 𝐾 ↑ 𝑗 ) = ( 𝐾 ↑ ( π‘˜ + 1 ) ) )
37 36 oveq2d ⊒ ( 𝑗 = ( π‘˜ + 1 ) β†’ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 𝑗 ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) )
38 35 37 breq12d ⊒ ( 𝑗 = ( π‘˜ + 1 ) β†’ ( ( ( 𝐺 β€˜ 𝑗 ) 𝐷 ( 𝐺 β€˜ ( 𝑗 + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 𝑗 ) ) ↔ ( ( 𝐺 β€˜ ( π‘˜ + 1 ) ) 𝐷 ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) )
39 38 imbi2d ⊒ ( 𝑗 = ( π‘˜ + 1 ) β†’ ( ( πœ‘ β†’ ( ( 𝐺 β€˜ 𝑗 ) 𝐷 ( 𝐺 β€˜ ( 𝑗 + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 𝑗 ) ) ) ↔ ( πœ‘ β†’ ( ( 𝐺 β€˜ ( π‘˜ + 1 ) ) 𝐷 ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) ) )
40 17 leidd ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) ≀ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) )
41 12 9 13 8 algr0 ⊒ ( πœ‘ β†’ ( 𝐺 β€˜ 1 ) = 𝐴 )
42 1nn ⊒ 1 ∈ β„•
43 12 9 13 8 5 algrp1 ⊒ ( ( πœ‘ ∧ 1 ∈ β„• ) β†’ ( 𝐺 β€˜ ( 1 + 1 ) ) = ( 𝐹 β€˜ ( 𝐺 β€˜ 1 ) ) )
44 42 43 mpan2 ⊒ ( πœ‘ β†’ ( 𝐺 β€˜ ( 1 + 1 ) ) = ( 𝐹 β€˜ ( 𝐺 β€˜ 1 ) ) )
45 41 fveq2d ⊒ ( πœ‘ β†’ ( 𝐹 β€˜ ( 𝐺 β€˜ 1 ) ) = ( 𝐹 β€˜ 𝐴 ) )
46 44 45 eqtrd ⊒ ( πœ‘ β†’ ( 𝐺 β€˜ ( 1 + 1 ) ) = ( 𝐹 β€˜ 𝐴 ) )
47 41 46 oveq12d ⊒ ( πœ‘ β†’ ( ( 𝐺 β€˜ 1 ) 𝐷 ( 𝐺 β€˜ ( 1 + 1 ) ) ) = ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) )
48 3 rpred ⊒ ( πœ‘ β†’ 𝐾 ∈ ℝ )
49 48 recnd ⊒ ( πœ‘ β†’ 𝐾 ∈ β„‚ )
50 49 exp1d ⊒ ( πœ‘ β†’ ( 𝐾 ↑ 1 ) = 𝐾 )
51 50 oveq2d ⊒ ( πœ‘ β†’ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 1 ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· 𝐾 ) )
52 17 recnd ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) ∈ β„‚ )
53 3 rpne0d ⊒ ( πœ‘ β†’ 𝐾 β‰  0 )
54 52 49 53 divcan1d ⊒ ( πœ‘ β†’ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· 𝐾 ) = ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) )
55 51 54 eqtrd ⊒ ( πœ‘ β†’ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 1 ) ) = ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) )
56 40 47 55 3brtr4d ⊒ ( πœ‘ β†’ ( ( 𝐺 β€˜ 1 ) 𝐷 ( 𝐺 β€˜ ( 1 + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ 1 ) ) )
57 14 ffvelcdmda ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐺 β€˜ π‘˜ ) ∈ 𝑋 )
58 peano2nn ⊒ ( π‘˜ ∈ β„• β†’ ( π‘˜ + 1 ) ∈ β„• )
59 ffvelcdm ⊒ ( ( 𝐺 : β„• ⟢ 𝑋 ∧ ( π‘˜ + 1 ) ∈ β„• ) β†’ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ∈ 𝑋 )
60 14 58 59 syl2an ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ∈ 𝑋 )
61 57 60 jca ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐺 β€˜ π‘˜ ) ∈ 𝑋 ∧ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ∈ 𝑋 ) )
62 6 ralrimivva ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) ≀ ( 𝐾 Β· ( π‘₯ 𝐷 𝑦 ) ) )
63 62 adantr ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) ≀ ( 𝐾 Β· ( π‘₯ 𝐷 𝑦 ) ) )
64 fveq2 ⊒ ( π‘₯ = ( 𝐺 β€˜ π‘˜ ) β†’ ( 𝐹 β€˜ π‘₯ ) = ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) )
65 64 oveq1d ⊒ ( π‘₯ = ( 𝐺 β€˜ π‘˜ ) β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) = ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) )
66 oveq1 ⊒ ( π‘₯ = ( 𝐺 β€˜ π‘˜ ) β†’ ( π‘₯ 𝐷 𝑦 ) = ( ( 𝐺 β€˜ π‘˜ ) 𝐷 𝑦 ) )
67 66 oveq2d ⊒ ( π‘₯ = ( 𝐺 β€˜ π‘˜ ) β†’ ( 𝐾 Β· ( π‘₯ 𝐷 𝑦 ) ) = ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 𝑦 ) ) )
68 65 67 breq12d ⊒ ( π‘₯ = ( 𝐺 β€˜ π‘˜ ) β†’ ( ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) ≀ ( 𝐾 Β· ( π‘₯ 𝐷 𝑦 ) ) ↔ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) ≀ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 𝑦 ) ) ) )
69 fveq2 ⊒ ( 𝑦 = ( 𝐺 β€˜ ( π‘˜ + 1 ) ) β†’ ( 𝐹 β€˜ 𝑦 ) = ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) )
70 69 oveq2d ⊒ ( 𝑦 = ( 𝐺 β€˜ ( π‘˜ + 1 ) ) β†’ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) = ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) )
71 oveq2 ⊒ ( 𝑦 = ( 𝐺 β€˜ ( π‘˜ + 1 ) ) β†’ ( ( 𝐺 β€˜ π‘˜ ) 𝐷 𝑦 ) = ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) )
72 71 oveq2d ⊒ ( 𝑦 = ( 𝐺 β€˜ ( π‘˜ + 1 ) ) β†’ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 𝑦 ) ) = ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) )
73 70 72 breq12d ⊒ ( 𝑦 = ( 𝐺 β€˜ ( π‘˜ + 1 ) ) β†’ ( ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) ≀ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 𝑦 ) ) ↔ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ) )
74 68 73 rspc2v ⊒ ( ( ( 𝐺 β€˜ π‘˜ ) ∈ 𝑋 ∧ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ∈ 𝑋 ) β†’ ( βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) ≀ ( 𝐾 Β· ( π‘₯ 𝐷 𝑦 ) ) β†’ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ) )
75 61 63 74 sylc ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) )
76 11 adantr ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
77 5 adantr ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ 𝐹 : 𝑋 ⟢ 𝑋 )
78 77 57 ffvelcdmd ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) ∈ 𝑋 )
79 77 60 ffvelcdmd ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ∈ 𝑋 )
80 metcl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) ∈ 𝑋 ∧ ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ∈ 𝑋 ) β†’ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ∈ ℝ )
81 76 78 79 80 syl3anc ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ∈ ℝ )
82 48 adantr ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ 𝐾 ∈ ℝ )
83 metcl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ ( 𝐺 β€˜ π‘˜ ) ∈ 𝑋 ∧ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ∈ 𝑋 ) β†’ ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ∈ ℝ )
84 76 57 60 83 syl3anc ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ∈ ℝ )
85 82 84 remulcld ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ∈ ℝ )
86 18 adantr ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) ∈ ℝ )
87 58 adantl ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( π‘˜ + 1 ) ∈ β„• )
88 87 nnnn0d ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( π‘˜ + 1 ) ∈ β„•0 )
89 82 88 reexpcld ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐾 ↑ ( π‘˜ + 1 ) ) ∈ ℝ )
90 86 89 remulcld ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ∈ ℝ )
91 letr ⊒ ( ( ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ∈ ℝ ∧ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ∈ ℝ ∧ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ∈ ℝ ) β†’ ( ( ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ∧ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) β†’ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) )
92 81 85 90 91 syl3anc ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ∧ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) β†’ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) )
93 75 92 mpand ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) β†’ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) )
94 nnnn0 ⊒ ( π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0 )
95 reexpcl ⊒ ( ( 𝐾 ∈ ℝ ∧ π‘˜ ∈ β„•0 ) β†’ ( 𝐾 ↑ π‘˜ ) ∈ ℝ )
96 48 94 95 syl2an ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐾 ↑ π‘˜ ) ∈ ℝ )
97 86 96 remulcld ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) ∈ ℝ )
98 3 rpgt0d ⊒ ( πœ‘ β†’ 0 < 𝐾 )
99 98 adantr ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ 0 < 𝐾 )
100 lemul1 ⊒ ( ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ∈ ℝ ∧ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) ∈ ℝ ∧ ( 𝐾 ∈ ℝ ∧ 0 < 𝐾 ) ) β†’ ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) ↔ ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) Β· 𝐾 ) ≀ ( ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) Β· 𝐾 ) ) )
101 84 97 82 99 100 syl112anc ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) ↔ ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) Β· 𝐾 ) ≀ ( ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) Β· 𝐾 ) ) )
102 84 recnd ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ∈ β„‚ )
103 49 adantr ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ 𝐾 ∈ β„‚ )
104 102 103 mulcomd ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) Β· 𝐾 ) = ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) )
105 86 recnd ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) ∈ β„‚ )
106 96 recnd ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐾 ↑ π‘˜ ) ∈ β„‚ )
107 105 106 103 mulassd ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) Β· 𝐾 ) = ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( ( 𝐾 ↑ π‘˜ ) Β· 𝐾 ) ) )
108 expp1 ⊒ ( ( 𝐾 ∈ β„‚ ∧ π‘˜ ∈ β„•0 ) β†’ ( 𝐾 ↑ ( π‘˜ + 1 ) ) = ( ( 𝐾 ↑ π‘˜ ) Β· 𝐾 ) )
109 49 94 108 syl2an ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐾 ↑ ( π‘˜ + 1 ) ) = ( ( 𝐾 ↑ π‘˜ ) Β· 𝐾 ) )
110 109 oveq2d ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( ( 𝐾 ↑ π‘˜ ) Β· 𝐾 ) ) )
111 107 110 eqtr4d ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) Β· 𝐾 ) = ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) )
112 104 111 breq12d ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) Β· 𝐾 ) ≀ ( ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) Β· 𝐾 ) ↔ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) )
113 101 112 bitrd ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) ↔ ( 𝐾 Β· ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) )
114 12 9 13 8 5 algrp1 ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) = ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) )
115 12 9 13 8 5 algrp1 ⊒ ( ( πœ‘ ∧ ( π‘˜ + 1 ) ∈ β„• ) β†’ ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) = ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) )
116 58 115 sylan2 ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) = ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) )
117 114 116 oveq12d ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐺 β€˜ ( π‘˜ + 1 ) ) 𝐷 ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) ) = ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) )
118 117 breq1d ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝐺 β€˜ ( π‘˜ + 1 ) ) 𝐷 ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ↔ ( ( 𝐹 β€˜ ( 𝐺 β€˜ π‘˜ ) ) 𝐷 ( 𝐹 β€˜ ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) )
119 93 113 118 3imtr4d ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) β†’ ( ( 𝐺 β€˜ ( π‘˜ + 1 ) ) 𝐷 ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) )
120 119 expcom ⊒ ( π‘˜ ∈ β„• β†’ ( πœ‘ β†’ ( ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) β†’ ( ( 𝐺 β€˜ ( π‘˜ + 1 ) ) 𝐷 ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) ) )
121 120 a2d ⊒ ( π‘˜ ∈ β„• β†’ ( ( πœ‘ β†’ ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) ) β†’ ( πœ‘ β†’ ( ( 𝐺 β€˜ ( π‘˜ + 1 ) ) 𝐷 ( 𝐺 β€˜ ( ( π‘˜ + 1 ) + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ ( π‘˜ + 1 ) ) ) ) ) )
122 25 32 39 32 56 121 nnind ⊒ ( π‘˜ ∈ β„• β†’ ( πœ‘ β†’ ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) ) )
123 122 impcom ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐺 β€˜ π‘˜ ) 𝐷 ( 𝐺 β€˜ ( π‘˜ + 1 ) ) ) ≀ ( ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝐴 ) ) / 𝐾 ) Β· ( 𝐾 ↑ π‘˜ ) ) )
124 11 14 18 3 4 123 geomcau ⊒ ( πœ‘ β†’ 𝐺 ∈ ( Cau β€˜ 𝐷 ) )
125 7 cmetcau ⊒ ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝐺 ∈ ( Cau β€˜ 𝐷 ) ) β†’ 𝐺 ∈ dom ( ⇝𝑑 β€˜ 𝐽 ) )
126 1 124 125 syl2anc ⊒ ( πœ‘ β†’ 𝐺 ∈ dom ( ⇝𝑑 β€˜ 𝐽 ) )
127 metxmet ⊒ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
128 7 methaus ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ Haus )
129 11 127 128 3syl ⊒ ( πœ‘ β†’ 𝐽 ∈ Haus )
130 lmfun ⊒ ( 𝐽 ∈ Haus β†’ Fun ( ⇝𝑑 β€˜ 𝐽 ) )
131 funfvbrb ⊒ ( Fun ( ⇝𝑑 β€˜ 𝐽 ) β†’ ( 𝐺 ∈ dom ( ⇝𝑑 β€˜ 𝐽 ) ↔ 𝐺 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐺 ) ) )
132 129 130 131 3syl ⊒ ( πœ‘ β†’ ( 𝐺 ∈ dom ( ⇝𝑑 β€˜ 𝐽 ) ↔ 𝐺 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐺 ) ) )
133 126 132 mpbid ⊒ ( πœ‘ β†’ 𝐺 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐺 ) )