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 | |
|
stoweidlem40.2 | |
||
stoweidlem40.3 | |
||
stoweidlem40.4 | |
||
stoweidlem40.5 | |
||
stoweidlem40.6 | |
||
stoweidlem40.7 | |
||
stoweidlem40.8 | |
||
stoweidlem40.9 | |
||
stoweidlem40.10 | |
||
stoweidlem40.11 | |
||
stoweidlem40.12 | |
||
stoweidlem40.13 | |
||
stoweidlem40.14 | |
||
Assertion | stoweidlem40 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stoweidlem40.1 | |
|
2 | stoweidlem40.2 | |
|
3 | stoweidlem40.3 | |
|
4 | stoweidlem40.4 | |
|
5 | stoweidlem40.5 | |
|
6 | stoweidlem40.6 | |
|
7 | stoweidlem40.7 | |
|
8 | stoweidlem40.8 | |
|
9 | stoweidlem40.9 | |
|
10 | stoweidlem40.10 | |
|
11 | stoweidlem40.11 | |
|
12 | stoweidlem40.12 | |
|
13 | stoweidlem40.13 | |
|
14 | stoweidlem40.14 | |
|
15 | simpr | |
|
16 | 1red | |
|
17 | 8 | ffvelrnda | |
18 | 13 | nnnn0d | |
19 | 18 | adantr | |
20 | 17 19 | reexpcld | |
21 | 16 20 | resubcld | |
22 | 4 | fvmpt2 | |
23 | 15 21 22 | syl2anc | |
24 | 23 | eqcomd | |
25 | 24 | oveq1d | |
26 | 2 25 | mpteq2da | |
27 | 3 26 | eqtrid | |
28 | nfmpt1 | |
|
29 | 4 28 | nfcxfr | |
30 | 1re | |
|
31 | 5 | fvmpt2 | |
32 | 30 31 | mpan2 | |
33 | 32 | eqcomd | |
34 | 33 | adantl | |
35 | 6 | fvmpt2 | |
36 | 15 20 35 | syl2anc | |
37 | 36 | eqcomd | |
38 | 34 37 | oveq12d | |
39 | 2 38 | mpteq2da | |
40 | 4 39 | eqtrid | |
41 | 12 | stoweidlem4 | |
42 | 30 41 | mpan2 | |
43 | 5 42 | eqeltrid | |
44 | 1 2 9 11 12 7 18 | stoweidlem19 | |
45 | 6 44 | eqeltrid | |
46 | nfmpt1 | |
|
47 | 5 46 | nfcxfr | |
48 | nfmpt1 | |
|
49 | 6 48 | nfcxfr | |
50 | 47 49 2 9 10 11 12 | stoweidlem33 | |
51 | 43 45 50 | mpd3an23 | |
52 | 40 51 | eqeltrd | |
53 | 14 | nnnn0d | |
54 | 29 2 9 11 12 52 53 | stoweidlem19 | |
55 | 27 54 | eqeltrd | |