Metamath Proof Explorer

Theorem stoweidlem20

Description: If a set A of real functions from a common domain T is closed under the sum of two functions, then it is closed under the sum of a finite number of functions, indexed by G. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem20.1 ⊢ Ⅎ 𝑡 𝜑
stoweidlem20.2 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
stoweidlem20.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
stoweidlem20.4 ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
stoweidlem20.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem20.6 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
Assertion stoweidlem20 ( 𝜑 → 𝐹 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 stoweidlem20.1 ⊢ Ⅎ 𝑡 𝜑
2 stoweidlem20.2 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
3 stoweidlem20.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 stoweidlem20.4 ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
5 stoweidlem20.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
6 stoweidlem20.6 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
7 3 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
8 7 leidd ⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
9 8 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝑀 ≤ 𝑀 ) )
10 eleq1 ⊢ ( 𝑛 = 𝑀 → ( 𝑛 ∈ ℕ ↔ 𝑀 ∈ ℕ ) )
11 breq1 ⊢ ( 𝑛 = 𝑀 → ( 𝑛 ≤ 𝑀 ↔ 𝑀 ≤ 𝑀 ) )
12 11 anbi2d ⊢ ( 𝑛 = 𝑀 → ( ( 𝜑 ∧ 𝑛 ≤ 𝑀 ) ↔ ( 𝜑 ∧ 𝑀 ≤ 𝑀 ) ) )
13 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 1 ... 𝑛 ) = ( 1 ... 𝑀 ) )
14 13 sumeq1d ⊢ ( 𝑛 = 𝑀 → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
15 14 mpteq2dv ⊢ ( 𝑛 = 𝑀 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
16 15 eleq1d ⊢ ( 𝑛 = 𝑀 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) )
17 12 16 imbi12d ⊢ ( 𝑛 = 𝑀 → ( ( ( 𝜑 ∧ 𝑛 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑀 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) )
18 10 17 imbi12d ⊢ ( 𝑛 = 𝑀 → ( ( 𝑛 ∈ ℕ → ( ( 𝜑 ∧ 𝑛 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) ↔ ( 𝑀 ∈ ℕ → ( ( 𝜑 ∧ 𝑀 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) ) )
19 breq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ≤ 𝑀 ↔ 1 ≤ 𝑀 ) )
20 19 anbi2d ⊢ ( 𝑥 = 1 → ( ( 𝜑 ∧ 𝑥 ≤ 𝑀 ) ↔ ( 𝜑 ∧ 1 ≤ 𝑀 ) ) )
21 oveq2 ⊢ ( 𝑥 = 1 → ( 1 ... 𝑥 ) = ( 1 ... 1 ) )
22 21 sumeq1d ⊢ ( 𝑥 = 1 → Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
23 22 mpteq2dv ⊢ ( 𝑥 = 1 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
24 23 eleq1d ⊢ ( 𝑥 = 1 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) )
25 20 24 imbi12d ⊢ ( 𝑥 = 1 → ( ( ( 𝜑 ∧ 𝑥 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 1 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) )
26 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ 𝑀 ↔ 𝑦 ≤ 𝑀 ) )
27 26 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ≤ 𝑀 ) ↔ ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) ) )
28 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 1 ... 𝑥 ) = ( 1 ... 𝑦 ) )
29 28 sumeq1d ⊢ ( 𝑥 = 𝑦 → Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
30 29 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
31 30 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) )
32 27 31 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) )
33 breq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ≤ 𝑀 ↔ ( 𝑦 + 1 ) ≤ 𝑀 ) )
34 33 anbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝜑 ∧ 𝑥 ≤ 𝑀 ) ↔ ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ) )
35 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 1 ... 𝑥 ) = ( 1 ... ( 𝑦 + 1 ) ) )
36 35 sumeq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
37 36 mpteq2dv ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
38 37 eleq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) )
39 34 38 imbi12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝜑 ∧ 𝑥 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) )
40 breq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ≤ 𝑀 ↔ 𝑛 ≤ 𝑀 ) )
41 40 anbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 ∧ 𝑥 ≤ 𝑀 ) ↔ ( 𝜑 ∧ 𝑛 ≤ 𝑀 ) ) )
42 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 1 ... 𝑥 ) = ( 1 ... 𝑛 ) )
43 42 sumeq1d ⊢ ( 𝑥 = 𝑛 → Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
44 43 mpteq2dv ⊢ ( 𝑥 = 𝑛 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
45 44 eleq1d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) )
46 41 45 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝜑 ∧ 𝑥 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑛 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) )
47 1z ⊢ 1 ∈ ℤ
48 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
49 3 48 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
50 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑀 ) )
51 49 50 syl ⊢ ( 𝜑 → 1 ∈ ( 1 ... 𝑀 ) )
52 4 51 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ 𝐴 )
53 52 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ ( 𝐺 ‘ 1 ) ∈ 𝐴 ) )
54 eleq1 ⊢ ( 𝑓 = ( 𝐺 ‘ 1 ) → ( 𝑓 ∈ 𝐴 ↔ ( 𝐺 ‘ 1 ) ∈ 𝐴 ) )
55 54 anbi2d ⊢ ( 𝑓 = ( 𝐺 ‘ 1 ) → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝐺 ‘ 1 ) ∈ 𝐴 ) ) )
56 feq1 ⊢ ( 𝑓 = ( 𝐺 ‘ 1 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝐺 ‘ 1 ) : 𝑇 ⟶ ℝ ) )
57 55 56 imbi12d ⊢ ( 𝑓 = ( 𝐺 ‘ 1 ) → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝐺 ‘ 1 ) ∈ 𝐴 ) → ( 𝐺 ‘ 1 ) : 𝑇 ⟶ ℝ ) ) )
58 57 6 vtoclg ⊢ ( ( 𝐺 ‘ 1 ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝐺 ‘ 1 ) ∈ 𝐴 ) → ( 𝐺 ‘ 1 ) : 𝑇 ⟶ ℝ ) )
59 52 53 58 sylc ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) : 𝑇 ⟶ ℝ )
60 59 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 1 ) ‘ 𝑡 ) ∈ ℝ )
61 60 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 1 ) ‘ 𝑡 ) ∈ ℂ )
62 fveq2 ⊢ ( 𝑖 = 1 → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 1 ) )
63 62 fveq1d ⊢ ( 𝑖 = 1 → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝐺 ‘ 1 ) ‘ 𝑡 ) )
64 63 fsum1 ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝐺 ‘ 1 ) ‘ 𝑡 ) ∈ ℂ ) → Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝐺 ‘ 1 ) ‘ 𝑡 ) )
65 47 61 64 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝐺 ‘ 1 ) ‘ 𝑡 ) )
66 1 65 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 1 ) ‘ 𝑡 ) ) )
67 59 feqmptd ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 1 ) ‘ 𝑡 ) ) )
68 66 67 eqtr4d ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝐺 ‘ 1 ) )
69 68 52 eqeltrd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 )
70 69 adantr ⊢ ( ( 𝜑 ∧ 1 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 )
71 simprl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) ∧ ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ) → 𝜑 )
72 simpll ⊢ ( ( ( 𝑦 ∈ ℕ ∧ ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) ∧ ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ) → 𝑦 ∈ ℕ )
73 simprr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) ∧ ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ) → ( 𝑦 + 1 ) ≤ 𝑀 )
74 simp1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 𝜑 )
75 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
76 75 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 𝑦 ∈ ℝ )
77 1red ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 1 ∈ ℝ )
78 76 77 readdcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝑦 + 1 ) ∈ ℝ )
79 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 𝑀 ∈ ℕ )
80 79 nnred ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 𝑀 ∈ ℝ )
81 76 lep1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 𝑦 ≤ ( 𝑦 + 1 ) )
82 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝑦 + 1 ) ≤ 𝑀 )
83 76 78 80 81 82 letrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 𝑦 ≤ 𝑀 )
84 74 83 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) )
85 71 72 73 84 syl3anc ⊢ ( ( ( 𝑦 ∈ ℕ ∧ ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) ∧ ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ) → ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) )
86 simplr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) ∧ ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ) → ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) )
87 85 86 mpd ⊢ ( ( ( 𝑦 ∈ ℕ ∧ ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) ∧ ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 )
88 nfv ⊢ Ⅎ 𝑡 𝑦 ∈ ℕ
89 nfv ⊢ Ⅎ 𝑡 ( 𝑦 + 1 ) ≤ 𝑀
90 1 88 89 nf3an ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 )
91 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑦 ∈ ℕ )
92 91 48 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
93 simpll1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝜑 )
94 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 1 ∈ ℤ )
95 3 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
96 95 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 𝑀 ∈ ℤ )
97 96 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝑀 ∈ ℤ )
98 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) → 𝑖 ∈ ℤ )
99 98 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝑖 ∈ ℤ )
100 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) → 1 ≤ 𝑖 )
101 100 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 1 ≤ 𝑖 )
102 98 zred ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) → 𝑖 ∈ ℝ )
103 102 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝑖 ∈ ℝ )
104 78 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → ( 𝑦 + 1 ) ∈ ℝ )
105 80 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝑀 ∈ ℝ )
106 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) → 𝑖 ≤ ( 𝑦 + 1 ) )
107 106 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝑖 ≤ ( 𝑦 + 1 ) )
108 simpll3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → ( 𝑦 + 1 ) ≤ 𝑀 )
109 103 104 105 107 108 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝑖 ≤ 𝑀 )
110 94 97 99 101 109 elfzd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
111 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝑡 ∈ 𝑇 )
112 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 )
113 112 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 )
114 simp1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → 𝜑 )
115 114 113 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝜑 ∧ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) )
116 eleq1 ⊢ ( 𝑓 = ( 𝐺 ‘ 𝑖 ) → ( 𝑓 ∈ 𝐴 ↔ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) )
117 116 anbi2d ⊢ ( 𝑓 = ( 𝐺 ‘ 𝑖 ) → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) ) )
118 feq1 ⊢ ( 𝑓 = ( 𝐺 ‘ 𝑖 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
119 117 118 imbi12d ⊢ ( 𝑓 = ( 𝐺 ‘ 𝑖 ) → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) ) )
120 119 6 vtoclg ⊢ ( ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
121 113 115 120 sylc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
122 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
123 121 122 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
124 123 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℂ )
125 93 110 111 124 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℂ )
126 fveq2 ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ ( 𝑦 + 1 ) ) )
127 126 fveq1d ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) )
128 92 125 127 fsump1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) )
129 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
130 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( 1 ... 𝑦 ) ∈ Fin )
131 simpll1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝜑 )
132 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 1 ∈ ℤ )
133 96 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑀 ∈ ℤ )
134 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... 𝑦 ) → 𝑖 ∈ ℤ )
135 134 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑖 ∈ ℤ )
136 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... 𝑦 ) → 1 ≤ 𝑖 )
137 136 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 1 ≤ 𝑖 )
138 134 zred ⊢ ( 𝑖 ∈ ( 1 ... 𝑦 ) → 𝑖 ∈ ℝ )
139 138 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑖 ∈ ℝ )
140 78 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → ( 𝑦 + 1 ) ∈ ℝ )
141 80 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑀 ∈ ℝ )
142 76 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑦 ∈ ℝ )
143 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑦 ) → 𝑖 ≤ 𝑦 )
144 143 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑖 ≤ 𝑦 )
145 letrp1 ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑖 ≤ 𝑦 ) → 𝑖 ≤ ( 𝑦 + 1 ) )
146 139 142 144 145 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑖 ≤ ( 𝑦 + 1 ) )
147 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → ( 𝑦 + 1 ) ≤ 𝑀 )
148 139 140 141 146 147 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑖 ≤ 𝑀 )
149 148 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑖 ≤ 𝑀 )
150 132 133 135 137 149 elfzd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
151 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → 𝑡 ∈ 𝑇 )
152 131 150 151 123 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑦 ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
153 130 152 fsumrecl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
154 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
155 154 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
156 129 153 155 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
157 156 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) )
158 128 157 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) )
159 90 158 mpteq2da ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ) )
160 159 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ) )
161 1zzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 1 ∈ ℤ )
162 peano2nn ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ )
163 162 nnzd ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℤ )
164 163 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝑦 + 1 ) ∈ ℤ )
165 162 nnge1d ⊢ ( 𝑦 ∈ ℕ → 1 ≤ ( 𝑦 + 1 ) )
166 165 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → 1 ≤ ( 𝑦 + 1 ) )
167 161 96 164 166 82 elfzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝑦 + 1 ) ∈ ( 1 ... 𝑀 ) )
168 4 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 𝑦 + 1 ) ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ ( 𝑦 + 1 ) ) ∈ 𝐴 )
169 74 167 168 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝐺 ‘ ( 𝑦 + 1 ) ) ∈ 𝐴 )
170 eleq1 ⊢ ( 𝑓 = ( 𝐺 ‘ ( 𝑦 + 1 ) ) → ( 𝑓 ∈ 𝐴 ↔ ( 𝐺 ‘ ( 𝑦 + 1 ) ) ∈ 𝐴 ) )
171 170 anbi2d ⊢ ( 𝑓 = ( 𝐺 ‘ ( 𝑦 + 1 ) ) → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝐺 ‘ ( 𝑦 + 1 ) ) ∈ 𝐴 ) ) )
172 feq1 ⊢ ( 𝑓 = ( 𝐺 ‘ ( 𝑦 + 1 ) ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝐺 ‘ ( 𝑦 + 1 ) ) : 𝑇 ⟶ ℝ ) )
173 171 172 imbi12d ⊢ ( 𝑓 = ( 𝐺 ‘ ( 𝑦 + 1 ) ) → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝐺 ‘ ( 𝑦 + 1 ) ) ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝑦 + 1 ) ) : 𝑇 ⟶ ℝ ) ) )
174 173 6 vtoclg ⊢ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝐺 ‘ ( 𝑦 + 1 ) ) ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝑦 + 1 ) ) : 𝑇 ⟶ ℝ ) )
175 174 anabsi7 ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ ( 𝑦 + 1 ) ) ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝑦 + 1 ) ) : 𝑇 ⟶ ℝ )
176 74 169 175 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝐺 ‘ ( 𝑦 + 1 ) ) : 𝑇 ⟶ ℝ )
177 176 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ∈ ℝ )
178 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) )
179 178 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ∈ ℝ ) → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ‘ 𝑡 ) = ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) )
180 129 177 179 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ‘ 𝑡 ) = ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) )
181 180 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ‘ 𝑡 ) ) = ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) )
182 90 181 mpteq2da ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ) )
183 182 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ) )
184 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → 𝜑 )
185 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 )
186 167 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( 𝑦 + 1 ) ∈ ( 1 ... 𝑀 ) )
187 175 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ ( 𝑦 + 1 ) ) ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝑦 + 1 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) )
188 168 187 syldan ⊢ ( ( 𝜑 ∧ ( 𝑦 + 1 ) ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ ( 𝑦 + 1 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) )
189 188 168 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑦 + 1 ) ∈ ( 1 ... 𝑀 ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ∈ 𝐴 )
190 184 186 189 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ∈ 𝐴 )
191 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
192 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) )
193 5 191 192 stoweidlem8 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
194 184 185 190 193 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
195 183 194 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ‘ 𝑡 ) + ( ( 𝐺 ‘ ( 𝑦 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
196 160 195 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 )
197 71 72 73 87 196 syl31anc ⊢ ( ( ( 𝑦 ∈ ℕ ∧ ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) ∧ ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 )
198 197 exp31 ⊢ ( 𝑦 ∈ ℕ → ( ( ( 𝜑 ∧ 𝑦 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑦 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) → ( ( 𝜑 ∧ ( 𝑦 + 1 ) ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) )
199 25 32 39 46 70 198 nnind ⊢ ( 𝑛 ∈ ℕ → ( ( 𝜑 ∧ 𝑛 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) )
200 18 199 vtoclg ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ∈ ℕ → ( ( 𝜑 ∧ 𝑀 ≤ 𝑀 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 ) ) )
201 3 3 9 200 syl3c ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ 𝐴 )
202 2 201 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )