Metamath Proof Explorer

Theorem fmuldfeqlem1

Description: induction step for the proof of fmuldfeq . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses fmuldfeqlem1.1 ⊢ Ⅎ 𝑓 𝜑
fmuldfeqlem1.2 ⊢ Ⅎ 𝑔 𝜑
fmuldfeqlem1.3 ⊢ Ⅎ 𝑡 𝑌
fmuldfeqlem1.5 ⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
fmuldfeqlem1.6 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
fmuldfeqlem1.7 ⊢ ( 𝜑 → 𝑇 ∈ V )
fmuldfeqlem1.8 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
fmuldfeqlem1.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 )
fmuldfeqlem1.10 ⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑀 ) )
fmuldfeqlem1.11 ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( 1 ... 𝑀 ) )
fmuldfeqlem1.12 ⊢ ( 𝜑 → ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) = ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) )
fmuldfeqlem1.13 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) → 𝑓 : 𝑇 ⟶ ℝ )
Assertion fmuldfeqlem1 ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) = ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ ( 𝑁 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 fmuldfeqlem1.1 ⊢ Ⅎ 𝑓 𝜑
2 fmuldfeqlem1.2 ⊢ Ⅎ 𝑔 𝜑
3 fmuldfeqlem1.3 ⊢ Ⅎ 𝑡 𝑌
4 fmuldfeqlem1.5 ⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
5 fmuldfeqlem1.6 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
6 fmuldfeqlem1.7 ⊢ ( 𝜑 → 𝑇 ∈ V )
7 fmuldfeqlem1.8 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
8 fmuldfeqlem1.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 )
9 fmuldfeqlem1.10 ⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑀 ) )
10 fmuldfeqlem1.11 ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( 1 ... 𝑀 ) )
11 fmuldfeqlem1.12 ⊢ ( 𝜑 → ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) = ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) )
12 fmuldfeqlem1.13 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) → 𝑓 : 𝑇 ⟶ ℝ )
13 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
14 13 mptex ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ V
15 5 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ V ) → ( 𝐹 ‘ 𝑡 ) = ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
16 14 15 mpan2 ⊢ ( 𝑡 ∈ 𝑇 → ( 𝐹 ‘ 𝑡 ) = ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
17 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑈 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑗 ) )
18 17 fveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝑈 ‘ 𝑗 ) ‘ 𝑡 ) )
19 18 cbvmptv ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑗 ) ‘ 𝑡 ) )
20 16 19 eqtrdi ⊢ ( 𝑡 ∈ 𝑇 → ( 𝐹 ‘ 𝑡 ) = ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑗 ) ‘ 𝑡 ) ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) = ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑗 ) ‘ 𝑡 ) ) )
22 fveq2 ⊢ ( 𝑗 = ( 𝑁 + 1 ) → ( 𝑈 ‘ 𝑗 ) = ( 𝑈 ‘ ( 𝑁 + 1 ) ) )
23 22 fveq1d ⊢ ( 𝑗 = ( 𝑁 + 1 ) → ( ( 𝑈 ‘ 𝑗 ) ‘ 𝑡 ) = ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) )
24 23 adantl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 = ( 𝑁 + 1 ) ) → ( ( 𝑈 ‘ 𝑗 ) ‘ 𝑡 ) = ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) )
25 10 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑁 + 1 ) ∈ ( 1 ... 𝑀 ) )
26 7 10 ffvelcdmd ⊢ ( 𝜑 → ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌 )
27 26 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌 ) )
28 nfcv ⊢ Ⅎ 𝑓 ( 𝑈 ‘ ( 𝑁 + 1 ) )
29 nfv ⊢ Ⅎ 𝑓 ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌
30 1 29 nfan ⊢ Ⅎ 𝑓 ( 𝜑 ∧ ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌 )
31 nfv ⊢ Ⅎ 𝑓 ( 𝑈 ‘ ( 𝑁 + 1 ) ) : 𝑇 ⟶ ℝ
32 30 31 nfim ⊢ Ⅎ 𝑓 ( ( 𝜑 ∧ ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌 ) → ( 𝑈 ‘ ( 𝑁 + 1 ) ) : 𝑇 ⟶ ℝ )
33 eleq1 ⊢ ( 𝑓 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) → ( 𝑓 ∈ 𝑌 ↔ ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌 ) )
34 33 anbi2d ⊢ ( 𝑓 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) → ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) ↔ ( 𝜑 ∧ ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌 ) ) )
35 feq1 ⊢ ( 𝑓 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝑈 ‘ ( 𝑁 + 1 ) ) : 𝑇 ⟶ ℝ ) )
36 34 35 imbi12d ⊢ ( 𝑓 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌 ) → ( 𝑈 ‘ ( 𝑁 + 1 ) ) : 𝑇 ⟶ ℝ ) ) )
37 28 32 36 12 vtoclgf ⊢ ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌 → ( ( 𝜑 ∧ ( 𝑈 ‘ ( 𝑁 + 1 ) ) ∈ 𝑌 ) → ( 𝑈 ‘ ( 𝑁 + 1 ) ) : 𝑇 ⟶ ℝ ) )
38 26 27 37 sylc ⊢ ( 𝜑 → ( 𝑈 ‘ ( 𝑁 + 1 ) ) : 𝑇 ⟶ ℝ )
39 38 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ∈ ℝ )
40 21 24 25 39 fvmptd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) ‘ ( 𝑁 + 1 ) ) = ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) )
41 40 oveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) · ( ( 𝐹 ‘ 𝑡 ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) )
42 elfzuz ⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
43 9 42 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
44 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) · ( ( 𝐹 ‘ 𝑡 ) ‘ ( 𝑁 + 1 ) ) ) )
45 43 44 syl ⊢ ( 𝜑 → ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) · ( ( 𝐹 ‘ 𝑡 ) ‘ ( 𝑁 + 1 ) ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) · ( ( 𝐹 ‘ 𝑡 ) ‘ ( 𝑁 + 1 ) ) ) )
47 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( 𝑃 , 𝑈 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) 𝑃 ( 𝑈 ‘ ( 𝑁 + 1 ) ) ) )
48 43 47 syl ⊢ ( 𝜑 → ( seq 1 ( 𝑃 , 𝑈 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) 𝑃 ( 𝑈 ‘ ( 𝑁 + 1 ) ) ) )
49 nfcv ⊢ Ⅎ ℎ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
50 nfcv ⊢ Ⅎ 𝑙 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
51 nfcv ⊢ Ⅎ 𝑓 ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) )
52 nfcv ⊢ Ⅎ 𝑔 ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) )
53 fveq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ‘ 𝑡 ) = ( ℎ ‘ 𝑡 ) )
54 fveq1 ⊢ ( 𝑔 = 𝑙 → ( 𝑔 ‘ 𝑡 ) = ( 𝑙 ‘ 𝑡 ) )
55 53 54 oveqan12d ⊢ ( ( 𝑓 = ℎ ∧ 𝑔 = 𝑙 ) → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) )
56 55 mpteq2dv ⊢ ( ( 𝑓 = ℎ ∧ 𝑔 = 𝑙 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) )
57 49 50 51 52 56 cbvmpo ⊢ ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ℎ ∈ 𝑌 , 𝑙 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) )
58 4 57 eqtri ⊢ 𝑃 = ( ℎ ∈ 𝑌 , 𝑙 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) )
59 58 a1i ⊢ ( 𝜑 → 𝑃 = ( ℎ ∈ 𝑌 , 𝑙 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ) )
60 nfcv ⊢ Ⅎ 𝑡 1
61 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
62 3 3 61 nfmpo ⊢ Ⅎ 𝑡 ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
63 4 62 nfcxfr ⊢ Ⅎ 𝑡 𝑃
64 nfcv ⊢ Ⅎ 𝑡 𝑈
65 60 63 64 nfseq ⊢ Ⅎ 𝑡 seq 1 ( 𝑃 , 𝑈 )
66 nfcv ⊢ Ⅎ 𝑡 𝑁
67 65 66 nffv ⊢ Ⅎ 𝑡 ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 )
68 67 nfeq2 ⊢ Ⅎ 𝑡 ℎ = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 )
69 nfv ⊢ Ⅎ 𝑡 𝑙 = ( 𝑈 ‘ ( 𝑁 + 1 ) )
70 68 69 nfan ⊢ Ⅎ 𝑡 ( ℎ = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∧ 𝑙 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) )
71 fveq1 ⊢ ( ℎ = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) → ( ℎ ‘ 𝑡 ) = ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) )
72 71 ad2antrr ⊢ ( ( ( ℎ = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∧ 𝑙 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ℎ ‘ 𝑡 ) = ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) )
73 fveq1 ⊢ ( 𝑙 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) → ( 𝑙 ‘ 𝑡 ) = ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) )
74 73 ad2antlr ⊢ ( ( ( ℎ = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∧ 𝑙 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑙 ‘ 𝑡 ) = ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) )
75 72 74 oveq12d ⊢ ( ( ( ℎ = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∧ 𝑙 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) = ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) )
76 70 75 mpteq2da ⊢ ( ( ℎ = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∧ 𝑙 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) ) )
77 76 adantl ⊢ ( ( 𝜑 ∧ ( ℎ = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∧ 𝑙 = ( 𝑈 ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) ) )
78 eqid ⊢ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 )
79 3simpc ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) )
80 nfcv ⊢ Ⅎ 𝑓 ℎ
81 nfcv ⊢ Ⅎ 𝑔 ℎ
82 nfcv ⊢ Ⅎ 𝑔 𝑙
83 nfv ⊢ Ⅎ 𝑓 ℎ ∈ 𝑌
84 nfv ⊢ Ⅎ 𝑓 𝑔 ∈ 𝑌
85 1 83 84 nf3an ⊢ Ⅎ 𝑓 ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 )
86 nfv ⊢ Ⅎ 𝑓 ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌
87 85 86 nfim ⊢ Ⅎ 𝑓 ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 )
88 nfv ⊢ Ⅎ 𝑔 ℎ ∈ 𝑌
89 nfv ⊢ Ⅎ 𝑔 𝑙 ∈ 𝑌
90 2 88 89 nf3an ⊢ Ⅎ 𝑔 ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 )
91 nfv ⊢ Ⅎ 𝑔 ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌
92 90 91 nfim ⊢ Ⅎ 𝑔 ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 )
93 eleq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ∈ 𝑌 ↔ ℎ ∈ 𝑌 ) )
94 93 3anbi2d ⊢ ( 𝑓 = ℎ → ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ↔ ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ) )
95 53 oveq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
96 95 mpteq2dv ⊢ ( 𝑓 = ℎ → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
97 96 eleq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ) )
98 94 97 imbi12d ⊢ ( 𝑓 = ℎ → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ) ↔ ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ) ) )
99 eleq1 ⊢ ( 𝑔 = 𝑙 → ( 𝑔 ∈ 𝑌 ↔ 𝑙 ∈ 𝑌 ) )
100 99 3anbi3d ⊢ ( 𝑔 = 𝑙 → ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ↔ ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) ) )
101 54 oveq2d ⊢ ( 𝑔 = 𝑙 → ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) )
102 101 mpteq2dv ⊢ ( 𝑔 = 𝑙 → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) )
103 102 eleq1d ⊢ ( 𝑔 = 𝑙 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 ) )
104 100 103 imbi12d ⊢ ( 𝑔 = 𝑙 → ( ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ) ↔ ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 ) ) )
105 80 81 82 87 92 98 104 8 vtocl2gf ⊢ ( ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 ) )
106 79 105 mpcom ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 )
107 58 78 9 7 106 6 fmulcl ⊢ ( 𝜑 → ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 )
108 mptexg ⊢ ( 𝑇 ∈ V → ( 𝑡 ∈ 𝑇 ↦ ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) ) ∈ V )
109 6 108 syl ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) ) ∈ V )
110 59 77 107 26 109 ovmpod ⊢ ( 𝜑 → ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) 𝑃 ( 𝑈 ‘ ( 𝑁 + 1 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) ) )
111 48 110 eqtrd ⊢ ( 𝜑 → ( seq 1 ( 𝑃 , 𝑈 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) ) )
112 107 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 ) )
113 nfcv ⊢ Ⅎ 𝑓 1
114 nfmpo1 ⊢ Ⅎ 𝑓 ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
115 4 114 nfcxfr ⊢ Ⅎ 𝑓 𝑃
116 nfcv ⊢ Ⅎ 𝑓 𝑈
117 113 115 116 nfseq ⊢ Ⅎ 𝑓 seq 1 ( 𝑃 , 𝑈 )
118 nfcv ⊢ Ⅎ 𝑓 𝑁
119 117 118 nffv ⊢ Ⅎ 𝑓 ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 )
120 119 nfel1 ⊢ Ⅎ 𝑓 ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌
121 1 120 nfan ⊢ Ⅎ 𝑓 ( 𝜑 ∧ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 )
122 nfcv ⊢ Ⅎ 𝑓 𝑇
123 nfcv ⊢ Ⅎ 𝑓 ℝ
124 119 122 123 nff ⊢ Ⅎ 𝑓 ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) : 𝑇 ⟶ ℝ
125 121 124 nfim ⊢ Ⅎ 𝑓 ( ( 𝜑 ∧ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 ) → ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) : 𝑇 ⟶ ℝ )
126 eleq1 ⊢ ( 𝑓 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) → ( 𝑓 ∈ 𝑌 ↔ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 ) )
127 126 anbi2d ⊢ ( 𝑓 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) → ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) ↔ ( 𝜑 ∧ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 ) ) )
128 feq1 ⊢ ( 𝑓 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) : 𝑇 ⟶ ℝ ) )
129 127 128 imbi12d ⊢ ( 𝑓 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 ) → ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) : 𝑇 ⟶ ℝ ) ) )
130 119 125 129 12 vtoclgf ⊢ ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 → ( ( 𝜑 ∧ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 ) → ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) : 𝑇 ⟶ ℝ ) )
131 107 112 130 sylc ⊢ ( 𝜑 → ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) : 𝑇 ⟶ ℝ )
132 131 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) ∈ ℝ )
133 132 39 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) ∈ ℝ )
134 111 133 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) = ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) )
135 11 oveq1d ⊢ ( 𝜑 → ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) = ( ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) )
136 135 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ‘ 𝑡 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) = ( ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) )
137 134 136 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) = ( ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑁 ) · ( ( 𝑈 ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) ) )
138 41 46 137 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( seq 1 ( 𝑃 , 𝑈 ) ‘ ( 𝑁 + 1 ) ) ‘ 𝑡 ) = ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ ( 𝑁 + 1 ) ) )