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 45829

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 12522	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℤ)
2		fmuldfeq.8	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3	2	nnzd 12514	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
4	3	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ ℤ)
5	2	nnge1d 12193	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
6	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ≤ 𝑀)
7		nnre 12152	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8		leid 11229	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑀 ≤ 𝑀)
9	2, 7, 8	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
10	9	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ≤ 𝑀)
11	1, 4, 4, 6, 10	elfzd 13431	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ (1...𝑀))
12	2	3ad2ant1 1133	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → 𝑀 ∈ ℕ)
13		eleq1 2824	. . . . . . 7 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑀) ↔ 1 ∈ (1...𝑀)))
14	13	3anbi3d 1444	. . . . . 6 ⊢ (𝑚 = 1 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀))))
15		fveq2 6834	. . . . . . . 8 ⊢ (𝑚 = 1 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘1))
16	15	fveq1d 6836	. . . . . . 7 ⊢ (𝑚 = 1 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
17		fveq2 6834	. . . . . . 7 ⊢ (𝑚 = 1 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘1))
18	16, 17	eqeq12d 2752	. . . . . 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 2824	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑀) ↔ 𝑛 ∈ (1...𝑀)))
21	20	3anbi3d 1444	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀))))
22		fveq2 6834	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑛))
23	22	fveq1d 6836	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡))
24		fveq2 6834	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑛))
25	23, 24	eqeq12d 2752	. . . . . 6 ⊢ (𝑚 = 𝑛 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
26	21, 25	imbi12d 344	. . . . 5 ⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))))
27		eleq1 2824	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑚 ∈ (1...𝑀) ↔ (𝑛 + 1) ∈ (1...𝑀)))
28	27	3anbi3d 1444	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))))
29		fveq2 6834	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘(𝑛 + 1)))
30	29	fveq1d 6836	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡))
31		fveq2 6834	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
32	30, 31	eqeq12d 2752	. . . . . 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 2824	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (𝑚 ∈ (1...𝑀) ↔ 𝑀 ∈ (1...𝑀)))
35	34	3anbi3d 1444	. . . . . 6 ⊢ (𝑚 = 𝑀 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀))))
36		fveq2 6834	. . . . . . . 8 ⊢ (𝑚 = 𝑀 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑀))
37	36	fveq1d 6836	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
38		fveq2 6834	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑀))
39	37, 38	eqeq12d 2752	. . . . . 6 ⊢ (𝑚 = 𝑀 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)))
40	35, 39	imbi12d 344	. . . . 5 ⊢ (𝑚 = 𝑀 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))))
41		1z 12521	. . . . . . . 8 ⊢ 1 ∈ ℤ
42		seq1 13937	. . . . . . . 8 ⊢ (1 ∈ ℤ → (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1))
43	41, 42	ax-mp 5	. . . . . . 7 ⊢ (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1)
44		1zzd 12522	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
45		1le1 11765	. . . . . . . . . . . . 13 ⊢ 1 ≤ 1
46	45	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ 1)
47	44, 3, 44, 46, 5	elfzd 13431	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...𝑀))
48		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖 𝑡 ∈ 𝑇
49		fmuldfeq.5	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
50		nfcv 2898	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑇
51		nfmpt1 5197	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
52	50, 51	nfmpt 5196	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
53	49, 52	nfcxfr 2896	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝐹
54		nfcv 2898	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝑡
55	53, 54	nffv 6844	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝐹‘𝑡)
56		nfcv 2898	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖1
57	55, 56	nffv 6844	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1)
58		nffvmpt1 6845	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
59	57, 58	nfeq 2912	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
60	48, 59	nfim 1897	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
61		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘1))
62		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
63	61, 62	eqeq12d 2752	. . . . . . . . . . . . 13 ⊢ (𝑖 = 1 → (((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ↔ ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
64	63	imbi2d 340	. . . . . . . . . . . 12 ⊢ (𝑖 = 1 → ((𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) ↔ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))))
65		ovex 7391	. . . . . . . . . . . . . . 15 ⊢ (1...𝑀) ∈ V
66	65	mptex 7169	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V
67	49	fvmpt2 6952	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ 𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V) → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
68	66, 67	mpan2 691	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝑇 → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
69	68	fveq1d 6836	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖))
70	60, 64, 69	vtoclg1f 3526	. . . . . . . . . . 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 2736	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
74		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑖 = 1 → (𝑈‘𝑖) = (𝑈‘1))
75	74	fveq1d 6836	. . . . . . . . . 10 ⊢ (𝑖 = 1 → ((𝑈‘𝑖)‘𝑡) = ((𝑈‘1)‘𝑡))
76	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ (1...𝑀))
77		fmuldfeq.9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)
78	77, 47	ffvelcdmd 7030	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘1) ∈ 𝑌)
79	78	ancli 548	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝜑 ∧ (𝑈‘1) ∈ 𝑌))
80		eleq1 2824	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑈‘1) → (𝑓 ∈ 𝑌 ↔ (𝑈‘1) ∈ 𝑌))
81	80	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘1) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘1) ∈ 𝑌)))
82		feq1 6640	. . . . . . . . . . . . . 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 3532	. . . . . . . . . . . 12 ⊢ ((𝑈‘1) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ))
87	78, 79, 86	sylc 65	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘1):𝑇⟶ℝ)
88	87	ffvelcdmda 7029	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑈‘1)‘𝑡) ∈ ℝ)
89	73, 75, 76, 88	fvmptd3 6964	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1) = ((𝑈‘1)‘𝑡))
90	72, 89	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑈‘1)‘𝑡))
91		seq1 13937	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → (seq1(𝑃, 𝑈)‘1) = (𝑈‘1))
92	41, 91	ax-mp 5	. . . . . . . . 9 ⊢ (seq1(𝑃, 𝑈)‘1) = (𝑈‘1)
93	92	fveq1i 6835	. . . . . . . 8 ⊢ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = ((𝑈‘1)‘𝑡)
94	90, 93	eqtr4di 2789	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
95	43, 94	eqtr2id 2784	. . . . . 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 12791	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
102	101	biimpi 216	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
103	102	anim1i 615	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)) → (𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)))
104		peano2fzr 13453	. . . . . . . . 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 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓1
114		fmuldfeq.3	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
115		nfmpo1 7438	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑓(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
116	114, 115	nfcxfr 2896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑃
117		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑈
118	113, 116, 117	nfseq 13934	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓seq1(𝑃, 𝑈)
119		nfcv 2898	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓𝑛
120	118, 119	nffv 6844	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓(seq1(𝑃, 𝑈)‘𝑛)
121		nfcv 2898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓𝑡
122	120, 121	nffv 6844	. . . . . . . . . . 11 ⊢ Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
123		nfcv 2898	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(seq1( · , (𝐹‘𝑡))‘𝑛)
124	122, 123	nfeq 2912	. . . . . . . . . 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 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔1
131		nfmpo2 7439	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
132	114, 131	nfcxfr 2896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑃
133		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑈
134	130, 132, 133	nfseq 13934	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔seq1(𝑃, 𝑈)
135		nfcv 2898	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔𝑛
136	134, 135	nffv 6844	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔(seq1(𝑃, 𝑈)‘𝑛)
137		nfcv 2898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝑡
138	136, 137	nffv 6844	. . . . . . . . . . 11 ⊢ Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
139		nfcv 2898	. . . . . . . . . . 11 ⊢ Ⅎ𝑔(seq1( · , (𝐹‘𝑡))‘𝑛)
140	138, 139	nfeq 2912	. . . . . . . . . 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 45828	. . . . . . 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 12163	. . . 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 6835	. . 3 ⊢ (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡)
161	160	a1i 11	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
162		simpr 484	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇)
163		elnnuz 12791	. . . . . 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 2898	. . . . . . . 8 ⊢ Ⅎ𝑖𝑘
171	55, 170	nffv 6844	. . . . . . 7 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘)
172	171	nfel1 2915	. . . . . 6 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘) ∈ ℝ
173	169, 172	nfim 1897	. . . . 5 ⊢ Ⅎ𝑖(((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
174		eleq1 2824	. . . . . . 7 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ (1...𝑀) ↔ 𝑘 ∈ (1...𝑀)))
175	174	anbi2d 630	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀))))
176		fveq2 6834	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘𝑘))
177	176	eleq1d 2821	. . . . . 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 7029	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝑌)
182		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
183	182, 181	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌))
184		eleq1 2824	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓 ∈ 𝑌 ↔ (𝑈‘𝑖) ∈ 𝑌))
185	184	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌)))
186		feq1 6640	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘𝑖):𝑇⟶ℝ))
187	185, 186	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ)))
188	187, 85	vtoclga 3532	. . . . . . . . . . 11 ⊢ ((𝑈‘𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ))
189	181, 183, 188	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
190	189	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
191		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇)
192	190, 191	ffvelcdmd 7030	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖)‘𝑡) ∈ ℝ)
193	73	fvmpt2 6952	. . . . . . . 8 ⊢ ((𝑖 ∈ (1...𝑀) ∧ ((𝑈‘𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
194	180, 192, 193	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
195	194, 192	eqeltrd 2836	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ∈ ℝ)
196	179, 195	eqeltrd 2836	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ)
197	173, 178, 196	chvarfv 2247	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
198		remulcl 11111	. . . . 5 ⊢ ((𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑘 · 𝑏) ∈ ℝ)
199	198	adantl 481	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑘 · 𝑏) ∈ ℝ)
200	165, 197, 199	seqcl 13945	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ)
201		fmuldfeq.6	. . . 4 ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))
202	201	fvmpt2 6952	. . 3 ⊢ ((𝑡 ∈ 𝑇 ∧ (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
203	162, 200, 202	syl2anc 584	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
204	158, 161, 203	3eqtr4d 2781	1 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 Ⅎwnf 1784 ∈ wcel 2113 Ⅎwnfc 2883 Vcvv 3440 class class class wbr 5098 ↦ cmpt 5179 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 ∈ cmpo 7360 ℝcr 11025 1c1 11027 + caddc 11029 · cmul 11031 ≤ cle 11167 ℕcn 12145 ℤcz 12488 ℤ_≥cuz 12751 ...cfz 13423 seqcseq 13924

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 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-er 8635 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-nn 12146 df-n0 12402 df-z 12489 df-uz 12752 df-fz 13424 df-seq 13925

This theorem is referenced by: stoweidlem42 46286 stoweidlem48 46292

W3C validator