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 
|- F/ t ph
stoweidlem32.2 
|- P = ( t e. T |-> ( Y x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )
stoweidlem32.3 
|- F = ( t e. T |-> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) )
stoweidlem32.4 
|- H = ( t e. T |-> Y )
stoweidlem32.5 
|- ( ph -> M e. NN )
stoweidlem32.6 
|- ( ph -> Y e. RR )
stoweidlem32.7 
|- ( ph -> G : ( 1 ... M ) --> A )
stoweidlem32.8 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem32.9 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem32.10 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem32.11 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
Assertion stoweidlem32 
|- ( ph -> P e. A )

Proof

Step Hyp Ref Expression
1 stoweidlem32.1 
 |-  F/ t ph
2 stoweidlem32.2 
 |-  P = ( t e. T |-> ( Y x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )
3 stoweidlem32.3 
 |-  F = ( t e. T |-> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) )
4 stoweidlem32.4 
 |-  H = ( t e. T |-> Y )
5 stoweidlem32.5 
 |-  ( ph -> M e. NN )
6 stoweidlem32.6 
 |-  ( ph -> Y e. RR )
7 stoweidlem32.7 
 |-  ( ph -> G : ( 1 ... M ) --> A )
8 stoweidlem32.8 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
9 stoweidlem32.9 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
10 stoweidlem32.10 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
11 stoweidlem32.11 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
12 fveq2 
 |-  ( t = s -> ( ( G ` i ) ` t ) = ( ( G ` i ) ` s ) )
13 12 sumeq2sdv 
 |-  ( t = s -> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) = sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) )
14 13 cbvmptv 
 |-  ( t e. T |-> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) = ( s e. T |-> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) )
15 3 14 eqtri 
 |-  F = ( s e. T |-> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) )
16 fveq2 
 |-  ( s = t -> ( ( G ` i ) ` s ) = ( ( G ` i ) ` t ) )
17 16 sumeq2sdv 
 |-  ( s = t -> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` s ) = sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) )
18 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
19 fzfid 
 |-  ( ( ph /\ t e. T ) -> ( 1 ... M ) e. Fin )
20 simpl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ph )
21 7 ffvelrnda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` i ) e. A )
22 eleq1 
 |-  ( f = ( G ` i ) -> ( f e. A <-> ( G ` i ) e. A ) )
23 22 anbi2d 
 |-  ( f = ( G ` i ) -> ( ( ph /\ f e. A ) <-> ( ph /\ ( G ` i ) e. A ) ) )
24 feq1 
 |-  ( f = ( G ` i ) -> ( f : T --> RR <-> ( G ` i ) : T --> RR ) )
25 23 24 imbi12d 
 |-  ( f = ( G ` i ) -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ ( G ` i ) e. A ) -> ( G ` i ) : T --> RR ) ) )
26 25 11 vtoclg 
 |-  ( ( G ` i ) e. A -> ( ( ph /\ ( G ` i ) e. A ) -> ( G ` i ) : T --> RR ) )
27 21 26 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ph /\ ( G ` i ) e. A ) -> ( G ` i ) : T --> RR ) )
28 20 21 27 mp2and 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` i ) : T --> RR )
29 28 adantlr 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( G ` i ) : T --> RR )
30 simplr 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> t e. T )
31 29 30 ffvelrnd 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( ( G ` i ) ` t ) e. RR )
32 19 31 fsumrecl 
 |-  ( ( ph /\ t e. T ) -> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) e. RR )
33 15 17 18 32 fvmptd3 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) = sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) )
34 33 32 eqeltrd 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
35 34 recnd 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. CC )
36 eqidd 
 |-  ( s = t -> Y = Y )
37 36 cbvmptv 
 |-  ( s e. T |-> Y ) = ( t e. T |-> Y )
38 4 37 eqtr4i 
 |-  H = ( s e. T |-> Y )
39 6 adantr 
 |-  ( ( ph /\ t e. T ) -> Y e. RR )
40 38 36 18 39 fvmptd3 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) = Y )
41 40 39 eqeltrd 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) e. RR )
42 41 recnd 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) e. CC )
43 35 42 mulcomd 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) x. ( H ` t ) ) = ( ( H ` t ) x. ( F ` t ) ) )
44 40 33 oveq12d 
 |-  ( ( ph /\ t e. T ) -> ( ( H ` t ) x. ( F ` t ) ) = ( Y x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )
45 43 44 eqtr2d 
 |-  ( ( ph /\ t e. T ) -> ( Y x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) = ( ( F ` t ) x. ( H ` t ) ) )
46 1 45 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( Y x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) ) = ( t e. T |-> ( ( F ` t ) x. ( H ` t ) ) ) )
47 2 46 syl5eq 
 |-  ( ph -> P = ( t e. T |-> ( ( F ` t ) x. ( H ` t ) ) ) )
48 1 3 5 7 8 11 stoweidlem20 
 |-  ( ph -> F e. A )
49 10 stoweidlem4 
 |-  ( ( ph /\ Y e. RR ) -> ( t e. T |-> Y ) e. A )
50 6 49 mpdan 
 |-  ( ph -> ( t e. T |-> Y ) e. A )
51 4 50 eqeltrid 
 |-  ( ph -> H e. A )
52 nfmpt1 
 |-  F/_ t ( t e. T |-> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) )
53 3 52 nfcxfr 
 |-  F/_ t F
54 53 nfeq2 
 |-  F/ t f = F
55 nfmpt1 
 |-  F/_ t ( t e. T |-> Y )
56 4 55 nfcxfr 
 |-  F/_ t H
57 56 nfeq2 
 |-  F/ t g = H
58 54 57 9 stoweidlem6 
 |-  ( ( ph /\ F e. A /\ H e. A ) -> ( t e. T |-> ( ( F ` t ) x. ( H ` t ) ) ) e. A )
59 48 51 58 mpd3an23 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) x. ( H ` t ) ) ) e. A )
60 47 59 eqeltrd 
 |-  ( ph -> P e. A )