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 43014

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 12281	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℤ)
2		fmuldfeq.8	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3	2	nnzd 12354	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
4	3	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ ℤ)
5	2	nnge1d 11951	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
6	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ≤ 𝑀)
7		nnre 11910	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8		leid 11001	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑀 ≤ 𝑀)
9	2, 7, 8	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
10	9	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ≤ 𝑀)
11	1, 4, 4, 6, 10	elfzd 13176	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ (1...𝑀))
12	2	3ad2ant1 1131	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → 𝑀 ∈ ℕ)
13		eleq1 2826	. . . . . . 7 ⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑀) ↔ 1 ∈ (1...𝑀)))
14	13	3anbi3d 1440	. . . . . 6 ⊢ (𝑚 = 1 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀))))
15		fveq2 6756	. . . . . . . 8 ⊢ (𝑚 = 1 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘1))
16	15	fveq1d 6758	. . . . . . 7 ⊢ (𝑚 = 1 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
17		fveq2 6756	. . . . . . 7 ⊢ (𝑚 = 1 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘1))
18	16, 17	eqeq12d 2754	. . . . . 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 2826	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑀) ↔ 𝑛 ∈ (1...𝑀)))
21	20	3anbi3d 1440	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀))))
22		fveq2 6756	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑛))
23	22	fveq1d 6758	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡))
24		fveq2 6756	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑛))
25	23, 24	eqeq12d 2754	. . . . . 6 ⊢ (𝑚 = 𝑛 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
26	21, 25	imbi12d 344	. . . . 5 ⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))))
27		eleq1 2826	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑚 ∈ (1...𝑀) ↔ (𝑛 + 1) ∈ (1...𝑀)))
28	27	3anbi3d 1440	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))))
29		fveq2 6756	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘(𝑛 + 1)))
30	29	fveq1d 6758	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡))
31		fveq2 6756	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))
32	30, 31	eqeq12d 2754	. . . . . 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 2826	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (𝑚 ∈ (1...𝑀) ↔ 𝑀 ∈ (1...𝑀)))
35	34	3anbi3d 1440	. . . . . 6 ⊢ (𝑚 = 𝑀 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀))))
36		fveq2 6756	. . . . . . . 8 ⊢ (𝑚 = 𝑀 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑀))
37	36	fveq1d 6758	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
38		fveq2 6756	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑀))
39	37, 38	eqeq12d 2754	. . . . . 6 ⊢ (𝑚 = 𝑀 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)))
40	35, 39	imbi12d 344	. . . . 5 ⊢ (𝑚 = 𝑀 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))))
41		1z 12280	. . . . . . . 8 ⊢ 1 ∈ ℤ
42		seq1 13662	. . . . . . . 8 ⊢ (1 ∈ ℤ → (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1))
43	41, 42	ax-mp 5	. . . . . . 7 ⊢ (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1)
44		1zzd 12281	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
45		1le1 11533	. . . . . . . . . . . . 13 ⊢ 1 ≤ 1
46	45	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ 1)
47	44, 3, 44, 46, 5	elfzd 13176	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...𝑀))
48		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖 𝑡 ∈ 𝑇
49		fmuldfeq.5	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
50		nfcv 2906	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑇
51		nfmpt1 5178	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
52	50, 51	nfmpt 5177	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
53	49, 52	nfcxfr 2904	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝐹
54		nfcv 2906	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖𝑡
55	53, 54	nffv 6766	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝐹‘𝑡)
56		nfcv 2906	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖1
57	55, 56	nffv 6766	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1)
58		nffvmpt1 6767	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
59	57, 58	nfeq 2919	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)
60	48, 59	nfim 1900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
61		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘1))
62		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))
63	61, 62	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ (𝑖 = 1 → (((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ↔ ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))
64	63	imbi2d 340	. . . . . . . . . . . 12 ⊢ (𝑖 = 1 → ((𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) ↔ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))))
65		ovex 7288	. . . . . . . . . . . . . . 15 ⊢ (1...𝑀) ∈ V
66	65	mptex 7081	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V
67	49	fvmpt2 6868	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ 𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V) → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
68	66, 67	mpan2 687	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝑇 → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))
69	68	fveq1d 6758	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖))
70	60, 64, 69	vtoclg1f 3494	. . . . . . . . . . 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 2738	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))
74		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑖 = 1 → (𝑈‘𝑖) = (𝑈‘1))
75	74	fveq1d 6758	. . . . . . . . . 10 ⊢ (𝑖 = 1 → ((𝑈‘𝑖)‘𝑡) = ((𝑈‘1)‘𝑡))
76	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ (1...𝑀))
77		fmuldfeq.9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)
78	77, 47	ffvelrnd 6944	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘1) ∈ 𝑌)
79	78	ancli 548	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝜑 ∧ (𝑈‘1) ∈ 𝑌))
80		eleq1 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑈‘1) → (𝑓 ∈ 𝑌 ↔ (𝑈‘1) ∈ 𝑌))
81	80	anbi2d 628	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘1) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘1) ∈ 𝑌)))
82		feq1 6565	. . . . . . . . . . . . . 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 3503	. . . . . . . . . . . 12 ⊢ ((𝑈‘1) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ))
87	78, 79, 86	sylc 65	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘1):𝑇⟶ℝ)
88	87	ffvelrnda 6943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑈‘1)‘𝑡) ∈ ℝ)
89	73, 75, 76, 88	fvmptd3 6880	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1) = ((𝑈‘1)‘𝑡))
90	72, 89	eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑈‘1)‘𝑡))
91		seq1 13662	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → (seq1(𝑃, 𝑈)‘1) = (𝑈‘1))
92	41, 91	ax-mp 5	. . . . . . . . 9 ⊢ (seq1(𝑃, 𝑈)‘1) = (𝑈‘1)
93	92	fveq1i 6757	. . . . . . . 8 ⊢ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = ((𝑈‘1)‘𝑡)
94	90, 93	eqtr4di 2797	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
95	43, 94	eqtr2id 2792	. . . . . 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 511	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)))
101		elnnuz 12551	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
102	101	biimpi 215	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
103	102	anim1i 614	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)) → (𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)))
104		peano2fzr 13198	. . . . . . . . 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 1918	. . . . . . . . 9 ⊢ Ⅎ𝑓𝜑
111		nfv 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑓 𝑛 ∈ (1...𝑀)
112		nfv 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑓(𝑛 + 1) ∈ (1...𝑀)
113		nfcv 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓1
114		fmuldfeq.3	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
115		nfmpo1 7333	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑓(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
116	114, 115	nfcxfr 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑃
117		nfcv 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓𝑈
118	113, 116, 117	nfseq 13659	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓seq1(𝑃, 𝑈)
119		nfcv 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓𝑛
120	118, 119	nffv 6766	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓(seq1(𝑃, 𝑈)‘𝑛)
121		nfcv 2906	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓𝑡
122	120, 121	nffv 6766	. . . . . . . . . . 11 ⊢ Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
123		nfcv 2906	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(seq1( · , (𝐹‘𝑡))‘𝑛)
124	122, 123	nfeq 2919	. . . . . . . . . 10 ⊢ Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)
125	111, 112, 124	nf3an 1905	. . . . . . . . 9 ⊢ Ⅎ𝑓(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
126	110, 125	nfan 1903	. . . . . . . 8 ⊢ Ⅎ𝑓(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))
127		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑔𝜑
128		nfv 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑔 𝑛 ∈ (1...𝑀)
129		nfv 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑔(𝑛 + 1) ∈ (1...𝑀)
130		nfcv 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔1
131		nfmpo2 7334	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))
132	114, 131	nfcxfr 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑃
133		nfcv 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝑈
134	130, 132, 133	nfseq 13659	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔seq1(𝑃, 𝑈)
135		nfcv 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔𝑛
136	134, 135	nffv 6766	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔(seq1(𝑃, 𝑈)‘𝑛)
137		nfcv 2906	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝑡
138	136, 137	nffv 6766	. . . . . . . . . . 11 ⊢ Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
139		nfcv 2906	. . . . . . . . . . 11 ⊢ Ⅎ𝑔(seq1( · , (𝐹‘𝑡))‘𝑛)
140	138, 139	nfeq 2919	. . . . . . . . . 10 ⊢ Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)
141	128, 129, 140	nf3an 1905	. . . . . . . . 9 ⊢ Ⅎ𝑔(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))
142	127, 141	nfan 1903	. . . . . . . 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 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 43013	. . . . . . 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 11921	. . . 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 6757	. . 3 ⊢ (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡)
161	160	a1i 11	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
162		simpr 484	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇)
163		elnnuz 12551	. . . . . 6 ⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ_≥‘1))
164	2, 163	sylib 217	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
165	164	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ (ℤ_≥‘1))
166		fmuldfeq.1	. . . . . . . 8 ⊢ Ⅎ𝑖𝜑
167	166, 48	nfan 1903	. . . . . . 7 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑡 ∈ 𝑇)
168		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑖 𝑘 ∈ (1...𝑀)
169	167, 168	nfan 1903	. . . . . 6 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀))
170		nfcv 2906	. . . . . . . 8 ⊢ Ⅎ𝑖𝑘
171	55, 170	nffv 6766	. . . . . . 7 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘)
172	171	nfel1 2922	. . . . . 6 ⊢ Ⅎ𝑖((𝐹‘𝑡)‘𝑘) ∈ ℝ
173	169, 172	nfim 1900	. . . . 5 ⊢ Ⅎ𝑖(((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
174		eleq1 2826	. . . . . . 7 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ (1...𝑀) ↔ 𝑘 ∈ (1...𝑀)))
175	174	anbi2d 628	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀))))
176		fveq2 6756	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘𝑘))
177	176	eleq1d 2823	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝐹‘𝑡)‘𝑖) ∈ ℝ ↔ ((𝐹‘𝑡)‘𝑘) ∈ ℝ))
178	175, 177	imbi12d 344	. . . . 5 ⊢ (𝑖 = 𝑘 → ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ) ↔ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)))
179	69	ad2antlr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖))
180		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀))
181	77	ffvelrnda 6943	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝑌)
182		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
183	182, 181	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌))
184		eleq1 2826	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓 ∈ 𝑌 ↔ (𝑈‘𝑖) ∈ 𝑌))
185	184	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌)))
186		feq1 6565	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑈‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘𝑖):𝑇⟶ℝ))
187	185, 186	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ)))
188	187, 85	vtoclga 3503	. . . . . . . . . . 11 ⊢ ((𝑈‘𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ))
189	181, 183, 188	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
190	189	adantlr 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ)
191		simplr 765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇)
192	190, 191	ffvelrnd 6944	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖)‘𝑡) ∈ ℝ)
193	73	fvmpt2 6868	. . . . . . . 8 ⊢ ((𝑖 ∈ (1...𝑀) ∧ ((𝑈‘𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
194	180, 192, 193	syl2anc 583	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡))
195	194, 192	eqeltrd 2839	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ∈ ℝ)
196	179, 195	eqeltrd 2839	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ)
197	173, 178, 196	chvarfv 2236	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ)
198		remulcl 10887	. . . . 5 ⊢ ((𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑘 · 𝑏) ∈ ℝ)
199	198	adantl 481	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑘 · 𝑏) ∈ ℝ)
200	165, 197, 199	seqcl 13671	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ)
201		fmuldfeq.6	. . . 4 ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))
202	201	fvmpt2 6868	. . 3 ⊢ ((𝑡 ∈ 𝑇 ∧ (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
203	162, 200, 202	syl2anc 583	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))
204	158, 161, 203	3eqtr4d 2788	1 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1539 Ⅎwnf 1787 ∈ wcel 2108 Ⅎwnfc 2886 Vcvv 3422 class class class wbr 5070 ↦ cmpt 5153 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ∈ cmpo 7257 ℝcr 10801 1c1 10803 + caddc 10805 · cmul 10807 ≤ cle 10941 ℕcn 11903 ℤcz 12249 ℤ_≥cuz 12511 ...cfz 13168 seqcseq 13649

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-n0 12164 df-z 12250 df-uz 12512 df-fz 13169 df-seq 13650

This theorem is referenced by: stoweidlem42 43473 stoweidlem48 43479

W3C validator