fmuldfeq

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)

	Ref	Expression
Hypotheses	fmuldfeq.1	$⊢ Ⅎ i φ$
	fmuldfeq.2	$⊢ \underline{Ⅎ} t Y$
	fmuldfeq.3	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
	fmuldfeq.4	$⊢ X = seq 1 (P, U) (M)$
	fmuldfeq.5	$⊢ F = (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
	fmuldfeq.6	$⊢ Z = (t \in T ⟼ seq 1 (\times F (t)) (M))$
	fmuldfeq.7	$⊢ φ \to T \in V$
	fmuldfeq.8	$⊢ φ \to M \in ℕ$
	fmuldfeq.9	$⊢ φ \to U : (1 \dots M) ⟶ Y$
	fmuldfeq.10	$⊢ (φ \land f \in Y) \to f : T ⟶ ℝ$
	fmuldfeq.11	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
Assertion	fmuldfeq	$⊢ (φ \land t \in T) \to X (t) = Z (t)$

Proof

Step	Hyp	Ref	Expression
1		fmuldfeq.1	$⊢ Ⅎ i φ$
2		fmuldfeq.2	$⊢ \underline{Ⅎ} t Y$
3		fmuldfeq.3	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
4		fmuldfeq.4	$⊢ X = seq 1 (P, U) (M)$
5		fmuldfeq.5	$⊢ F = (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
6		fmuldfeq.6	$⊢ Z = (t \in T ⟼ seq 1 (\times F (t)) (M))$
7		fmuldfeq.7	$⊢ φ \to T \in V$
8		fmuldfeq.8	$⊢ φ \to M \in ℕ$
9		fmuldfeq.9	$⊢ φ \to U : (1 \dots M) ⟶ Y$
10		fmuldfeq.10	$⊢ (φ \land f \in Y) \to f : T ⟶ ℝ$
11		fmuldfeq.11	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
12	8	nnge1d	$⊢ φ \to 1 \leq M$
13	12	adantr	$⊢ (φ \land t \in T) \to 1 \leq M$
14		nnre	$⊢ M \in ℕ \to M \in ℝ$
15		leid	$⊢ M \in ℝ \to M \leq M$
16	8 14 15	3syl	$⊢ φ \to M \leq M$
17	16	adantr	$⊢ (φ \land t \in T) \to M \leq M$
18	8	nnzd	$⊢ φ \to M \in ℤ$
19	18	adantr	$⊢ (φ \land t \in T) \to M \in ℤ$
20		1zzd	$⊢ (φ \land t \in T) \to 1 \in ℤ$
21		elfz	$⊢ (M \in ℤ \land 1 \in ℤ \land M \in ℤ) \to (M \in (1 \dots M) \leftrightarrow (1 \leq M \land M \leq M))$
22	19 20 19 21	syl3anc	$⊢ (φ \land t \in T) \to (M \in (1 \dots M) \leftrightarrow (1 \leq M \land M \leq M))$
23	13 17 22	mpbir2and	$⊢ (φ \land t \in T) \to M \in (1 \dots M)$
24	8	3ad2ant1	$⊢ (φ \land t \in T \land M \in (1 \dots M)) \to M \in ℕ$
25		eleq1	$⊢ m = 1 \to (m \in (1 \dots M) \leftrightarrow 1 \in (1 \dots M))$
26	25	3anbi3d	$⊢ m = 1 \to ((φ \land t \in T \land m \in (1 \dots M)) \leftrightarrow (φ \land t \in T \land 1 \in (1 \dots M)))$
27		fveq2	$⊢ m = 1 \to seq 1 (P, U) (m) = seq 1 (P, U) (1)$
28	27	fveq1d	$⊢ m = 1 \to seq 1 (P, U) (m) (t) = seq 1 (P, U) (1) (t)$
29		fveq2	$⊢ m = 1 \to seq 1 (\times F (t)) (m) = seq 1 (\times F (t)) (1)$
30	28 29	eqeq12d	$⊢ m = 1 \to (seq 1 (P, U) (m) (t) = seq 1 (\times F (t)) (m) \leftrightarrow seq 1 (P, U) (1) (t) = seq 1 (\times F (t)) (1))$
31	26 30	imbi12d	$⊢ m = 1 \to (((φ \land t \in T \land m \in (1 \dots M)) \to seq 1 (P, U) (m) (t) = seq 1 (\times F (t)) (m)) \leftrightarrow ((φ \land t \in T \land 1 \in (1 \dots M)) \to seq 1 (P, U) (1) (t) = seq 1 (\times F (t)) (1)))$
32		eleq1	$⊢ m = n \to (m \in (1 \dots M) \leftrightarrow n \in (1 \dots M))$
33	32	3anbi3d	$⊢ m = n \to ((φ \land t \in T \land m \in (1 \dots M)) \leftrightarrow (φ \land t \in T \land n \in (1 \dots M)))$
34		fveq2	$⊢ m = n \to seq 1 (P, U) (m) = seq 1 (P, U) (n)$
35	34	fveq1d	$⊢ m = n \to seq 1 (P, U) (m) (t) = seq 1 (P, U) (n) (t)$
36		fveq2	$⊢ m = n \to seq 1 (\times F (t)) (m) = seq 1 (\times F (t)) (n)$
37	35 36	eqeq12d	$⊢ m = n \to (seq 1 (P, U) (m) (t) = seq 1 (\times F (t)) (m) \leftrightarrow seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))$
38	33 37	imbi12d	$⊢ m = n \to (((φ \land t \in T \land m \in (1 \dots M)) \to seq 1 (P, U) (m) (t) = seq 1 (\times F (t)) (m)) \leftrightarrow ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)))$
39		eleq1	$⊢ m = n + 1 \to (m \in (1 \dots M) \leftrightarrow n + 1 \in (1 \dots M))$
40	39	3anbi3d	$⊢ m = n + 1 \to ((φ \land t \in T \land m \in (1 \dots M)) \leftrightarrow (φ \land t \in T \land n + 1 \in (1 \dots M)))$
41		fveq2	$⊢ m = n + 1 \to seq 1 (P, U) (m) = seq 1 (P, U) (n + 1)$
42	41	fveq1d	$⊢ m = n + 1 \to seq 1 (P, U) (m) (t) = seq 1 (P, U) (n + 1) (t)$
43		fveq2	$⊢ m = n + 1 \to seq 1 (\times F (t)) (m) = seq 1 (\times F (t)) (n + 1)$
44	42 43	eqeq12d	$⊢ m = n + 1 \to (seq 1 (P, U) (m) (t) = seq 1 (\times F (t)) (m) \leftrightarrow seq 1 (P, U) (n + 1) (t) = seq 1 (\times F (t)) (n + 1))$
45	40 44	imbi12d	$⊢ m = n + 1 \to (((φ \land t \in T \land m \in (1 \dots M)) \to seq 1 (P, U) (m) (t) = seq 1 (\times F (t)) (m)) \leftrightarrow ((φ \land t \in T \land n + 1 \in (1 \dots M)) \to seq 1 (P, U) (n + 1) (t) = seq 1 (\times F (t)) (n + 1)))$
46		eleq1	$⊢ m = M \to (m \in (1 \dots M) \leftrightarrow M \in (1 \dots M))$
47	46	3anbi3d	$⊢ m = M \to ((φ \land t \in T \land m \in (1 \dots M)) \leftrightarrow (φ \land t \in T \land M \in (1 \dots M)))$
48		fveq2	$⊢ m = M \to seq 1 (P, U) (m) = seq 1 (P, U) (M)$
49	48	fveq1d	$⊢ m = M \to seq 1 (P, U) (m) (t) = seq 1 (P, U) (M) (t)$
50		fveq2	$⊢ m = M \to seq 1 (\times F (t)) (m) = seq 1 (\times F (t)) (M)$
51	49 50	eqeq12d	$⊢ m = M \to (seq 1 (P, U) (m) (t) = seq 1 (\times F (t)) (m) \leftrightarrow seq 1 (P, U) (M) (t) = seq 1 (\times F (t)) (M))$
52	47 51	imbi12d	$⊢ m = M \to (((φ \land t \in T \land m \in (1 \dots M)) \to seq 1 (P, U) (m) (t) = seq 1 (\times F (t)) (m)) \leftrightarrow ((φ \land t \in T \land M \in (1 \dots M)) \to seq 1 (P, U) (M) (t) = seq 1 (\times F (t)) (M)))$
53		1z	$⊢ 1 \in ℤ$
54		seq1	$⊢ 1 \in ℤ \to seq 1 (\times F (t)) (1) = F (t) (1)$
55	53 54	ax-mp	$⊢ seq 1 (\times F (t)) (1) = F (t) (1)$
56		1le1	$⊢ 1 \leq 1$
57	56	a1i	$⊢ φ \to 1 \leq 1$
58		1zzd	$⊢ φ \to 1 \in ℤ$
59		elfz	$⊢ (1 \in ℤ \land 1 \in ℤ \land M \in ℤ) \to (1 \in (1 \dots M) \leftrightarrow (1 \leq 1 \land 1 \leq M))$
60	58 58 18 59	syl3anc	$⊢ φ \to (1 \in (1 \dots M) \leftrightarrow (1 \leq 1 \land 1 \leq M))$
61	57 12 60	mpbir2and	$⊢ φ \to 1 \in (1 \dots M)$
62		nfv	$⊢ Ⅎ i t \in T$
63		nfcv	$⊢ \underline{Ⅎ} i T$
64		nfmpt1	$⊢ \underline{Ⅎ} i (i \in (1 \dots M) ⟼ U (i) (t))$
65	63 64	nfmpt	$⊢ \underline{Ⅎ} i (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
66	5 65	nfcxfr	$⊢ \underline{Ⅎ} i F$
67		nfcv	$⊢ \underline{Ⅎ} i t$
68	66 67	nffv	$⊢ \underline{Ⅎ} i F (t)$
69		nfcv	$⊢ \underline{Ⅎ} i 1$
70	68 69	nffv	$⊢ \underline{Ⅎ} i F (t) (1)$
71		nffvmpt1	$⊢ \underline{Ⅎ} i (i \in (1 \dots M) ⟼ U (i) (t)) (1)$
72	70 71	nfeq	$⊢ Ⅎ i F (t) (1) = (i \in (1 \dots M) ⟼ U (i) (t)) (1)$
73	62 72	nfim	$⊢ Ⅎ i (t \in T \to F (t) (1) = (i \in (1 \dots M) ⟼ U (i) (t)) (1))$
74		fveq2	$⊢ i = 1 \to F (t) (i) = F (t) (1)$
75		fveq2	$⊢ i = 1 \to (i \in (1 \dots M) ⟼ U (i) (t)) (i) = (i \in (1 \dots M) ⟼ U (i) (t)) (1)$
76	74 75	eqeq12d	$⊢ i = 1 \to (F (t) (i) = (i \in (1 \dots M) ⟼ U (i) (t)) (i) \leftrightarrow F (t) (1) = (i \in (1 \dots M) ⟼ U (i) (t)) (1))$
77	76	imbi2d	$⊢ i = 1 \to ((t \in T \to F (t) (i) = (i \in (1 \dots M) ⟼ U (i) (t)) (i)) \leftrightarrow (t \in T \to F (t) (1) = (i \in (1 \dots M) ⟼ U (i) (t)) (1)))$
78		ovex	$⊢ (1 \dots M) \in V$
79	78	mptex	$⊢ (i \in (1 \dots M) ⟼ U (i) (t)) \in V$
80	5	fvmpt2	$⊢ (t \in T \land (i \in (1 \dots M) ⟼ U (i) (t)) \in V) \to F (t) = (i \in (1 \dots M) ⟼ U (i) (t))$
81	79 80	mpan2	$⊢ t \in T \to F (t) = (i \in (1 \dots M) ⟼ U (i) (t))$
82	81	fveq1d	$⊢ t \in T \to F (t) (i) = (i \in (1 \dots M) ⟼ U (i) (t)) (i)$
83	73 77 82	vtoclg1f	$⊢ 1 \in (1 \dots M) \to (t \in T \to F (t) (1) = (i \in (1 \dots M) ⟼ U (i) (t)) (1))$
84	61 83	syl	$⊢ φ \to (t \in T \to F (t) (1) = (i \in (1 \dots M) ⟼ U (i) (t)) (1))$
85	84	imp	$⊢ (φ \land t \in T) \to F (t) (1) = (i \in (1 \dots M) ⟼ U (i) (t)) (1)$
86		eqid	$⊢ (i \in (1 \dots M) ⟼ U (i) (t)) = (i \in (1 \dots M) ⟼ U (i) (t))$
87		fveq2	$⊢ i = 1 \to U (i) = U (1)$
88	87	fveq1d	$⊢ i = 1 \to U (i) (t) = U (1) (t)$
89	61	adantr	$⊢ (φ \land t \in T) \to 1 \in (1 \dots M)$
90	9 61	ffvelrnd	$⊢ φ \to U (1) \in Y$
91	90	ancli	$⊢ φ \to (φ \land U (1) \in Y)$
92		eleq1	$⊢ f = U (1) \to (f \in Y \leftrightarrow U (1) \in Y)$
93	92	anbi2d	$⊢ f = U (1) \to ((φ \land f \in Y) \leftrightarrow (φ \land U (1) \in Y))$
94		feq1	$⊢ f = U (1) \to (f : T ⟶ ℝ \leftrightarrow U (1) : T ⟶ ℝ)$
95	93 94	imbi12d	$⊢ f = U (1) \to (((φ \land f \in Y) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land U (1) \in Y) \to U (1) : T ⟶ ℝ))$
96	10	a1i	$⊢ f \in Y \to ((φ \land f \in Y) \to f : T ⟶ ℝ)$
97	95 96	vtoclga	$⊢ U (1) \in Y \to ((φ \land U (1) \in Y) \to U (1) : T ⟶ ℝ)$
98	90 91 97	sylc	$⊢ φ \to U (1) : T ⟶ ℝ$
99	98	ffvelrnda	$⊢ (φ \land t \in T) \to U (1) (t) \in ℝ$
100	86 88 89 99	fvmptd3	$⊢ (φ \land t \in T) \to (i \in (1 \dots M) ⟼ U (i) (t)) (1) = U (1) (t)$
101	85 100	eqtrd	$⊢ (φ \land t \in T) \to F (t) (1) = U (1) (t)$
102		seq1	$⊢ 1 \in ℤ \to seq 1 (P, U) (1) = U (1)$
103	53 102	ax-mp	$⊢ seq 1 (P, U) (1) = U (1)$
104	103	fveq1i	$⊢ seq 1 (P, U) (1) (t) = U (1) (t)$
105	101 104	eqtr4di	$⊢ (φ \land t \in T) \to F (t) (1) = seq 1 (P, U) (1) (t)$
106	55 105	syl5req	$⊢ (φ \land t \in T) \to seq 1 (P, U) (1) (t) = seq 1 (\times F (t)) (1)$
107	106	3adant3	$⊢ (φ \land t \in T \land 1 \in (1 \dots M)) \to seq 1 (P, U) (1) (t) = seq 1 (\times F (t)) (1)$
108		simp31	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to φ$
109		simp1	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to n \in ℕ$
110		simp33	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to n + 1 \in (1 \dots M)$
111	109 110	jca	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to (n \in ℕ \land n + 1 \in (1 \dots M))$
112		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
113	112	biimpi	$⊢ n \in ℕ \to n \in ℤ_{\geq 1}$
114	113	anim1i	$⊢ (n \in ℕ \land n + 1 \in (1 \dots M)) \to (n \in ℤ_{\geq 1} \land n + 1 \in (1 \dots M))$
115		peano2fzr	$⊢ (n \in ℤ_{\geq 1} \land n + 1 \in (1 \dots M)) \to n \in (1 \dots M)$
116	111 114 115	3syl	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to n \in (1 \dots M)$
117		simp32	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to t \in T$
118		simp2	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))$
119	108 117 116 118	mp3and	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)$
120	116 110 119	3jca	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))$
121		nfv	$⊢ Ⅎ f φ$
122		nfv	$⊢ Ⅎ f n \in (1 \dots M)$
123		nfv	$⊢ Ⅎ f n + 1 \in (1 \dots M)$
124		nfcv	$⊢ \underline{Ⅎ} f 1$
125		nfmpo1	$⊢ \underline{Ⅎ} f (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
126	3 125	nfcxfr	$⊢ \underline{Ⅎ} f P$
127		nfcv	$⊢ \underline{Ⅎ} f U$
128	124 126 127	nfseq	$⊢ \underline{Ⅎ} f seq 1 (P, U)$
129		nfcv	$⊢ \underline{Ⅎ} f n$
130	128 129	nffv	$⊢ \underline{Ⅎ} f seq 1 (P, U) (n)$
131		nfcv	$⊢ \underline{Ⅎ} f t$
132	130 131	nffv	$⊢ \underline{Ⅎ} f seq 1 (P, U) (n) (t)$
133		nfcv	$⊢ \underline{Ⅎ} f seq 1 (\times F (t)) (n)$
134	132 133	nfeq	$⊢ Ⅎ f seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)$
135	122 123 134	nf3an	$⊢ Ⅎ f (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))$
136	121 135	nfan	$⊢ Ⅎ f (φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)))$
137		nfv	$⊢ Ⅎ g φ$
138		nfv	$⊢ Ⅎ g n \in (1 \dots M)$
139		nfv	$⊢ Ⅎ g n + 1 \in (1 \dots M)$
140		nfcv	$⊢ \underline{Ⅎ} g 1$
141		nfmpo2	$⊢ \underline{Ⅎ} g (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
142	3 141	nfcxfr	$⊢ \underline{Ⅎ} g P$
143		nfcv	$⊢ \underline{Ⅎ} g U$
144	140 142 143	nfseq	$⊢ \underline{Ⅎ} g seq 1 (P, U)$
145		nfcv	$⊢ \underline{Ⅎ} g n$
146	144 145	nffv	$⊢ \underline{Ⅎ} g seq 1 (P, U) (n)$
147		nfcv	$⊢ \underline{Ⅎ} g t$
148	146 147	nffv	$⊢ \underline{Ⅎ} g seq 1 (P, U) (n) (t)$
149		nfcv	$⊢ \underline{Ⅎ} g seq 1 (\times F (t)) (n)$
150	148 149	nfeq	$⊢ Ⅎ g seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)$
151	138 139 150	nf3an	$⊢ Ⅎ g (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))$
152	137 151	nfan	$⊢ Ⅎ g (φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)))$
153	7	adantr	$⊢ (φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))) \to T \in V$
154	9	adantr	$⊢ (φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))) \to U : (1 \dots M) ⟶ Y$
155	11	3adant1r	$⊢ ((φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))) \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
156		simpr1	$⊢ (φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))) \to n \in (1 \dots M)$
157		simpr2	$⊢ (φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))) \to n + 1 \in (1 \dots M)$
158		simpr3	$⊢ (φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)$
159	10	adantlr	$⊢ ((φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))) \land f \in Y) \to f : T ⟶ ℝ$
160	136 152 2 3 5 153 154 155 156 157 158 159	fmuldfeqlem1	$⊢ ((φ \land (n \in (1 \dots M) \land n + 1 \in (1 \dots M) \land seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n))) \land t \in T) \to seq 1 (P, U) (n + 1) (t) = seq 1 (\times F (t)) (n + 1)$
161	108 120 117 160	syl21anc	$⊢ (n \in ℕ \land ((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \land (φ \land t \in T \land n + 1 \in (1 \dots M))) \to seq 1 (P, U) (n + 1) (t) = seq 1 (\times F (t)) (n + 1)$
162	161	3exp	$⊢ n \in ℕ \to (((φ \land t \in T \land n \in (1 \dots M)) \to seq 1 (P, U) (n) (t) = seq 1 (\times F (t)) (n)) \to ((φ \land t \in T \land n + 1 \in (1 \dots M)) \to seq 1 (P, U) (n + 1) (t) = seq 1 (\times F (t)) (n + 1)))$
163	31 38 45 52 107 162	nnind	$⊢ M \in ℕ \to ((φ \land t \in T \land M \in (1 \dots M)) \to seq 1 (P, U) (M) (t) = seq 1 (\times F (t)) (M))$
164	24 163	mpcom	$⊢ (φ \land t \in T \land M \in (1 \dots M)) \to seq 1 (P, U) (M) (t) = seq 1 (\times F (t)) (M)$
165	23 164	mpd3an3	$⊢ (φ \land t \in T) \to seq 1 (P, U) (M) (t) = seq 1 (\times F (t)) (M)$
166	4	fveq1i	$⊢ X (t) = seq 1 (P, U) (M) (t)$
167	166	a1i	$⊢ (φ \land t \in T) \to X (t) = seq 1 (P, U) (M) (t)$
168		simpr	$⊢ (φ \land t \in T) \to t \in T$
169		elnnuz	$⊢ M \in ℕ \leftrightarrow M \in ℤ_{\geq 1}$
170	8 169	sylib	$⊢ φ \to M \in ℤ_{\geq 1}$
171	170	adantr	$⊢ (φ \land t \in T) \to M \in ℤ_{\geq 1}$
172	1 62	nfan	$⊢ Ⅎ i (φ \land t \in T)$
173		nfv	$⊢ Ⅎ i k \in (1 \dots M)$
174	172 173	nfan	$⊢ Ⅎ i ((φ \land t \in T) \land k \in (1 \dots M))$
175		nfcv	$⊢ \underline{Ⅎ} i k$
176	68 175	nffv	$⊢ \underline{Ⅎ} i F (t) (k)$
177	176	nfel1	$⊢ Ⅎ i F (t) (k) \in ℝ$
178	174 177	nfim	$⊢ Ⅎ i (((φ \land t \in T) \land k \in (1 \dots M)) \to F (t) (k) \in ℝ)$
179		eleq1	$⊢ i = k \to (i \in (1 \dots M) \leftrightarrow k \in (1 \dots M))$
180	179	anbi2d	$⊢ i = k \to (((φ \land t \in T) \land i \in (1 \dots M)) \leftrightarrow ((φ \land t \in T) \land k \in (1 \dots M)))$
181		fveq2	$⊢ i = k \to F (t) (i) = F (t) (k)$
182	181	eleq1d	$⊢ i = k \to (F (t) (i) \in ℝ \leftrightarrow F (t) (k) \in ℝ)$
183	180 182	imbi12d	$⊢ i = k \to ((((φ \land t \in T) \land i \in (1 \dots M)) \to F (t) (i) \in ℝ) \leftrightarrow (((φ \land t \in T) \land k \in (1 \dots M)) \to F (t) (k) \in ℝ))$
184	82	ad2antlr	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to F (t) (i) = (i \in (1 \dots M) ⟼ U (i) (t)) (i)$
185		simpr	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to i \in (1 \dots M)$
186	9	ffvelrnda	$⊢ (φ \land i \in (1 \dots M)) \to U (i) \in Y$
187		simpl	$⊢ (φ \land i \in (1 \dots M)) \to φ$
188	187 186	jca	$⊢ (φ \land i \in (1 \dots M)) \to (φ \land U (i) \in Y)$
189		eleq1	$⊢ f = U (i) \to (f \in Y \leftrightarrow U (i) \in Y)$
190	189	anbi2d	$⊢ f = U (i) \to ((φ \land f \in Y) \leftrightarrow (φ \land U (i) \in Y))$
191		feq1	$⊢ f = U (i) \to (f : T ⟶ ℝ \leftrightarrow U (i) : T ⟶ ℝ)$
192	190 191	imbi12d	$⊢ f = U (i) \to (((φ \land f \in Y) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land U (i) \in Y) \to U (i) : T ⟶ ℝ))$
193	192 96	vtoclga	$⊢ U (i) \in Y \to ((φ \land U (i) \in Y) \to U (i) : T ⟶ ℝ)$
194	186 188 193	sylc	$⊢ (φ \land i \in (1 \dots M)) \to U (i) : T ⟶ ℝ$
195	194	adantlr	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to U (i) : T ⟶ ℝ$
196		simplr	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to t \in T$
197	195 196	ffvelrnd	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to U (i) (t) \in ℝ$
198	86	fvmpt2	$⊢ (i \in (1 \dots M) \land U (i) (t) \in ℝ) \to (i \in (1 \dots M) ⟼ U (i) (t)) (i) = U (i) (t)$
199	185 197 198	syl2anc	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to (i \in (1 \dots M) ⟼ U (i) (t)) (i) = U (i) (t)$
200	199 197	eqeltrd	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to (i \in (1 \dots M) ⟼ U (i) (t)) (i) \in ℝ$
201	184 200	eqeltrd	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to F (t) (i) \in ℝ$
202	178 183 201	chvarfv	$⊢ ((φ \land t \in T) \land k \in (1 \dots M)) \to F (t) (k) \in ℝ$
203		remulcl	$⊢ (k \in ℝ \land b \in ℝ) \to k b \in ℝ$
204	203	adantl	$⊢ ((φ \land t \in T) \land (k \in ℝ \land b \in ℝ)) \to k b \in ℝ$
205	171 202 204	seqcl	$⊢ (φ \land t \in T) \to seq 1 (\times F (t)) (M) \in ℝ$
206	6	fvmpt2	$⊢ (t \in T \land seq 1 (\times F (t)) (M) \in ℝ) \to Z (t) = seq 1 (\times F (t)) (M)$
207	168 205 206	syl2anc	$⊢ (φ \land t \in T) \to Z (t) = seq 1 (\times F (t)) (M)$
208	165 167 207	3eqtr4d	$⊢ (φ \land t \in T) \to X (t) = Z (t)$

Metamath Proof Explorer

Theorem fmuldfeq

Proof