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

Metamath Proof Explorer

Theorem fmuldfeq

Proof