fmuldfeq - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fmuldfeq		Structured version Visualization version GIF version

Theorem fmuldfeq 44597

Description: X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

**Hypotheses**
Ref	Expression
fmuldfeq.1	⊢ Ⅎ𝑖𝜑
fmuldfeq.2	⊢ Ⅎ𝑡𝑌
fmuldfeq.3	⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
fmuldfeq.4	⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
fmuldfeq.5	⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
fmuldfeq.6	⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))
fmuldfeq.7	⊢ (𝜑 → 𝑇 ∈ V)
fmuldfeq.8	⊢ (𝜑 → 𝑀 ∈ ℕ)
fmuldfeq.9	⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)
fmuldfeq.10	⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)
fmuldfeq.11	⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)

**Assertion**
Ref	Expression
fmuldfeq	⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡))

Distinct variable groups: 𝑡,𝑇 𝑓,𝑔,𝑡,𝑇 𝑓,𝑖,𝑡,𝑇 𝑓,𝐹,𝑔 𝑓,𝑀,𝑔 𝑈,𝑓,𝑔,𝑡 𝑓,𝑌,𝑔 𝜑,𝑓,𝑔 𝑖,𝑀 𝑈,𝑖 Allowed substitution hints: 𝜑(𝑡,𝑖) 𝑃(𝑡,𝑓,𝑔,𝑖) 𝐹(𝑡,𝑖) 𝑀(𝑡) 𝑋(𝑡,𝑓,𝑔,𝑖) 𝑌(𝑡,𝑖) 𝑍(𝑡,𝑓,𝑔,𝑖)

Proof of Theorem fmuldfeq Dummy variables 𝑘 𝑏 𝑛 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1zzd 12597	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℤ)
2		fmuldfeq.8	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3	2	nnzd 12589	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
4	3	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ ℤ)
5	2	nnge1d 12264	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
6	5	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ≤ 𝑀)
7		nnre 12223	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8		leid 11314	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑀 ≤ 𝑀)
9	2, 7, 8	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
10	9	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ≤ 𝑀)
11	1, 4, 4, 6, 10	elfzd 13496	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ (1...𝑀))
12	2	3ad2ant1 1131	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → 𝑀 ∈ ℕ)
13		eleq1 2819	. . . . . . 7 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑀) ↔ 1 ∈ (1...𝑀)))
14	13	3anbi3d 1440	. . . . . 6 ⊢ (𝑚 = 1 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀))))
15		fveq2 6890	. . . . . . . 8 ⊢ (𝑚 = 1 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘1))
16	15	fveq1d 6892	. . . . . . 7 ⊢ (𝑚 = 1 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
17		fveq2 6890	. . . . . . 7 ⊢ (𝑚 = 1 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘1))
18	16, 17	eqeq12d 2746	. . . . . 6 ⊢ (𝑚 = 1 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1)))
19	14, 18	imbi12d 343	. . . . 5 ⊢ (𝑚 = 1 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))))
20		eleq1 2819	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑀) ↔ 𝑛 ∈ (1...𝑀)))
21	20	3anbi3d 1440	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀))))
22		fveq2 6890	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑛))
23	22	fveq1d 6892	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡))
24		fveq2 6890	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑛))
25	23, 24	eqeq12d 2746	. . . . . 6 ⊢ (𝑚 = 𝑛 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
26	21, 25	imbi12d 343	. . . . 5 ⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))))
27		eleq1 2819	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑚 ∈ (1...𝑀) ↔ (𝑛 + 1) ∈ (1...𝑀)))
28	27	3anbi3d 1440	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))))
29		fveq2 6890	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘(𝑛 + 1)))
30	29	fveq1d 6892	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡))
31		fveq2 6890	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
32	30, 31	eqeq12d 2746	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1))))
33	28, 32	imbi12d 343	. . . . 5 ⊢ (𝑚 = (𝑛 + 1) → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))))
34		eleq1 2819	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (𝑚 ∈ (1...𝑀) ↔ 𝑀 ∈ (1...𝑀)))
35	34	3anbi3d 1440	. . . . . 6 ⊢ (𝑚 = 𝑀 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀))))
36		fveq2 6890	. . . . . . . 8 ⊢ (𝑚 = 𝑀 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑀))
37	36	fveq1d 6892	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
38		fveq2 6890	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑀))
39	37, 38	eqeq12d 2746	. . . . . 6 ⊢ (𝑚 = 𝑀 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)))
40	35, 39	imbi12d 343	. . . . 5 ⊢ (𝑚 = 𝑀 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))))
41		1z 12596	. . . . . . . 8 ⊢ 1 ∈ ℤ
42		seq1 13983	. . . . . . . 8 ⊢ (1 ∈ ℤ → (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1))
43	41, 42	ax-mp 5	. . . . . . 7 ⊢ (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1)
44		1zzd 12597	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
45		1le1 11846	. . . . . . . . . . . . 13 ⊢ 1 ≤ 1
46	45	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ 1)
47	44, 3, 44, 46, 5	elfzd 13496	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...𝑀))
48		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖 𝑡 ∈ 𝑇
49		fmuldfeq.5	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
50		nfcv 2901	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑇
51		nfmpt1 5255	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
52	50, 51	nfmpt 5254	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
53	49, 52	nfcxfr 2899	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝐹
54		nfcv 2901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝑡
55	53, 54	nffv 6900	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝐹‘𝑡)
56		nfcv 2901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖1
57	55, 56	nffv 6900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1)
58		nffvmpt1 6901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
59	57, 58	nfeq 2914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
60	48, 59	nfim 1897	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
61		fveq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘1))
62		fveq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
63	61, 62	eqeq12d 2746	. . . . . . . . . . . . 13 ⊢ (𝑖 = 1 → (((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ↔ ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
64	63	imbi2d 339	. . . . . . . . . . . 12 ⊢ (𝑖 = 1 → ((𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) ↔ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))))
65		ovex 7444	. . . . . . . . . . . . . . 15 ⊢ (1...𝑀) ∈ V
66	65	mptex 7226	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V
67	49	fvmpt2 7008	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ 𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V) → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
68	66, 67	mpan2 687	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝑇 → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
69	68	fveq1d 6892	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖))
70	60, 64, 69	vtoclg1f 3557	. . . . . . . . . . 11 ⊢ (1 ∈ (1...𝑀) → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
71	47, 70	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
72	71	imp 405	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
73		eqid 2730	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
74		fveq2 6890	. . . . . . . . . . 11 ⊢ (𝑖 = 1 → (𝑈‘𝑖) = (𝑈‘1))
75	74	fveq1d 6892	. . . . . . . . . 10 ⊢ (𝑖 = 1 → ((𝑈‘𝑖)‘𝑡) = ((𝑈‘1)‘𝑡))
76	47	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ (1...𝑀))
77		fmuldfeq.9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)
78	77, 47	ffvelcdmd 7086	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘1) ∈ 𝑌)
79	78	ancli 547	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝜑 ∧ (𝑈‘1) ∈ 𝑌))
80		eleq1 2819	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑈‘1) → (𝑓 ∈ 𝑌 ↔ (𝑈‘1) ∈ 𝑌))
81	80	anbi2d 627	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘1) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘1) ∈ 𝑌)))
82		feq1 6697	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘1) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘1):𝑇⟶ℝ))
83	81, 82	imbi12d 343	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘1) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ)))
84		fmuldfeq.10	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)
85	84	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ 𝑌 → ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ))
86	83, 85	vtoclga 3565	. . . . . . . . . . . 12 ⊢ ((𝑈‘1) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ))
87	78, 79, 86	sylc 65	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘1):𝑇⟶ℝ)
88	87	ffvelcdmda 7085	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑈‘1)‘𝑡) ∈ ℝ)
89	73, 75, 76, 88	fvmptd3 7020	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1) = ((𝑈‘1)‘𝑡))
90	72, 89	eqtrd 2770	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑈‘1)‘𝑡))
91		seq1 13983	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → (seq1(𝑃, 𝑈)‘1) = (𝑈‘1))
92	41, 91	ax-mp 5	. . . . . . . . 9 ⊢ (seq1(𝑃, 𝑈)‘1) = (𝑈‘1)
93	92	fveq1i 6891	. . . . . . . 8 ⊢ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = ((𝑈‘1)‘𝑡)
94	90, 93	eqtr4di 2788	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
95	43, 94	eqtr2id 2783	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))
96	95	3adant3 1130	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))
97		simp31 1207	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝜑)
98		simp1 1134	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ ℕ)
99		simp33 1209	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 + 1) ∈ (1...𝑀))
100	98, 99	jca 510	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)))
101		elnnuz 12870	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
102	101	biimpi 215	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
103	102	anim1i 613	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)) → (𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)))
104		peano2fzr 13518	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)) → 𝑛 ∈ (1...𝑀))
105	100, 103, 104	3syl 18	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ (1...𝑀))
106		simp32 1208	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑡 ∈ 𝑇)
107		simp2 1135	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
108	97, 106, 105, 107	mp3and 1462	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
109	105, 99, 108	3jca 1126	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
110		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑓𝜑
111		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑓 𝑛 ∈ (1...𝑀)
112		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑓(𝑛 + 1) ∈ (1...𝑀)
113		nfcv 2901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓1
114		fmuldfeq.3	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
115		nfmpo1 7491	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑓(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
116	114, 115	nfcxfr 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑃
117		nfcv 2901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑈
118	113, 116, 117	nfseq 13980	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓seq1(𝑃, 𝑈)
119		nfcv 2901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓𝑛
120	118, 119	nffv 6900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓(seq1(𝑃, 𝑈)‘𝑛)
121		nfcv 2901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓𝑡
122	120, 121	nffv 6900	. . . . . . . . . . 11 ⊢ Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
123		nfcv 2901	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(seq1( · , (𝐹‘𝑡))‘𝑛)
124	122, 123	nfeq 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)
125	111, 112, 124	nf3an 1902	. . . . . . . . 9 ⊢ Ⅎ𝑓(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
126	110, 125	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑓(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
127		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑔𝜑
128		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑔 𝑛 ∈ (1...𝑀)
129		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑔(𝑛 + 1) ∈ (1...𝑀)
130		nfcv 2901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔1
131		nfmpo2 7492	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
132	114, 131	nfcxfr 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑃
133		nfcv 2901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑈
134	130, 132, 133	nfseq 13980	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔seq1(𝑃, 𝑈)
135		nfcv 2901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔𝑛
136	134, 135	nffv 6900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔(seq1(𝑃, 𝑈)‘𝑛)
137		nfcv 2901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝑡
138	136, 137	nffv 6900	. . . . . . . . . . 11 ⊢ Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
139		nfcv 2901	. . . . . . . . . . 11 ⊢ Ⅎ𝑔(seq1( · , (𝐹‘𝑡))‘𝑛)
140	138, 139	nfeq 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)
141	128, 129, 140	nf3an 1902	. . . . . . . . 9 ⊢ Ⅎ𝑔(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
142	127, 141	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑔(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
143		fmuldfeq.2	. . . . . . . 8 ⊢ Ⅎ𝑡𝑌
144		fmuldfeq.7	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ V)
145	144	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑇 ∈ V)
146	77	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑈:(1...𝑀)⟶𝑌)
147		fmuldfeq.11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)
148	147	3adant1r 1175	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)
149		simpr1 1192	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑛 ∈ (1...𝑀))
150		simpr2 1193	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → (𝑛 + 1) ∈ (1...𝑀))
151		simpr3 1194	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
152	84	adantlr 711	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)
153	126, 142, 143, 114, 49, 145, 146, 148, 149, 150, 151, 152	fmuldfeqlem1 44596	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
154	97, 109, 106, 153	syl21anc 834	. . . . . 6 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
155	154	3exp 1117	. . . . 5 ⊢ (𝑛 ∈ ℕ → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))))
156	19, 26, 33, 40, 96, 155	nnind 12234	. . . 4 ⊢ (𝑀 ∈ ℕ → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)))
157	12, 156	mpcom 38	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
158	11, 157	mpd3an3 1460	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
159		fmuldfeq.4	. . . 4 ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
160	159	fveq1i 6891	. . 3 ⊢ (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡)
161	160	a1i 11	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
162		simpr 483	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇)
163		elnnuz 12870	. . . . . 6 ⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ_≥‘1))
164	2, 163	sylib 217	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
165	164	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ (ℤ_≥‘1))
166		fmuldfeq.1	. . . . . . . 8 ⊢ Ⅎ𝑖𝜑
167	166, 48	nfan 1900	. . . . . . 7 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑡 ∈ 𝑇)
168		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑖 𝑘 ∈ (1...𝑀)
169	167, 168	nfan 1900	. . . . . 6 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀))
170		nfcv 2901	. . . . . . . 8 ⊢ Ⅎ𝑖𝑘
171	55, 170	nffv 6900	. . . . . . 7 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘)
172	171	nfel1 2917	. . . . . 6 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘) ∈ ℝ
173	169, 172	nfim 1897	. . . . 5 ⊢ Ⅎ𝑖(((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
174		eleq1 2819	. . . . . . 7 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ (1...𝑀) ↔ 𝑘 ∈ (1...𝑀)))
175	174	anbi2d 627	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀))))
176		fveq2 6890	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘𝑘))
177	176	eleq1d 2816	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝐹‘𝑡)‘𝑖) ∈ ℝ ↔ ((𝐹‘𝑡)‘𝑘) ∈ ℝ))
178	175, 177	imbi12d 343	. . . . 5 ⊢ (𝑖 = 𝑘 → ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ) ↔ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)))
179	69	ad2antlr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖))
180		simpr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀))
181	77	ffvelcdmda 7085	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝑌)
182		simpl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
183	182, 181	jca 510	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌))
184		eleq1 2819	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓 ∈ 𝑌 ↔ (𝑈‘𝑖) ∈ 𝑌))
185	184	anbi2d 627	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌)))
186		feq1 6697	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘𝑖):𝑇⟶ℝ))
187	185, 186	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ)))
188	187, 85	vtoclga 3565	. . . . . . . . . . 11 ⊢ ((𝑈‘𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ))
189	181, 183, 188	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
190	189	adantlr 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
191		simplr 765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇)
192	190, 191	ffvelcdmd 7086	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖)‘𝑡) ∈ ℝ)
193	73	fvmpt2 7008	. . . . . . . 8 ⊢ ((𝑖 ∈ (1...𝑀) ∧ ((𝑈‘𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
194	180, 192, 193	syl2anc 582	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
195	194, 192	eqeltrd 2831	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ∈ ℝ)
196	179, 195	eqeltrd 2831	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ)
197	173, 178, 196	chvarfv 2231	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
198		remulcl 11197	. . . . 5 ⊢ ((𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑘 · 𝑏) ∈ ℝ)
199	198	adantl 480	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑘 · 𝑏) ∈ ℝ)
200	165, 197, 199	seqcl 13992	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ)
201		fmuldfeq.6	. . . 4 ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))
202	201	fvmpt2 7008	. . 3 ⊢ ((𝑡 ∈ 𝑇 ∧ (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
203	162, 200, 202	syl2anc 582	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
204	158, 161, 203	3eqtr4d 2780	1 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1085 = wceq 1539 Ⅎwnf 1783 ∈ wcel 2104 Ⅎwnfc 2881 Vcvv 3472 class class class wbr 5147 ↦ cmpt 5230 ⟶wf 6538 ‘cfv 6542 (class class class)co 7411 ∈ cmpo 7413 ℝcr 11111 1c1 11113 + caddc 11115 · cmul 11117 ≤ cle 11253 ℕcn 12216 ℤcz 12562 ℤ_≥cuz 12826 ...cfz 13488 seqcseq 13970

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-n0 12477 df-z 12563 df-uz 12827 df-fz 13489 df-seq 13971

This theorem is referenced by: stoweidlem42 45056 stoweidlem48 45062

W3C validator