stoweidlem32

Description: If a set A of real functions from a common domain T is a subalgebra and it contains constants, then it is closed under the sum of a finite number of functions, indexed by G and finally scaled by a real Y. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem32.1	$⊢ Ⅎ t φ$
	stoweidlem32.2	$⊢ P = (t \in T ⟼ Y \sum_{i = 1}^{M} G (i) (t))$
	stoweidlem32.3	$⊢ F = (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t))$
	stoweidlem32.4	$⊢ H = (t \in T ⟼ Y)$
	stoweidlem32.5	$⊢ φ \to M \in ℕ$
	stoweidlem32.6	$⊢ φ \to Y \in ℝ$
	stoweidlem32.7	$⊢ φ \to G : (1 \dots M) ⟶ A$
	stoweidlem32.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem32.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem32.10	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem32.11	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
Assertion	stoweidlem32	$⊢ φ \to P \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem32.1	$⊢ Ⅎ t φ$
2		stoweidlem32.2	$⊢ P = (t \in T ⟼ Y \sum_{i = 1}^{M} G (i) (t))$
3		stoweidlem32.3	$⊢ F = (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t))$
4		stoweidlem32.4	$⊢ H = (t \in T ⟼ Y)$
5		stoweidlem32.5	$⊢ φ \to M \in ℕ$
6		stoweidlem32.6	$⊢ φ \to Y \in ℝ$
7		stoweidlem32.7	$⊢ φ \to G : (1 \dots M) ⟶ A$
8		stoweidlem32.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
9		stoweidlem32.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
10		stoweidlem32.10	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
11		stoweidlem32.11	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
12		fveq2	$⊢ t = s \to G (i) (t) = G (i) (s)$
13	12	sumeq2sdv	$⊢ t = s \to \sum_{i = 1}^{M} G (i) (t) = \sum_{i = 1}^{M} G (i) (s)$
14	13	cbvmptv	$⊢ (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t)) = (s \in T ⟼ \sum_{i = 1}^{M} G (i) (s))$
15	3 14	eqtri	$⊢ F = (s \in T ⟼ \sum_{i = 1}^{M} G (i) (s))$
16		fveq2	$⊢ s = t \to G (i) (s) = G (i) (t)$
17	16	sumeq2sdv	$⊢ s = t \to \sum_{i = 1}^{M} G (i) (s) = \sum_{i = 1}^{M} G (i) (t)$
18		simpr	$⊢ (φ \land t \in T) \to t \in T$
19		fzfid	$⊢ (φ \land t \in T) \to (1 \dots M) \in Fin$
20		simpl	$⊢ (φ \land i \in (1 \dots M)) \to φ$
21	7	ffvelrnda	$⊢ (φ \land i \in (1 \dots M)) \to G (i) \in A$
22		eleq1	$⊢ f = G (i) \to (f \in A \leftrightarrow G (i) \in A)$
23	22	anbi2d	$⊢ f = G (i) \to ((φ \land f \in A) \leftrightarrow (φ \land G (i) \in A))$
24		feq1	$⊢ f = G (i) \to (f : T ⟶ ℝ \leftrightarrow G (i) : T ⟶ ℝ)$
25	23 24	imbi12d	$⊢ f = G (i) \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land G (i) \in A) \to G (i) : T ⟶ ℝ))$
26	25 11	vtoclg	$⊢ G (i) \in A \to ((φ \land G (i) \in A) \to G (i) : T ⟶ ℝ)$
27	21 26	syl	$⊢ (φ \land i \in (1 \dots M)) \to ((φ \land G (i) \in A) \to G (i) : T ⟶ ℝ)$
28	20 21 27	mp2and	$⊢ (φ \land i \in (1 \dots M)) \to G (i) : T ⟶ ℝ$
29	28	adantlr	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to G (i) : T ⟶ ℝ$
30		simplr	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to t \in T$
31	29 30	ffvelrnd	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to G (i) (t) \in ℝ$
32	19 31	fsumrecl	$⊢ (φ \land t \in T) \to \sum_{i = 1}^{M} G (i) (t) \in ℝ$
33	15 17 18 32	fvmptd3	$⊢ (φ \land t \in T) \to F (t) = \sum_{i = 1}^{M} G (i) (t)$
34	33 32	eqeltrd	$⊢ (φ \land t \in T) \to F (t) \in ℝ$
35	34	recnd	$⊢ (φ \land t \in T) \to F (t) \in ℂ$
36		eqidd	$⊢ s = t \to Y = Y$
37	36	cbvmptv	$⊢ (s \in T ⟼ Y) = (t \in T ⟼ Y)$
38	4 37	eqtr4i	$⊢ H = (s \in T ⟼ Y)$
39	6	adantr	$⊢ (φ \land t \in T) \to Y \in ℝ$
40	38 36 18 39	fvmptd3	$⊢ (φ \land t \in T) \to H (t) = Y$
41	40 39	eqeltrd	$⊢ (φ \land t \in T) \to H (t) \in ℝ$
42	41	recnd	$⊢ (φ \land t \in T) \to H (t) \in ℂ$
43	35 42	mulcomd	$⊢ (φ \land t \in T) \to F (t) H (t) = H (t) F (t)$
44	40 33	oveq12d	$⊢ (φ \land t \in T) \to H (t) F (t) = Y \sum_{i = 1}^{M} G (i) (t)$
45	43 44	eqtr2d	$⊢ (φ \land t \in T) \to Y \sum_{i = 1}^{M} G (i) (t) = F (t) H (t)$
46	1 45	mpteq2da	$⊢ φ \to (t \in T ⟼ Y \sum_{i = 1}^{M} G (i) (t)) = (t \in T ⟼ F (t) H (t))$
47	2 46	eqtrid	$⊢ φ \to P = (t \in T ⟼ F (t) H (t))$
48	1 3 5 7 8 11	stoweidlem20	$⊢ φ \to F \in A$
49	10	stoweidlem4	$⊢ (φ \land Y \in ℝ) \to (t \in T ⟼ Y) \in A$
50	6 49	mpdan	$⊢ φ \to (t \in T ⟼ Y) \in A$
51	4 50	eqeltrid	$⊢ φ \to H \in A$
52		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t))$
53	3 52	nfcxfr	$⊢ \underline{Ⅎ} t F$
54	53	nfeq2	$⊢ Ⅎ t f = F$
55		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ Y)$
56	4 55	nfcxfr	$⊢ \underline{Ⅎ} t H$
57	56	nfeq2	$⊢ Ⅎ t g = H$
58	54 57 9	stoweidlem6	$⊢ (φ \land F \in A \land H \in A) \to (t \in T ⟼ F (t) H (t)) \in A$
59	48 51 58	mpd3an23	$⊢ φ \to (t \in T ⟼ F (t) H (t)) \in A$
60	47 59	eqeltrd	$⊢ φ \to P \in A$

Metamath Proof Explorer

Theorem stoweidlem32

Proof