Metamath Proof Explorer

Theorem stoweidlem40

Description: This lemma proves that q_n is in the subalgebra, as in the proof of Lemma 1 in BrosowskiDeutsh p. 90. Q is used to represent q_n in the paper, N is used to represent n in the paper, and M is used to represent k^n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem40.1 
|- F/_ t P
stoweidlem40.2 
|- F/ t ph
stoweidlem40.3 
|- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ M ) )
stoweidlem40.4 
|- F = ( t e. T |-> ( 1 - ( ( P ` t ) ^ N ) ) )
stoweidlem40.5 
|- G = ( t e. T |-> 1 )
stoweidlem40.6 
|- H = ( t e. T |-> ( ( P ` t ) ^ N ) )
stoweidlem40.7 
|- ( ph -> P e. A )
stoweidlem40.8 
|- ( ph -> P : T --> RR )
stoweidlem40.9 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem40.10 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem40.11 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem40.12 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem40.13 
|- ( ph -> N e. NN )
stoweidlem40.14 
|- ( ph -> M e. NN )
Assertion stoweidlem40 
|- ( ph -> Q e. A )

Proof

Step Hyp Ref Expression
1 stoweidlem40.1 
 |-  F/_ t P
2 stoweidlem40.2 
 |-  F/ t ph
3 stoweidlem40.3 
 |-  Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ M ) )
4 stoweidlem40.4 
 |-  F = ( t e. T |-> ( 1 - ( ( P ` t ) ^ N ) ) )
5 stoweidlem40.5 
 |-  G = ( t e. T |-> 1 )
6 stoweidlem40.6 
 |-  H = ( t e. T |-> ( ( P ` t ) ^ N ) )
7 stoweidlem40.7 
 |-  ( ph -> P e. A )
8 stoweidlem40.8 
 |-  ( ph -> P : T --> RR )
9 stoweidlem40.9 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
10 stoweidlem40.10 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
11 stoweidlem40.11 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
12 stoweidlem40.12 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
13 stoweidlem40.13 
 |-  ( ph -> N e. NN )
14 stoweidlem40.14 
 |-  ( ph -> M e. NN )
15 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
16 1red 
 |-  ( ( ph /\ t e. T ) -> 1 e. RR )
17 8 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( P ` t ) e. RR )
18 13 nnnn0d 
 |-  ( ph -> N e. NN0 )
19 18 adantr 
 |-  ( ( ph /\ t e. T ) -> N e. NN0 )
20 17 19 reexpcld 
 |-  ( ( ph /\ t e. T ) -> ( ( P ` t ) ^ N ) e. RR )
21 16 20 resubcld 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( ( P ` t ) ^ N ) ) e. RR )
22 4 fvmpt2 
 |-  ( ( t e. T /\ ( 1 - ( ( P ` t ) ^ N ) ) e. RR ) -> ( F ` t ) = ( 1 - ( ( P ` t ) ^ N ) ) )
23 15 21 22 syl2anc 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) = ( 1 - ( ( P ` t ) ^ N ) ) )
24 23 eqcomd 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( ( P ` t ) ^ N ) ) = ( F ` t ) )
25 24 oveq1d 
 |-  ( ( ph /\ t e. T ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ M ) = ( ( F ` t ) ^ M ) )
26 2 25 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ M ) ) = ( t e. T |-> ( ( F ` t ) ^ M ) ) )
27 3 26 eqtrid 
 |-  ( ph -> Q = ( t e. T |-> ( ( F ` t ) ^ M ) ) )
28 nfmpt1 
 |-  F/_ t ( t e. T |-> ( 1 - ( ( P ` t ) ^ N ) ) )
29 4 28 nfcxfr 
 |-  F/_ t F
30 1re 
 |-  1 e. RR
31 5 fvmpt2 
 |-  ( ( t e. T /\ 1 e. RR ) -> ( G ` t ) = 1 )
32 30 31 mpan2 
 |-  ( t e. T -> ( G ` t ) = 1 )
33 32 eqcomd 
 |-  ( t e. T -> 1 = ( G ` t ) )
34 33 adantl 
 |-  ( ( ph /\ t e. T ) -> 1 = ( G ` t ) )
35 6 fvmpt2 
 |-  ( ( t e. T /\ ( ( P ` t ) ^ N ) e. RR ) -> ( H ` t ) = ( ( P ` t ) ^ N ) )
36 15 20 35 syl2anc 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) = ( ( P ` t ) ^ N ) )
37 36 eqcomd 
 |-  ( ( ph /\ t e. T ) -> ( ( P ` t ) ^ N ) = ( H ` t ) )
38 34 37 oveq12d 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( ( P ` t ) ^ N ) ) = ( ( G ` t ) - ( H ` t ) ) )
39 2 38 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( 1 - ( ( P ` t ) ^ N ) ) ) = ( t e. T |-> ( ( G ` t ) - ( H ` t ) ) ) )
40 4 39 eqtrid 
 |-  ( ph -> F = ( t e. T |-> ( ( G ` t ) - ( H ` t ) ) ) )
41 12 stoweidlem4 
 |-  ( ( ph /\ 1 e. RR ) -> ( t e. T |-> 1 ) e. A )
42 30 41 mpan2 
 |-  ( ph -> ( t e. T |-> 1 ) e. A )
43 5 42 eqeltrid 
 |-  ( ph -> G e. A )
44 1 2 9 11 12 7 18 stoweidlem19 
 |-  ( ph -> ( t e. T |-> ( ( P ` t ) ^ N ) ) e. A )
45 6 44 eqeltrid 
 |-  ( ph -> H e. A )
46 nfmpt1 
 |-  F/_ t ( t e. T |-> 1 )
47 5 46 nfcxfr 
 |-  F/_ t G
48 nfmpt1 
 |-  F/_ t ( t e. T |-> ( ( P ` t ) ^ N ) )
49 6 48 nfcxfr 
 |-  F/_ t H
50 47 49 2 9 10 11 12 stoweidlem33 
 |-  ( ( ph /\ G e. A /\ H e. A ) -> ( t e. T |-> ( ( G ` t ) - ( H ` t ) ) ) e. A )
51 43 45 50 mpd3an23 
 |-  ( ph -> ( t e. T |-> ( ( G ` t ) - ( H ` t ) ) ) e. A )
52 40 51 eqeltrd 
 |-  ( ph -> F e. A )
53 14 nnnn0d 
 |-  ( ph -> M e. NN0 )
54 29 2 9 11 12 52 53 stoweidlem19 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) ^ M ) ) e. A )
55 27 54 eqeltrd 
 |-  ( ph -> Q e. A )