Metamath Proof Explorer

Theorem cvmliftlem9

Description: Lemma for cvmlift . The Q ( M ) functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the Q functions agree on their common domain. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmliftlem.b ⊢ 𝐵 = ∪ 𝐶
cvmliftlem.x ⊢ 𝑋 = ∪ 𝐽
cvmliftlem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftlem.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
cvmliftlem.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmliftlem.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
cvmliftlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
cvmliftlem.t ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
cvmliftlem.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
cvmliftlem.l ⊢ 𝐿 = ( topGen ‘ ran (,) )
cvmliftlem.q ⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
Assertion cvmliftlem9 ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑀 ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 cvmliftlem.b ⊢ 𝐵 = ∪ 𝐶
3 cvmliftlem.x ⊢ 𝑋 = ∪ 𝐽
4 cvmliftlem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
5 cvmliftlem.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
6 cvmliftlem.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
7 cvmliftlem.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
8 cvmliftlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 cvmliftlem.t ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
10 cvmliftlem.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
11 cvmliftlem.l ⊢ 𝐿 = ( topGen ‘ ran (,) )
12 cvmliftlem.q ⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
13 elfznn ⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → 𝑀 ∈ ℕ )
14 eqid ⊢ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 14 cvmliftlem5 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑧 ∈ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
16 13 15 sylan2 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑧 ∈ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
17 simpr ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 = ( ( 𝑀 − 1 ) / 𝑁 ) ) → 𝑧 = ( ( 𝑀 − 1 ) / 𝑁 ) )
18 17 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 = ( ( 𝑀 − 1 ) / 𝑁 ) ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )
19 18 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 = ( ( 𝑀 − 1 ) / 𝑁 ) ) → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) = ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) )
20 13 adantl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ ℕ )
21 20 nnred ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
22 peano2rem ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 1 ) ∈ ℝ )
23 21 22 syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 − 1 ) ∈ ℝ )
24 8 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ )
25 23 24 nndivred ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ℝ )
26 25 rexrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ℝ* )
27 21 24 nndivred ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
28 27 rexrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 / 𝑁 ) ∈ ℝ* )
29 21 ltm1d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 − 1 ) < 𝑀 )
30 24 nnred ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
31 24 nngt0d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 0 < 𝑁 )
32 ltdiv1 ⊢ ( ( ( 𝑀 − 1 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( ( 𝑀 − 1 ) / 𝑁 ) < ( 𝑀 / 𝑁 ) ) )
33 23 21 30 31 32 syl112anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( ( 𝑀 − 1 ) / 𝑁 ) < ( 𝑀 / 𝑁 ) ) )
34 29 33 mpbid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) < ( 𝑀 / 𝑁 ) )
35 25 27 34 ltled ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ≤ ( 𝑀 / 𝑁 ) )
36 lbicc2 ⊢ ( ( ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ℝ* ∧ ( 𝑀 / 𝑁 ) ∈ ℝ* ∧ ( ( 𝑀 − 1 ) / 𝑁 ) ≤ ( 𝑀 / 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) )
37 26 28 35 36 syl3anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) )
38 fvexd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ∈ V )
39 16 19 37 38 fvmptd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑀 ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) = ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) )
40 4 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
42 1 2 3 4 5 6 7 8 9 10 11 41 cvmliftlem1 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) )
43 1 2 3 4 5 6 7 8 9 10 11 12 14 cvmliftlem7 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) )
44 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
45 2 3 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ 𝑋 )
46 40 44 45 3syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐹 : 𝐵 ⟶ 𝑋 )
47 ffn ⊢ ( 𝐹 : 𝐵 ⟶ 𝑋 → 𝐹 Fn 𝐵 )
48 fniniseg ⊢ ( 𝐹 Fn 𝐵 → ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ↔ ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ) )
49 46 47 48 3syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ↔ ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ) )
50 43 49 mpbid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) )
51 50 simpld ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 )
52 50 simprd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )
53 1 2 3 4 5 6 7 8 9 10 11 41 14 37 cvmliftlem3 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
54 52 53 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
55 eqid ⊢ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) = ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 )
56 1 2 55 cvmsiota ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) → ( ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) )
57 40 42 51 54 56 syl13anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) )
58 57 simprd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) )
59 fvres ⊢ ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) → ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) )
60 58 59 syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) )
61 60 52 eqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )
62 57 simpld ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) )
63 1 cvmsf1o ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ∧ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ) → ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) –1-1-onto→ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
64 40 42 62 63 syl3anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) –1-1-onto→ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
65 f1ocnvfv ⊢ ( ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) –1-1-onto→ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) → ( ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) )
66 64 58 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) )
67 61 66 mpd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )
68 39 67 eqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑀 ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )