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 45771

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 12520	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℤ)
2		fmuldfeq.8	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3	2	nnzd 12512	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
4	3	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ ℤ)
5	2	nnge1d 12191	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
6	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ≤ 𝑀)
7		nnre 12150	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8		leid 11227	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑀 ≤ 𝑀)
9	2, 7, 8	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
10	9	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ≤ 𝑀)
11	1, 4, 4, 6, 10	elfzd 13429	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ (1...𝑀))
12	2	3ad2ant1 1133	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → 𝑀 ∈ ℕ)
13		eleq1 2822	. . . . . . 7 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑀) ↔ 1 ∈ (1...𝑀)))
14	13	3anbi3d 1444	. . . . . 6 ⊢ (𝑚 = 1 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀))))
15		fveq2 6832	. . . . . . . 8 ⊢ (𝑚 = 1 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘1))
16	15	fveq1d 6834	. . . . . . 7 ⊢ (𝑚 = 1 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
17		fveq2 6832	. . . . . . 7 ⊢ (𝑚 = 1 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘1))
18	16, 17	eqeq12d 2750	. . . . . 6 ⊢ (𝑚 = 1 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1)))
19	14, 18	imbi12d 344	. . . . 5 ⊢ (𝑚 = 1 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))))
20		eleq1 2822	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑀) ↔ 𝑛 ∈ (1...𝑀)))
21	20	3anbi3d 1444	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀))))
22		fveq2 6832	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑛))
23	22	fveq1d 6834	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡))
24		fveq2 6832	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑛))
25	23, 24	eqeq12d 2750	. . . . . 6 ⊢ (𝑚 = 𝑛 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
26	21, 25	imbi12d 344	. . . . 5 ⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))))
27		eleq1 2822	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑚 ∈ (1...𝑀) ↔ (𝑛 + 1) ∈ (1...𝑀)))
28	27	3anbi3d 1444	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))))
29		fveq2 6832	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘(𝑛 + 1)))
30	29	fveq1d 6834	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡))
31		fveq2 6832	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
32	30, 31	eqeq12d 2750	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1))))
33	28, 32	imbi12d 344	. . . . 5 ⊢ (𝑚 = (𝑛 + 1) → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))))
34		eleq1 2822	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (𝑚 ∈ (1...𝑀) ↔ 𝑀 ∈ (1...𝑀)))
35	34	3anbi3d 1444	. . . . . 6 ⊢ (𝑚 = 𝑀 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀))))
36		fveq2 6832	. . . . . . . 8 ⊢ (𝑚 = 𝑀 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑀))
37	36	fveq1d 6834	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
38		fveq2 6832	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑀))
39	37, 38	eqeq12d 2750	. . . . . 6 ⊢ (𝑚 = 𝑀 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)))
40	35, 39	imbi12d 344	. . . . 5 ⊢ (𝑚 = 𝑀 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))))
41		1z 12519	. . . . . . . 8 ⊢ 1 ∈ ℤ
42		seq1 13935	. . . . . . . 8 ⊢ (1 ∈ ℤ → (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1))
43	41, 42	ax-mp 5	. . . . . . 7 ⊢ (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1)
44		1zzd 12520	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
45		1le1 11763	. . . . . . . . . . . . 13 ⊢ 1 ≤ 1
46	45	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ 1)
47	44, 3, 44, 46, 5	elfzd 13429	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...𝑀))
48		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖 𝑡 ∈ 𝑇
49		fmuldfeq.5	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
50		nfcv 2896	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑇
51		nfmpt1 5195	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
52	50, 51	nfmpt 5194	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
53	49, 52	nfcxfr 2894	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝐹
54		nfcv 2896	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝑡
55	53, 54	nffv 6842	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝐹‘𝑡)
56		nfcv 2896	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖1
57	55, 56	nffv 6842	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1)
58		nffvmpt1 6843	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
59	57, 58	nfeq 2910	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
60	48, 59	nfim 1897	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
61		fveq2 6832	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘1))
62		fveq2 6832	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
63	61, 62	eqeq12d 2750	. . . . . . . . . . . . 13 ⊢ (𝑖 = 1 → (((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ↔ ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
64	63	imbi2d 340	. . . . . . . . . . . 12 ⊢ (𝑖 = 1 → ((𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) ↔ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))))
65		ovex 7389	. . . . . . . . . . . . . . 15 ⊢ (1...𝑀) ∈ V
66	65	mptex 7167	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V
67	49	fvmpt2 6950	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ 𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V) → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
68	66, 67	mpan2 691	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝑇 → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
69	68	fveq1d 6834	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖))
70	60, 64, 69	vtoclg1f 3524	. . . . . . . . . . 11 ⊢ (1 ∈ (1...𝑀) → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
71	47, 70	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
72	71	imp 406	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
73		eqid 2734	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
74		fveq2 6832	. . . . . . . . . . 11 ⊢ (𝑖 = 1 → (𝑈‘𝑖) = (𝑈‘1))
75	74	fveq1d 6834	. . . . . . . . . 10 ⊢ (𝑖 = 1 → ((𝑈‘𝑖)‘𝑡) = ((𝑈‘1)‘𝑡))
76	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ (1...𝑀))
77		fmuldfeq.9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)
78	77, 47	ffvelcdmd 7028	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘1) ∈ 𝑌)
79	78	ancli 548	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝜑 ∧ (𝑈‘1) ∈ 𝑌))
80		eleq1 2822	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑈‘1) → (𝑓 ∈ 𝑌 ↔ (𝑈‘1) ∈ 𝑌))
81	80	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘1) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘1) ∈ 𝑌)))
82		feq1 6638	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘1) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘1):𝑇⟶ℝ))
83	81, 82	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘1) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ)))
84		fmuldfeq.10	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)
85	84	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ 𝑌 → ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ))
86	83, 85	vtoclga 3530	. . . . . . . . . . . 12 ⊢ ((𝑈‘1) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ))
87	78, 79, 86	sylc 65	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘1):𝑇⟶ℝ)
88	87	ffvelcdmda 7027	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑈‘1)‘𝑡) ∈ ℝ)
89	73, 75, 76, 88	fvmptd3 6962	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1) = ((𝑈‘1)‘𝑡))
90	72, 89	eqtrd 2769	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑈‘1)‘𝑡))
91		seq1 13935	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → (seq1(𝑃, 𝑈)‘1) = (𝑈‘1))
92	41, 91	ax-mp 5	. . . . . . . . 9 ⊢ (seq1(𝑃, 𝑈)‘1) = (𝑈‘1)
93	92	fveq1i 6833	. . . . . . . 8 ⊢ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = ((𝑈‘1)‘𝑡)
94	90, 93	eqtr4di 2787	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
95	43, 94	eqtr2id 2782	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))
96	95	3adant3 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))
97		simp31 1210	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝜑)
98		simp1 1136	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ ℕ)
99		simp33 1212	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 + 1) ∈ (1...𝑀))
100	98, 99	jca 511	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)))
101		elnnuz 12789	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
102	101	biimpi 216	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
103	102	anim1i 615	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)) → (𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)))
104		peano2fzr 13451	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)) → 𝑛 ∈ (1...𝑀))
105	100, 103, 104	3syl 18	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ (1...𝑀))
106		simp32 1211	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑡 ∈ 𝑇)
107		simp2 1137	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
108	97, 106, 105, 107	mp3and 1466	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
109	105, 99, 108	3jca 1128	. . . . . . 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 2896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓1
114		fmuldfeq.3	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
115		nfmpo1 7436	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑓(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
116	114, 115	nfcxfr 2894	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑃
117		nfcv 2896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑈
118	113, 116, 117	nfseq 13932	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓seq1(𝑃, 𝑈)
119		nfcv 2896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓𝑛
120	118, 119	nffv 6842	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓(seq1(𝑃, 𝑈)‘𝑛)
121		nfcv 2896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓𝑡
122	120, 121	nffv 6842	. . . . . . . . . . 11 ⊢ Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
123		nfcv 2896	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(seq1( · , (𝐹‘𝑡))‘𝑛)
124	122, 123	nfeq 2910	. . . . . . . . . 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 2896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔1
131		nfmpo2 7437	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
132	114, 131	nfcxfr 2894	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑃
133		nfcv 2896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑈
134	130, 132, 133	nfseq 13932	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔seq1(𝑃, 𝑈)
135		nfcv 2896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔𝑛
136	134, 135	nffv 6842	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔(seq1(𝑃, 𝑈)‘𝑛)
137		nfcv 2896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝑡
138	136, 137	nffv 6842	. . . . . . . . . . 11 ⊢ Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
139		nfcv 2896	. . . . . . . . . . 11 ⊢ Ⅎ𝑔(seq1( · , (𝐹‘𝑡))‘𝑛)
140	138, 139	nfeq 2910	. . . . . . . . . 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 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑇 ∈ V)
146	77	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑈:(1...𝑀)⟶𝑌)
147		fmuldfeq.11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)
148	147	3adant1r 1178	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)
149		simpr1 1195	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑛 ∈ (1...𝑀))
150		simpr2 1196	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → (𝑛 + 1) ∈ (1...𝑀))
151		simpr3 1197	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
152	84	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)
153	126, 142, 143, 114, 49, 145, 146, 148, 149, 150, 151, 152	fmuldfeqlem1 45770	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
154	97, 109, 106, 153	syl21anc 837	. . . . . 6 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
155	154	3exp 1119	. . . . 5 ⊢ (𝑛 ∈ ℕ → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))))
156	19, 26, 33, 40, 96, 155	nnind 12161	. . . 4 ⊢ (𝑀 ∈ ℕ → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)))
157	12, 156	mpcom 38	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
158	11, 157	mpd3an3 1464	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
159		fmuldfeq.4	. . . 4 ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
160	159	fveq1i 6833	. . 3 ⊢ (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡)
161	160	a1i 11	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
162		simpr 484	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇)
163		elnnuz 12789	. . . . . 6 ⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ_≥‘1))
164	2, 163	sylib 218	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
165	164	adantr 480	. . . 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 2896	. . . . . . . 8 ⊢ Ⅎ𝑖𝑘
171	55, 170	nffv 6842	. . . . . . 7 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘)
172	171	nfel1 2913	. . . . . 6 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘) ∈ ℝ
173	169, 172	nfim 1897	. . . . 5 ⊢ Ⅎ𝑖(((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
174		eleq1 2822	. . . . . . 7 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ (1...𝑀) ↔ 𝑘 ∈ (1...𝑀)))
175	174	anbi2d 630	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀))))
176		fveq2 6832	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘𝑘))
177	176	eleq1d 2819	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝐹‘𝑡)‘𝑖) ∈ ℝ ↔ ((𝐹‘𝑡)‘𝑘) ∈ ℝ))
178	175, 177	imbi12d 344	. . . . 5 ⊢ (𝑖 = 𝑘 → ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ) ↔ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)))
179	69	ad2antlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖))
180		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀))
181	77	ffvelcdmda 7027	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝑌)
182		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
183	182, 181	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌))
184		eleq1 2822	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓 ∈ 𝑌 ↔ (𝑈‘𝑖) ∈ 𝑌))
185	184	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌)))
186		feq1 6638	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘𝑖):𝑇⟶ℝ))
187	185, 186	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ)))
188	187, 85	vtoclga 3530	. . . . . . . . . . 11 ⊢ ((𝑈‘𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ))
189	181, 183, 188	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
190	189	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
191		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇)
192	190, 191	ffvelcdmd 7028	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖)‘𝑡) ∈ ℝ)
193	73	fvmpt2 6950	. . . . . . . 8 ⊢ ((𝑖 ∈ (1...𝑀) ∧ ((𝑈‘𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
194	180, 192, 193	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
195	194, 192	eqeltrd 2834	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ∈ ℝ)
196	179, 195	eqeltrd 2834	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ)
197	173, 178, 196	chvarfv 2245	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
198		remulcl 11109	. . . . 5 ⊢ ((𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑘 · 𝑏) ∈ ℝ)
199	198	adantl 481	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑘 · 𝑏) ∈ ℝ)
200	165, 197, 199	seqcl 13943	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ)
201		fmuldfeq.6	. . . 4 ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))
202	201	fvmpt2 6950	. . 3 ⊢ ((𝑡 ∈ 𝑇 ∧ (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
203	162, 200, 202	syl2anc 584	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
204	158, 161, 203	3eqtr4d 2779	1 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 Ⅎwnf 1784 ∈ wcel 2113 Ⅎwnfc 2881 Vcvv 3438 class class class wbr 5096 ↦ cmpt 5177 ⟶wf 6486 ‘cfv 6490 (class class class)co 7356 ∈ cmpo 7358 ℝcr 11023 1c1 11025 + caddc 11027 · cmul 11029 ≤ cle 11165 ℕcn 12143 ℤcz 12486 ℤ_≥cuz 12749 ...cfz 13421 seqcseq 13922

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-er 8633 df-en 8882 df-dom 8883 df-sdom 8884 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-nn 12144 df-n0 12400 df-z 12487 df-uz 12750 df-fz 13422 df-seq 13923

This theorem is referenced by: stoweidlem42 46228 stoweidlem48 46234

W3C validator