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 _tP
stoweidlem40.2 tφ
stoweidlem40.3 Q=tT1PtNM
stoweidlem40.4 F=tT1PtN
stoweidlem40.5 G=tT1
stoweidlem40.6 H=tTPtN
stoweidlem40.7 φPA
stoweidlem40.8 φP:T
stoweidlem40.9 φfAf:T
stoweidlem40.10 φfAgAtTft+gtA
stoweidlem40.11 φfAgAtTftgtA
stoweidlem40.12 φxtTxA
stoweidlem40.13 φN
stoweidlem40.14 φM
Assertion stoweidlem40 φQA

Proof

Step Hyp Ref Expression
1 stoweidlem40.1 _tP
2 stoweidlem40.2 tφ
3 stoweidlem40.3 Q=tT1PtNM
4 stoweidlem40.4 F=tT1PtN
5 stoweidlem40.5 G=tT1
6 stoweidlem40.6 H=tTPtN
7 stoweidlem40.7 φPA
8 stoweidlem40.8 φP:T
9 stoweidlem40.9 φfAf:T
10 stoweidlem40.10 φfAgAtTft+gtA
11 stoweidlem40.11 φfAgAtTftgtA
12 stoweidlem40.12 φxtTxA
13 stoweidlem40.13 φN
14 stoweidlem40.14 φM
15 simpr φtTtT
16 1red φtT1
17 8 ffvelrnda φtTPt
18 13 nnnn0d φN0
19 18 adantr φtTN0
20 17 19 reexpcld φtTPtN
21 16 20 resubcld φtT1PtN
22 4 fvmpt2 tT1PtNFt=1PtN
23 15 21 22 syl2anc φtTFt=1PtN
24 23 eqcomd φtT1PtN=Ft
25 24 oveq1d φtT1PtNM=FtM
26 2 25 mpteq2da φtT1PtNM=tTFtM
27 3 26 eqtrid φQ=tTFtM
28 nfmpt1 _ttT1PtN
29 4 28 nfcxfr _tF
30 1re 1
31 5 fvmpt2 tT1Gt=1
32 30 31 mpan2 tTGt=1
33 32 eqcomd tT1=Gt
34 33 adantl φtT1=Gt
35 6 fvmpt2 tTPtNHt=PtN
36 15 20 35 syl2anc φtTHt=PtN
37 36 eqcomd φtTPtN=Ht
38 34 37 oveq12d φtT1PtN=GtHt
39 2 38 mpteq2da φtT1PtN=tTGtHt
40 4 39 eqtrid φF=tTGtHt
41 12 stoweidlem4 φ1tT1A
42 30 41 mpan2 φtT1A
43 5 42 eqeltrid φGA
44 1 2 9 11 12 7 18 stoweidlem19 φtTPtNA
45 6 44 eqeltrid φHA
46 nfmpt1 _ttT1
47 5 46 nfcxfr _tG
48 nfmpt1 _ttTPtN
49 6 48 nfcxfr _tH
50 47 49 2 9 10 11 12 stoweidlem33 φGAHAtTGtHtA
51 43 45 50 mpd3an23 φtTGtHtA
52 40 51 eqeltrd φFA
53 14 nnnn0d φM0
54 29 2 9 11 12 52 53 stoweidlem19 φtTFtMA
55 27 54 eqeltrd φQA