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 46564

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 12720	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℤ)
2		fmuldfeq.8	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3	2	nnzd 12712	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
4	3	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ ℤ)
5	2	nnge1d 12379	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
6	5	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ≤ 𝑀)
7		nnre 12335	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8		leid 11399	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑀 ≤ 𝑀)
9	2, 7, 8	3syl 19	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
10	9	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ≤ 𝑀)
11	1, 4, 4, 6, 10	elfzd 13640	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ (1...𝑀))
12	2	3ad2ant1 1151	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → 𝑀 ∈ ℕ)
13		eleq1 2849	. . . . . . 7 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑀) ↔ 1 ∈ (1...𝑀)))
14	13	3anbi3d 1470	. . . . . 6 ⊢ (𝑚 = 1 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀))))
15		fveq2 6883	. . . . . . . 8 ⊢ (𝑚 = 1 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘1))
16	15	fveq1d 6885	. . . . . . 7 ⊢ (𝑚 = 1 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
17		fveq2 6883	. . . . . . 7 ⊢ (𝑚 = 1 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘1))
18	16, 17	eqeq12d 2777	. . . . . 6 ⊢ (𝑚 = 1 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1)))
19	14, 18	imbi12d 347	. . . . 5 ⊢ (𝑚 = 1 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))))
20		eleq1 2849	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑀) ↔ 𝑛 ∈ (1...𝑀)))
21	20	3anbi3d 1470	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀))))
22		fveq2 6883	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑛))
23	22	fveq1d 6885	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡))
24		fveq2 6883	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑛))
25	23, 24	eqeq12d 2777	. . . . . 6 ⊢ (𝑚 = 𝑛 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
26	21, 25	imbi12d 347	. . . . 5 ⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))))
27		eleq1 2849	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑚 ∈ (1...𝑀) ↔ (𝑛 + 1) ∈ (1...𝑀)))
28	27	3anbi3d 1470	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))))
29		fveq2 6883	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘(𝑛 + 1)))
30	29	fveq1d 6885	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡))
31		fveq2 6883	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
32	30, 31	eqeq12d 2777	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1))))
33	28, 32	imbi12d 347	. . . . 5 ⊢ (𝑚 = (𝑛 + 1) → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))))
34		eleq1 2849	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (𝑚 ∈ (1...𝑀) ↔ 𝑀 ∈ (1...𝑀)))
35	34	3anbi3d 1470	. . . . . 6 ⊢ (𝑚 = 𝑀 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀))))
36		fveq2 6883	. . . . . . . 8 ⊢ (𝑚 = 𝑀 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑀))
37	36	fveq1d 6885	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
38		fveq2 6883	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑀))
39	37, 38	eqeq12d 2777	. . . . . 6 ⊢ (𝑚 = 𝑀 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)))
40	35, 39	imbi12d 347	. . . . 5 ⊢ (𝑚 = 𝑀 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))))
41		1z 12719	. . . . . . . 8 ⊢ 1 ∈ ℤ
42		seq1 14150	. . . . . . . 8 ⊢ (1 ∈ ℤ → (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1))
43	41, 42	ax-mp 5	. . . . . . 7 ⊢ (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1)
44		1zzd 12720	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
45		1le1 11937	. . . . . . . . . . . . 13 ⊢ 1 ≤ 1
46	45	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ 1)
47	44, 3, 44, 46, 5	elfzd 13640	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...𝑀))
48		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖 𝑡 ∈ 𝑇
49		fmuldfeq.5	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
50		nfcv 2923	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑇
51		nfmpt1 5204	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
52	50, 51	nfmpt 5203	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
53	49, 52	nfcxfr 2921	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝐹
54		nfcv 2923	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝑡
55	53, 54	nffv 6893	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝐹‘𝑡)
56		nfcv 2923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖1
57	55, 56	nffv 6893	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1)
58		nffvmpt1 6894	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
59	57, 58	nfeq 2936	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
60	48, 59	nfim 1929	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
61		fveq2 6883	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘1))
62		fveq2 6883	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
63	61, 62	eqeq12d 2777	. . . . . . . . . . . . 13 ⊢ (𝑖 = 1 → (((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ↔ ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
64	63	imbi2d 343	. . . . . . . . . . . 12 ⊢ (𝑖 = 1 → ((𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) ↔ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))))
65		ovex 7451	. . . . . . . . . . . . . . 15 ⊢ (1...𝑀) ∈ V
66	65	mptex 7227	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V
67	49	fvmpt2 7003	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ 𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V) → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
68	66, 67	mpan2 704	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝑇 → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
69	68	fveq1d 6885	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖))
70	60, 64, 69	vtoclg1f 3531	. . . . . . . . . . 11 ⊢ (1 ∈ (1...𝑀) → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
71	47, 70	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
72	71	imp 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
73		eqid 2761	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
74		fveq2 6883	. . . . . . . . . . 11 ⊢ (𝑖 = 1 → (𝑈‘𝑖) = (𝑈‘1))
75	74	fveq1d 6885	. . . . . . . . . 10 ⊢ (𝑖 = 1 → ((𝑈‘𝑖)‘𝑡) = ((𝑈‘1)‘𝑡))
76	47	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ (1...𝑀))
77		fmuldfeq.9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)
78	77, 47	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘1) ∈ 𝑌)
79	78	ancli 558	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝜑 ∧ (𝑈‘1) ∈ 𝑌))
80		eleq1 2849	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑈‘1) → (𝑓 ∈ 𝑌 ↔ (𝑈‘1) ∈ 𝑌))
81	80	anbi2d 642	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘1) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘1) ∈ 𝑌)))
82		feq1 6685	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘1) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘1):𝑇⟶ℝ))
83	81, 82	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘1) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ)))
84		fmuldfeq.10	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)
85	84	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ 𝑌 → ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ))
86	83, 85	vtoclga 3537	. . . . . . . . . . . 12 ⊢ ((𝑈‘1) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ))
87	78, 79, 86	sylc 66	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘1):𝑇⟶ℝ)
88	87	ffvelcdmda 7082	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑈‘1)‘𝑡) ∈ ℝ)
89	73, 75, 76, 88	fvmptd3 7015	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1) = ((𝑈‘1)‘𝑡))
90	72, 89	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑈‘1)‘𝑡))
91		seq1 14150	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → (seq1(𝑃, 𝑈)‘1) = (𝑈‘1))
92	41, 91	ax-mp 5	. . . . . . . . 9 ⊢ (seq1(𝑃, 𝑈)‘1) = (𝑈‘1)
93	92	fveq1i 6884	. . . . . . . 8 ⊢ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = ((𝑈‘1)‘𝑡)
94	90, 93	eqtr4di 2814	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
95	43, 94	eqtr2id 2809	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))
96	95	3adant3 1150	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))
97		simp31 1228	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝜑)
98		simp1 1154	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ ℕ)
99		simp33 1230	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 + 1) ∈ (1...𝑀))
100	98, 99	jca 521	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)))
101		elnnuz 12998	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
102	101	biimpi 219	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
103	102	anim1i 627	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)) → (𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)))
104		peano2fzr 13663	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)) → 𝑛 ∈ (1...𝑀))
105	100, 103, 104	3syl 19	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ (1...𝑀))
106		simp32 1229	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑡 ∈ 𝑇)
107		simp2 1155	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
108	97, 106, 105, 107	mp3and 1493	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
109	105, 99, 108	3jca 1146	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
110		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑓𝜑
111		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑓 𝑛 ∈ (1...𝑀)
112		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑓(𝑛 + 1) ∈ (1...𝑀)
113		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓1
114		fmuldfeq.3	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
115		nfmpo1 7498	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑓(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
116	114, 115	nfcxfr 2921	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑃
117		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑈
118	113, 116, 117	nfseq 14147	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓seq1(𝑃, 𝑈)
119		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓𝑛
120	118, 119	nffv 6893	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓(seq1(𝑃, 𝑈)‘𝑛)
121		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓𝑡
122	120, 121	nffv 6893	. . . . . . . . . . 11 ⊢ Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
123		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(seq1( · , (𝐹‘𝑡))‘𝑛)
124	122, 123	nfeq 2936	. . . . . . . . . 10 ⊢ Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)
125	111, 112, 124	nf3an 1934	. . . . . . . . 9 ⊢ Ⅎ𝑓(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
126	110, 125	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑓(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
127		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑔𝜑
128		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑔 𝑛 ∈ (1...𝑀)
129		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑔(𝑛 + 1) ∈ (1...𝑀)
130		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔1
131		nfmpo2 7499	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
132	114, 131	nfcxfr 2921	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑃
133		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑈
134	130, 132, 133	nfseq 14147	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔seq1(𝑃, 𝑈)
135		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔𝑛
136	134, 135	nffv 6893	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔(seq1(𝑃, 𝑈)‘𝑛)
137		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝑡
138	136, 137	nffv 6893	. . . . . . . . . . 11 ⊢ Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
139		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑔(seq1( · , (𝐹‘𝑡))‘𝑛)
140	138, 139	nfeq 2936	. . . . . . . . . 10 ⊢ Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)
141	128, 129, 140	nf3an 1934	. . . . . . . . 9 ⊢ Ⅎ𝑔(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
142	127, 141	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑔(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
143		fmuldfeq.2	. . . . . . . 8 ⊢ Ⅎ𝑡𝑌
144		fmuldfeq.7	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ V)
145	144	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑇 ∈ V)
146	77	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑈:(1...𝑀)⟶𝑌)
147		fmuldfeq.11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)
148	147	3adant1r 1196	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)
149		simpr1 1213	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑛 ∈ (1...𝑀))
150		simpr2 1214	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → (𝑛 + 1) ∈ (1...𝑀))
151		simpr3 1215	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
152	84	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)
153	126, 142, 143, 114, 49, 145, 146, 148, 149, 150, 151, 152	fmuldfeqlem1 46563	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
154	97, 109, 106, 153	syl21anc 851	. . . . . 6 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
155	154	3exp 1137	. . . . 5 ⊢ (𝑛 ∈ ℕ → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))))
156	19, 26, 33, 40, 96, 155	nnind 12346	. . . 4 ⊢ (𝑀 ∈ ℕ → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)))
157	12, 156	mpcom 39	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
158	11, 157	mpd3an3 1491	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
159		fmuldfeq.4	. . . 4 ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
160	159	fveq1i 6884	. . 3 ⊢ (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡)
161	160	a1i 11	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
162		simpr 490	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇)
163		elnnuz 12998	. . . . . 6 ⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ_≥‘1))
164	2, 163	sylib 221	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
165	164	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ (ℤ_≥‘1))
166		fmuldfeq.1	. . . . . . . 8 ⊢ Ⅎ𝑖𝜑
167	166, 48	nfan 1932	. . . . . . 7 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑡 ∈ 𝑇)
168		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑖 𝑘 ∈ (1...𝑀)
169	167, 168	nfan 1932	. . . . . 6 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀))
170		nfcv 2923	. . . . . . . 8 ⊢ Ⅎ𝑖𝑘
171	55, 170	nffv 6893	. . . . . . 7 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘)
172	171	nfel1 2939	. . . . . 6 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘) ∈ ℝ
173	169, 172	nfim 1929	. . . . 5 ⊢ Ⅎ𝑖(((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
174		eleq1 2849	. . . . . . 7 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ (1...𝑀) ↔ 𝑘 ∈ (1...𝑀)))
175	174	anbi2d 642	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀))))
176		fveq2 6883	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘𝑘))
177	176	eleq1d 2846	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝐹‘𝑡)‘𝑖) ∈ ℝ ↔ ((𝐹‘𝑡)‘𝑘) ∈ ℝ))
178	175, 177	imbi12d 347	. . . . 5 ⊢ (𝑖 = 𝑘 → ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ) ↔ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)))
179	69	ad2antlr 740	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖))
180		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀))
181	77	ffvelcdmda 7082	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝑌)
182		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
183	182, 181	jca 521	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌))
184		eleq1 2849	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓 ∈ 𝑌 ↔ (𝑈‘𝑖) ∈ 𝑌))
185	184	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌)))
186		feq1 6685	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘𝑖):𝑇⟶ℝ))
187	185, 186	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ)))
188	187, 85	vtoclga 3537	. . . . . . . . . . 11 ⊢ ((𝑈‘𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ))
189	181, 183, 188	sylc 66	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
190	189	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
191		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇)
192	190, 191	ffvelcdmd 7083	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖)‘𝑡) ∈ ℝ)
193	73	fvmpt2 7003	. . . . . . . 8 ⊢ ((𝑖 ∈ (1...𝑀) ∧ ((𝑈‘𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
194	180, 192, 193	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
195	194, 192	eqeltrd 2861	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ∈ ℝ)
196	179, 195	eqeltrd 2861	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ)
197	173, 178, 196	chvarfv 2277	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
198		remulcl 11278	. . . . 5 ⊢ ((𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑘 · 𝑏) ∈ ℝ)
199	198	adantl 487	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑘 · 𝑏) ∈ ℝ)
200	165, 197, 199	seqcl 14158	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ)
201		fmuldfeq.6	. . . 4 ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))
202	201	fvmpt2 7003	. . 3 ⊢ ((𝑡 ∈ 𝑇 ∧ (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
203	162, 200, 202	syl2anc 596	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
204	158, 161, 203	3eqtr4d 2806	1 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 Ⅎwnf 1816 ∈ wcel 2145 Ⅎwnfc 2908 Vcvv 3451 class class class wbr 5103 ↦ cmpt 5186 ⟶wf 6533 ‘cfv 6537 (class class class)co 7418 ∈ cmpo 7420 ℝcr 11192 1c1 11194 + caddc 11196 · cmul 11198 ≤ cle 11337 ℕcn 12328 ℤcz 12686 ℤ_≥cuz 12958 ...cfz 13632 seqcseq 14137

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-er 8710 df-en 8967 df-dom 8968 df-sdom 8969 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-nn 12329 df-n0 12600 df-z 12687 df-uz 12959 df-fz 13633 df-seq 14138

This theorem is used by: stoweidlem42 47021 stoweidlem48 47027

W3C validator