Metamath Proof Explorer

Theorem stoweidlem19

Description: If a set of real functions is closed under multiplication and it contains constants, then it is closed under finite exponentiation. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem19.1 
|- F/_ t F
stoweidlem19.2 
|- F/ t ph
stoweidlem19.3 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem19.4 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem19.5 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem19.6 
|- ( ph -> F e. A )
stoweidlem19.7 
|- ( ph -> N e. NN0 )
Assertion stoweidlem19 
|- ( ph -> ( t e. T |-> ( ( F ` t ) ^ N ) ) e. A )

Proof

Step Hyp Ref Expression
1 stoweidlem19.1 
 |-  F/_ t F
2 stoweidlem19.2 
 |-  F/ t ph
3 stoweidlem19.3 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
4 stoweidlem19.4 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
5 stoweidlem19.5 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
6 stoweidlem19.6 
 |-  ( ph -> F e. A )
7 stoweidlem19.7 
 |-  ( ph -> N e. NN0 )
8 oveq2 
 |-  ( n = 0 -> ( ( F ` t ) ^ n ) = ( ( F ` t ) ^ 0 ) )
9 8 mpteq2dv 
 |-  ( n = 0 -> ( t e. T |-> ( ( F ` t ) ^ n ) ) = ( t e. T |-> ( ( F ` t ) ^ 0 ) ) )
10 9 eleq1d 
 |-  ( n = 0 -> ( ( t e. T |-> ( ( F ` t ) ^ n ) ) e. A <-> ( t e. T |-> ( ( F ` t ) ^ 0 ) ) e. A ) )
11 10 imbi2d 
 |-  ( n = 0 -> ( ( ph -> ( t e. T |-> ( ( F ` t ) ^ n ) ) e. A ) <-> ( ph -> ( t e. T |-> ( ( F ` t ) ^ 0 ) ) e. A ) ) )
12 oveq2 
 |-  ( n = m -> ( ( F ` t ) ^ n ) = ( ( F ` t ) ^ m ) )
13 12 mpteq2dv 
 |-  ( n = m -> ( t e. T |-> ( ( F ` t ) ^ n ) ) = ( t e. T |-> ( ( F ` t ) ^ m ) ) )
14 13 eleq1d 
 |-  ( n = m -> ( ( t e. T |-> ( ( F ` t ) ^ n ) ) e. A <-> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) )
15 14 imbi2d 
 |-  ( n = m -> ( ( ph -> ( t e. T |-> ( ( F ` t ) ^ n ) ) e. A ) <-> ( ph -> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) ) )
16 oveq2 
 |-  ( n = ( m + 1 ) -> ( ( F ` t ) ^ n ) = ( ( F ` t ) ^ ( m + 1 ) ) )
17 16 mpteq2dv 
 |-  ( n = ( m + 1 ) -> ( t e. T |-> ( ( F ` t ) ^ n ) ) = ( t e. T |-> ( ( F ` t ) ^ ( m + 1 ) ) ) )
18 17 eleq1d 
 |-  ( n = ( m + 1 ) -> ( ( t e. T |-> ( ( F ` t ) ^ n ) ) e. A <-> ( t e. T |-> ( ( F ` t ) ^ ( m + 1 ) ) ) e. A ) )
19 18 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ph -> ( t e. T |-> ( ( F ` t ) ^ n ) ) e. A ) <-> ( ph -> ( t e. T |-> ( ( F ` t ) ^ ( m + 1 ) ) ) e. A ) ) )
20 oveq2 
 |-  ( n = N -> ( ( F ` t ) ^ n ) = ( ( F ` t ) ^ N ) )
21 20 mpteq2dv 
 |-  ( n = N -> ( t e. T |-> ( ( F ` t ) ^ n ) ) = ( t e. T |-> ( ( F ` t ) ^ N ) ) )
22 21 eleq1d 
 |-  ( n = N -> ( ( t e. T |-> ( ( F ` t ) ^ n ) ) e. A <-> ( t e. T |-> ( ( F ` t ) ^ N ) ) e. A ) )
23 22 imbi2d 
 |-  ( n = N -> ( ( ph -> ( t e. T |-> ( ( F ` t ) ^ n ) ) e. A ) <-> ( ph -> ( t e. T |-> ( ( F ` t ) ^ N ) ) e. A ) ) )
24 6 ancli 
 |-  ( ph -> ( ph /\ F e. A ) )
25 eleq1 
 |-  ( f = F -> ( f e. A <-> F e. A ) )
26 25 anbi2d 
 |-  ( f = F -> ( ( ph /\ f e. A ) <-> ( ph /\ F e. A ) ) )
27 feq1 
 |-  ( f = F -> ( f : T --> RR <-> F : T --> RR ) )
28 26 27 imbi12d 
 |-  ( f = F -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ F e. A ) -> F : T --> RR ) ) )
29 28 3 vtoclg 
 |-  ( F e. A -> ( ( ph /\ F e. A ) -> F : T --> RR ) )
30 6 24 29 sylc 
 |-  ( ph -> F : T --> RR )
31 30 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
32 recn 
 |-  ( ( F ` t ) e. RR -> ( F ` t ) e. CC )
33 exp0 
 |-  ( ( F ` t ) e. CC -> ( ( F ` t ) ^ 0 ) = 1 )
34 31 32 33 3syl 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) ^ 0 ) = 1 )
35 34 eqcomd 
 |-  ( ( ph /\ t e. T ) -> 1 = ( ( F ` t ) ^ 0 ) )
36 2 35 mpteq2da 
 |-  ( ph -> ( t e. T |-> 1 ) = ( t e. T |-> ( ( F ` t ) ^ 0 ) ) )
37 1re 
 |-  1 e. RR
38 5 stoweidlem4 
 |-  ( ( ph /\ 1 e. RR ) -> ( t e. T |-> 1 ) e. A )
39 37 38 mpan2 
 |-  ( ph -> ( t e. T |-> 1 ) e. A )
40 36 39 eqeltrrd 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) ^ 0 ) ) e. A )
41 simpr 
 |-  ( ( ( m e. NN0 /\ ( ph -> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) ) /\ ph ) -> ph )
42 simpll 
 |-  ( ( ( m e. NN0 /\ ( ph -> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) ) /\ ph ) -> m e. NN0 )
43 simplr 
 |-  ( ( ( m e. NN0 /\ ( ph -> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) ) /\ ph ) -> ( ph -> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) )
44 41 43 mpd 
 |-  ( ( ( m e. NN0 /\ ( ph -> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) ) /\ ph ) -> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A )
45 nfv 
 |-  F/ t m e. NN0
46 nfmpt1 
 |-  F/_ t ( t e. T |-> ( ( F ` t ) ^ m ) )
47 46 nfel1 
 |-  F/ t ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A
48 2 45 47 nf3an 
 |-  F/ t ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A )
49 simpl1 
 |-  ( ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) /\ t e. T ) -> ph )
50 simpr 
 |-  ( ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) /\ t e. T ) -> t e. T )
51 31 recnd 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. CC )
52 49 50 51 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) /\ t e. T ) -> ( F ` t ) e. CC )
53 simpl2 
 |-  ( ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) /\ t e. T ) -> m e. NN0 )
54 52 53 expp1d 
 |-  ( ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) /\ t e. T ) -> ( ( F ` t ) ^ ( m + 1 ) ) = ( ( ( F ` t ) ^ m ) x. ( F ` t ) ) )
55 48 54 mpteq2da 
 |-  ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) -> ( t e. T |-> ( ( F ` t ) ^ ( m + 1 ) ) ) = ( t e. T |-> ( ( ( F ` t ) ^ m ) x. ( F ` t ) ) ) )
56 31 3adant2 
 |-  ( ( ph /\ m e. NN0 /\ t e. T ) -> ( F ` t ) e. RR )
57 simp2 
 |-  ( ( ph /\ m e. NN0 /\ t e. T ) -> m e. NN0 )
58 56 57 reexpcld 
 |-  ( ( ph /\ m e. NN0 /\ t e. T ) -> ( ( F ` t ) ^ m ) e. RR )
59 49 53 50 58 syl3anc 
 |-  ( ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) /\ t e. T ) -> ( ( F ` t ) ^ m ) e. RR )
60 eqid 
 |-  ( t e. T |-> ( ( F ` t ) ^ m ) ) = ( t e. T |-> ( ( F ` t ) ^ m ) )
61 60 fvmpt2 
 |-  ( ( t e. T /\ ( ( F ` t ) ^ m ) e. RR ) -> ( ( t e. T |-> ( ( F ` t ) ^ m ) ) ` t ) = ( ( F ` t ) ^ m ) )
62 61 eqcomd 
 |-  ( ( t e. T /\ ( ( F ` t ) ^ m ) e. RR ) -> ( ( F ` t ) ^ m ) = ( ( t e. T |-> ( ( F ` t ) ^ m ) ) ` t ) )
63 50 59 62 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) /\ t e. T ) -> ( ( F ` t ) ^ m ) = ( ( t e. T |-> ( ( F ` t ) ^ m ) ) ` t ) )
64 63 oveq1d 
 |-  ( ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) /\ t e. T ) -> ( ( ( F ` t ) ^ m ) x. ( F ` t ) ) = ( ( ( t e. T |-> ( ( F ` t ) ^ m ) ) ` t ) x. ( F ` t ) ) )
65 48 64 mpteq2da 
 |-  ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) -> ( t e. T |-> ( ( ( F ` t ) ^ m ) x. ( F ` t ) ) ) = ( t e. T |-> ( ( ( t e. T |-> ( ( F ` t ) ^ m ) ) ` t ) x. ( F ` t ) ) ) )
66 6 adantr 
 |-  ( ( ph /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) -> F e. A )
67 46 nfeq2 
 |-  F/ t f = ( t e. T |-> ( ( F ` t ) ^ m ) )
68 1 nfeq2 
 |-  F/ t g = F
69 67 68 4 stoweidlem6 
 |-  ( ( ph /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A /\ F e. A ) -> ( t e. T |-> ( ( ( t e. T |-> ( ( F ` t ) ^ m ) ) ` t ) x. ( F ` t ) ) ) e. A )
70 66 69 mpd3an3 
 |-  ( ( ph /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> ( ( F ` t ) ^ m ) ) ` t ) x. ( F ` t ) ) ) e. A )
71 70 3adant2 
 |-  ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> ( ( F ` t ) ^ m ) ) ` t ) x. ( F ` t ) ) ) e. A )
72 65 71 eqeltrd 
 |-  ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) -> ( t e. T |-> ( ( ( F ` t ) ^ m ) x. ( F ` t ) ) ) e. A )
73 55 72 eqeltrd 
 |-  ( ( ph /\ m e. NN0 /\ ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) -> ( t e. T |-> ( ( F ` t ) ^ ( m + 1 ) ) ) e. A )
74 41 42 44 73 syl3anc 
 |-  ( ( ( m e. NN0 /\ ( ph -> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) ) /\ ph ) -> ( t e. T |-> ( ( F ` t ) ^ ( m + 1 ) ) ) e. A )
75 74 exp31 
 |-  ( m e. NN0 -> ( ( ph -> ( t e. T |-> ( ( F ` t ) ^ m ) ) e. A ) -> ( ph -> ( t e. T |-> ( ( F ` t ) ^ ( m + 1 ) ) ) e. A ) ) )
76 11 15 19 23 40 75 nn0ind 
 |-  ( N e. NN0 -> ( ph -> ( t e. T |-> ( ( F ` t ) ^ N ) ) e. A ) )
77 7 76 mpcom 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) ^ N ) ) e. A )