Metamath Proof Explorer

Theorem 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 ⊢ Ⅎ 𝑡 𝜑
stoweidlem32.2 ⊢ 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑌 · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
stoweidlem32.3 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
stoweidlem32.4 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ 𝑌 )
stoweidlem32.5 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
stoweidlem32.6 ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
stoweidlem32.7 ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
stoweidlem32.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem32.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem32.10 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem32.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
Assertion stoweidlem32 ( 𝜑 → 𝑃 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 stoweidlem32.1 ⊢ Ⅎ 𝑡 𝜑
2 stoweidlem32.2 ⊢ 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑌 · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
3 stoweidlem32.3 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
4 stoweidlem32.4 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ 𝑌 )
5 stoweidlem32.5 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6 stoweidlem32.6 ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
7 stoweidlem32.7 ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
8 stoweidlem32.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
9 stoweidlem32.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10 stoweidlem32.10 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
11 stoweidlem32.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
12 fveq2 ⊢ ( 𝑡 = 𝑠 → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) )
13 12 sumeq2sdv ⊢ ( 𝑡 = 𝑠 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) )
14 13 cbvmptv ⊢ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑠 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) )
15 3 14 eqtri ⊢ 𝐹 = ( 𝑠 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) )
16 fveq2 ⊢ ( 𝑠 = 𝑡 → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) = ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
17 16 sumeq2sdv ⊢ ( 𝑠 = 𝑡 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑠 ) = Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
19 fzfid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 ... 𝑀 ) ∈ Fin )
20 simpl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝜑 )
21 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 )
22 eleq1 ⊢ ( 𝑓 = ( 𝐺 ‘ 𝑖 ) → ( 𝑓 ∈ 𝐴 ↔ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) )
23 22 anbi2d ⊢ ( 𝑓 = ( 𝐺 ‘ 𝑖 ) → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) ) )
24 feq1 ⊢ ( 𝑓 = ( 𝐺 ‘ 𝑖 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
25 23 24 imbi12d ⊢ ( 𝑓 = ( 𝐺 ‘ 𝑖 ) → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) ) )
26 25 11 vtoclg ⊢ ( ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
27 21 26 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
28 20 21 27 mp2and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
29 28 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
30 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑡 ∈ 𝑇 )
31 29 30 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
32 19 31 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
33 15 17 18 32 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) = Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
34 33 32 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
35 34 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
36 eqidd ⊢ ( 𝑠 = 𝑡 → 𝑌 = 𝑌 )
37 36 cbvmptv ⊢ ( 𝑠 ∈ 𝑇 ↦ 𝑌 ) = ( 𝑡 ∈ 𝑇 ↦ 𝑌 )
38 4 37 eqtr4i ⊢ 𝐻 = ( 𝑠 ∈ 𝑇 ↦ 𝑌 )
39 6 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑌 ∈ ℝ )
40 38 36 18 39 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) = 𝑌 )
41 40 39 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) ∈ ℝ )
42 41 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) ∈ ℂ )
43 35 42 mulcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) · ( 𝐻 ‘ 𝑡 ) ) = ( ( 𝐻 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) )
44 40 33 oveq12d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐻 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) = ( 𝑌 · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
45 43 44 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑌 · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( 𝐻 ‘ 𝑡 ) ) )
46 1 45 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( 𝑌 · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐻 ‘ 𝑡 ) ) ) )
47 2 46 syl5eq ⊢ ( 𝜑 → 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐻 ‘ 𝑡 ) ) ) )
48 1 3 5 7 8 11 stoweidlem20 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
49 10 stoweidlem4 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑌 ) ∈ 𝐴 )
50 6 49 mpdan ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝑌 ) ∈ 𝐴 )
51 4 50 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ 𝐴 )
52 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
53 3 52 nfcxfr ⊢ Ⅎ 𝑡 𝐹
54 53 nfeq2 ⊢ Ⅎ 𝑡 𝑓 = 𝐹
55 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ 𝑌 )
56 4 55 nfcxfr ⊢ Ⅎ 𝑡 𝐻
57 56 nfeq2 ⊢ Ⅎ 𝑡 𝑔 = 𝐻
58 54 57 9 stoweidlem6 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐻 ‘ 𝑡 ) ) ) ∈ 𝐴 )
59 48 51 58 mpd3an23 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐻 ‘ 𝑡 ) ) ) ∈ 𝐴 )
60 47 59 eqeltrd ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )