fmuldfeqlem1

Description: induction step for the proof of fmuldfeq . (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		fmuldfeqlem1.1	$⊢ Ⅎ f φ$
2		fmuldfeqlem1.2	$⊢ Ⅎ g φ$
3		fmuldfeqlem1.3	$⊢ \underline{Ⅎ} t Y$
4		fmuldfeqlem1.5	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
5		fmuldfeqlem1.6	$⊢ F = (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
6		fmuldfeqlem1.7	$⊢ φ \to T \in V$
7		fmuldfeqlem1.8	$⊢ φ \to U : (1 \dots M) ⟶ Y$
8		fmuldfeqlem1.9	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
9		fmuldfeqlem1.10	$⊢ φ \to N \in (1 \dots M)$
10		fmuldfeqlem1.11	$⊢ φ \to N + 1 \in (1 \dots M)$
11		fmuldfeqlem1.12	$⊢ φ \to seq 1 (P, U) (N) (t) = seq 1 (\times F (t)) (N)$
12		fmuldfeqlem1.13	$⊢ (φ \land f \in Y) \to f : T ⟶ ℝ$
13		ovex	$⊢ (1 \dots M) \in V$
14	13	mptex	$⊢ (i \in (1 \dots M) ⟼ U (i) (t)) \in V$
15	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))$
16	14 15	mpan2	$⊢ t \in T \to F (t) = (i \in (1 \dots M) ⟼ U (i) (t))$
17		fveq2	$⊢ i = j \to U (i) = U (j)$
18	17	fveq1d	$⊢ i = j \to U (i) (t) = U (j) (t)$
19	18	cbvmptv	$⊢ (i \in (1 \dots M) ⟼ U (i) (t)) = (j \in (1 \dots M) ⟼ U (j) (t))$
20	16 19	eqtrdi	$⊢ t \in T \to F (t) = (j \in (1 \dots M) ⟼ U (j) (t))$
21	20	adantl	$⊢ (φ \land t \in T) \to F (t) = (j \in (1 \dots M) ⟼ U (j) (t))$
22		fveq2	$⊢ j = N + 1 \to U (j) = U (N + 1)$
23	22	fveq1d	$⊢ j = N + 1 \to U (j) (t) = U (N + 1) (t)$
24	23	adantl	$⊢ ((φ \land t \in T) \land j = N + 1) \to U (j) (t) = U (N + 1) (t)$
25	10	adantr	$⊢ (φ \land t \in T) \to N + 1 \in (1 \dots M)$
26	7 10	ffvelrnd	$⊢ φ \to U (N + 1) \in Y$
27	26	ancli	$⊢ φ \to (φ \land U (N + 1) \in Y)$
28		nfcv	$⊢ \underline{Ⅎ} f U (N + 1)$
29		nfv	$⊢ Ⅎ f U (N + 1) \in Y$
30	1 29	nfan	$⊢ Ⅎ f (φ \land U (N + 1) \in Y)$
31		nfv	$⊢ Ⅎ f U (N + 1) : T ⟶ ℝ$
32	30 31	nfim	$⊢ Ⅎ f ((φ \land U (N + 1) \in Y) \to U (N + 1) : T ⟶ ℝ)$
33		eleq1	$⊢ f = U (N + 1) \to (f \in Y \leftrightarrow U (N + 1) \in Y)$
34	33	anbi2d	$⊢ f = U (N + 1) \to ((φ \land f \in Y) \leftrightarrow (φ \land U (N + 1) \in Y))$
35		feq1	$⊢ f = U (N + 1) \to (f : T ⟶ ℝ \leftrightarrow U (N + 1) : T ⟶ ℝ)$
36	34 35	imbi12d	$⊢ f = U (N + 1) \to (((φ \land f \in Y) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land U (N + 1) \in Y) \to U (N + 1) : T ⟶ ℝ))$
37	28 32 36 12	vtoclgf	$⊢ U (N + 1) \in Y \to ((φ \land U (N + 1) \in Y) \to U (N + 1) : T ⟶ ℝ)$
38	26 27 37	sylc	$⊢ φ \to U (N + 1) : T ⟶ ℝ$
39	38	ffvelrnda	$⊢ (φ \land t \in T) \to U (N + 1) (t) \in ℝ$
40	21 24 25 39	fvmptd	$⊢ (φ \land t \in T) \to F (t) (N + 1) = U (N + 1) (t)$
41	40	oveq2d	$⊢ (φ \land t \in T) \to seq 1 (\times F (t)) (N) F (t) (N + 1) = seq 1 (\times F (t)) (N) U (N + 1) (t)$
42		elfzuz	$⊢ N \in (1 \dots M) \to N \in ℤ_{\geq 1}$
43	9 42	syl	$⊢ φ \to N \in ℤ_{\geq 1}$
44		seqp1	$⊢ N \in ℤ_{\geq 1} \to seq 1 (\times F (t)) (N + 1) = seq 1 (\times F (t)) (N) F (t) (N + 1)$
45	43 44	syl	$⊢ φ \to seq 1 (\times F (t)) (N + 1) = seq 1 (\times F (t)) (N) F (t) (N + 1)$
46	45	adantr	$⊢ (φ \land t \in T) \to seq 1 (\times F (t)) (N + 1) = seq 1 (\times F (t)) (N) F (t) (N + 1)$
47		seqp1	$⊢ N \in ℤ_{\geq 1} \to seq 1 (P, U) (N + 1) = seq 1 (P, U) (N) P U (N + 1)$
48	43 47	syl	$⊢ φ \to seq 1 (P, U) (N + 1) = seq 1 (P, U) (N) P U (N + 1)$
49		nfcv	$⊢ \underline{Ⅎ} h (t \in T ⟼ f (t) g (t))$
50		nfcv	$⊢ \underline{Ⅎ} l (t \in T ⟼ f (t) g (t))$
51		nfcv	$⊢ \underline{Ⅎ} f (t \in T ⟼ h (t) l (t))$
52		nfcv	$⊢ \underline{Ⅎ} g (t \in T ⟼ h (t) l (t))$
53		fveq1	$⊢ f = h \to f (t) = h (t)$
54		fveq1	$⊢ g = l \to g (t) = l (t)$
55	53 54	oveqan12d	$⊢ (f = h \land g = l) \to f (t) g (t) = h (t) l (t)$
56	55	mpteq2dv	$⊢ (f = h \land g = l) \to (t \in T ⟼ f (t) g (t)) = (t \in T ⟼ h (t) l (t))$
57	49 50 51 52 56	cbvmpo	$⊢ (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t))) = (h \in Y, l \in Y ⟼ (t \in T ⟼ h (t) l (t)))$
58	4 57	eqtri	$⊢ P = (h \in Y, l \in Y ⟼ (t \in T ⟼ h (t) l (t)))$
59	58	a1i	$⊢ φ \to P = (h \in Y, l \in Y ⟼ (t \in T ⟼ h (t) l (t)))$
60		nfcv	$⊢ \underline{Ⅎ} t 1$
61		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ f (t) g (t))$
62	3 3 61	nfmpo	$⊢ \underline{Ⅎ} t (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
63	4 62	nfcxfr	$⊢ \underline{Ⅎ} t P$
64		nfcv	$⊢ \underline{Ⅎ} t U$
65	60 63 64	nfseq	$⊢ \underline{Ⅎ} t seq 1 (P, U)$
66		nfcv	$⊢ \underline{Ⅎ} t N$
67	65 66	nffv	$⊢ \underline{Ⅎ} t seq 1 (P, U) (N)$
68	67	nfeq2	$⊢ Ⅎ t h = seq 1 (P, U) (N)$
69		nfv	$⊢ Ⅎ t l = U (N + 1)$
70	68 69	nfan	$⊢ Ⅎ t (h = seq 1 (P, U) (N) \land l = U (N + 1))$
71		fveq1	$⊢ h = seq 1 (P, U) (N) \to h (t) = seq 1 (P, U) (N) (t)$
72	71	ad2antrr	$⊢ ((h = seq 1 (P, U) (N) \land l = U (N + 1)) \land t \in T) \to h (t) = seq 1 (P, U) (N) (t)$
73		fveq1	$⊢ l = U (N + 1) \to l (t) = U (N + 1) (t)$
74	73	ad2antlr	$⊢ ((h = seq 1 (P, U) (N) \land l = U (N + 1)) \land t \in T) \to l (t) = U (N + 1) (t)$
75	72 74	oveq12d	$⊢ ((h = seq 1 (P, U) (N) \land l = U (N + 1)) \land t \in T) \to h (t) l (t) = seq 1 (P, U) (N) (t) U (N + 1) (t)$
76	70 75	mpteq2da	$⊢ (h = seq 1 (P, U) (N) \land l = U (N + 1)) \to (t \in T ⟼ h (t) l (t)) = (t \in T ⟼ seq 1 (P, U) (N) (t) U (N + 1) (t))$
77	76	adantl	$⊢ (φ \land (h = seq 1 (P, U) (N) \land l = U (N + 1))) \to (t \in T ⟼ h (t) l (t)) = (t \in T ⟼ seq 1 (P, U) (N) (t) U (N + 1) (t))$
78		eqid	$⊢ seq 1 (P, U) (N) = seq 1 (P, U) (N)$
79		3simpc	$⊢ (φ \land h \in Y \land l \in Y) \to (h \in Y \land l \in Y)$
80		nfcv	$⊢ \underline{Ⅎ} f h$
81		nfcv	$⊢ \underline{Ⅎ} g h$
82		nfcv	$⊢ \underline{Ⅎ} g l$
83		nfv	$⊢ Ⅎ f h \in Y$
84		nfv	$⊢ Ⅎ f g \in Y$
85	1 83 84	nf3an	$⊢ Ⅎ f (φ \land h \in Y \land g \in Y)$
86		nfv	$⊢ Ⅎ f (t \in T ⟼ h (t) g (t)) \in Y$
87	85 86	nfim	$⊢ Ⅎ f ((φ \land h \in Y \land g \in Y) \to (t \in T ⟼ h (t) g (t)) \in Y)$
88		nfv	$⊢ Ⅎ g h \in Y$
89		nfv	$⊢ Ⅎ g l \in Y$
90	2 88 89	nf3an	$⊢ Ⅎ g (φ \land h \in Y \land l \in Y)$
91		nfv	$⊢ Ⅎ g (t \in T ⟼ h (t) l (t)) \in Y$
92	90 91	nfim	$⊢ Ⅎ g ((φ \land h \in Y \land l \in Y) \to (t \in T ⟼ h (t) l (t)) \in Y)$
93		eleq1	$⊢ f = h \to (f \in Y \leftrightarrow h \in Y)$
94	93	3anbi2d	$⊢ f = h \to ((φ \land f \in Y \land g \in Y) \leftrightarrow (φ \land h \in Y \land g \in Y))$
95	53	oveq1d	$⊢ f = h \to f (t) g (t) = h (t) g (t)$
96	95	mpteq2dv	$⊢ f = h \to (t \in T ⟼ f (t) g (t)) = (t \in T ⟼ h (t) g (t))$
97	96	eleq1d	$⊢ f = h \to ((t \in T ⟼ f (t) g (t)) \in Y \leftrightarrow (t \in T ⟼ h (t) g (t)) \in Y)$
98	94 97	imbi12d	$⊢ f = h \to (((φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y) \leftrightarrow ((φ \land h \in Y \land g \in Y) \to (t \in T ⟼ h (t) g (t)) \in Y))$
99		eleq1	$⊢ g = l \to (g \in Y \leftrightarrow l \in Y)$
100	99	3anbi3d	$⊢ g = l \to ((φ \land h \in Y \land g \in Y) \leftrightarrow (φ \land h \in Y \land l \in Y))$
101	54	oveq2d	$⊢ g = l \to h (t) g (t) = h (t) l (t)$
102	101	mpteq2dv	$⊢ g = l \to (t \in T ⟼ h (t) g (t)) = (t \in T ⟼ h (t) l (t))$
103	102	eleq1d	$⊢ g = l \to ((t \in T ⟼ h (t) g (t)) \in Y \leftrightarrow (t \in T ⟼ h (t) l (t)) \in Y)$
104	100 103	imbi12d	$⊢ g = l \to (((φ \land h \in Y \land g \in Y) \to (t \in T ⟼ h (t) g (t)) \in Y) \leftrightarrow ((φ \land h \in Y \land l \in Y) \to (t \in T ⟼ h (t) l (t)) \in Y))$
105	80 81 82 87 92 98 104 8	vtocl2gf	$⊢ (h \in Y \land l \in Y) \to ((φ \land h \in Y \land l \in Y) \to (t \in T ⟼ h (t) l (t)) \in Y)$
106	79 105	mpcom	$⊢ (φ \land h \in Y \land l \in Y) \to (t \in T ⟼ h (t) l (t)) \in Y$
107	58 78 9 7 106 6	fmulcl	$⊢ φ \to seq 1 (P, U) (N) \in Y$
108		mptexg	$⊢ T \in V \to (t \in T ⟼ seq 1 (P, U) (N) (t) U (N + 1) (t)) \in V$
109	6 108	syl	$⊢ φ \to (t \in T ⟼ seq 1 (P, U) (N) (t) U (N + 1) (t)) \in V$
110	59 77 107 26 109	ovmpod	$⊢ φ \to seq 1 (P, U) (N) P U (N + 1) = (t \in T ⟼ seq 1 (P, U) (N) (t) U (N + 1) (t))$
111	48 110	eqtrd	$⊢ φ \to seq 1 (P, U) (N + 1) = (t \in T ⟼ seq 1 (P, U) (N) (t) U (N + 1) (t))$
112	107	ancli	$⊢ φ \to (φ \land seq 1 (P, U) (N) \in Y)$
113		nfcv	$⊢ \underline{Ⅎ} f 1$
114		nfmpo1	$⊢ \underline{Ⅎ} f (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
115	4 114	nfcxfr	$⊢ \underline{Ⅎ} f P$
116		nfcv	$⊢ \underline{Ⅎ} f U$
117	113 115 116	nfseq	$⊢ \underline{Ⅎ} f seq 1 (P, U)$
118		nfcv	$⊢ \underline{Ⅎ} f N$
119	117 118	nffv	$⊢ \underline{Ⅎ} f seq 1 (P, U) (N)$
120	119	nfel1	$⊢ Ⅎ f seq 1 (P, U) (N) \in Y$
121	1 120	nfan	$⊢ Ⅎ f (φ \land seq 1 (P, U) (N) \in Y)$
122		nfcv	$⊢ \underline{Ⅎ} f T$
123		nfcv	$⊢ \underline{Ⅎ} f ℝ$
124	119 122 123	nff	$⊢ Ⅎ f seq 1 (P, U) (N) : T ⟶ ℝ$
125	121 124	nfim	$⊢ Ⅎ f ((φ \land seq 1 (P, U) (N) \in Y) \to seq 1 (P, U) (N) : T ⟶ ℝ)$
126		eleq1	$⊢ f = seq 1 (P, U) (N) \to (f \in Y \leftrightarrow seq 1 (P, U) (N) \in Y)$
127	126	anbi2d	$⊢ f = seq 1 (P, U) (N) \to ((φ \land f \in Y) \leftrightarrow (φ \land seq 1 (P, U) (N) \in Y))$
128		feq1	$⊢ f = seq 1 (P, U) (N) \to (f : T ⟶ ℝ \leftrightarrow seq 1 (P, U) (N) : T ⟶ ℝ)$
129	127 128	imbi12d	$⊢ f = seq 1 (P, U) (N) \to (((φ \land f \in Y) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land seq 1 (P, U) (N) \in Y) \to seq 1 (P, U) (N) : T ⟶ ℝ))$
130	119 125 129 12	vtoclgf	$⊢ seq 1 (P, U) (N) \in Y \to ((φ \land seq 1 (P, U) (N) \in Y) \to seq 1 (P, U) (N) : T ⟶ ℝ)$
131	107 112 130	sylc	$⊢ φ \to seq 1 (P, U) (N) : T ⟶ ℝ$
132	131	ffvelrnda	$⊢ (φ \land t \in T) \to seq 1 (P, U) (N) (t) \in ℝ$
133	132 39	remulcld	$⊢ (φ \land t \in T) \to seq 1 (P, U) (N) (t) U (N + 1) (t) \in ℝ$
134	111 133	fvmpt2d	$⊢ (φ \land t \in T) \to seq 1 (P, U) (N + 1) (t) = seq 1 (P, U) (N) (t) U (N + 1) (t)$
135	11	oveq1d	$⊢ φ \to seq 1 (P, U) (N) (t) U (N + 1) (t) = seq 1 (\times F (t)) (N) U (N + 1) (t)$
136	135	adantr	$⊢ (φ \land t \in T) \to seq 1 (P, U) (N) (t) U (N + 1) (t) = seq 1 (\times F (t)) (N) U (N + 1) (t)$
137	134 136	eqtrd	$⊢ (φ \land t \in T) \to seq 1 (P, U) (N + 1) (t) = seq 1 (\times F (t)) (N) U (N + 1) (t)$
138	41 46 137	3eqtr4rd	$⊢ (φ \land t \in T) \to seq 1 (P, U) (N + 1) (t) = seq 1 (\times F (t)) (N + 1)$

Metamath Proof Explorer

Theorem fmuldfeqlem1

Proof