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 ⊢ Ⅎ 𝑡 𝑃
stoweidlem40.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem40.3 ⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ 𝑀 ) )
stoweidlem40.4 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) )
stoweidlem40.5 ⊢ 𝐺 = ( 𝑡 ∈ 𝑇 ↦ 1 )
stoweidlem40.6 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) )
stoweidlem40.7 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
stoweidlem40.8 ⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
stoweidlem40.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem40.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem40.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem40.12 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem40.13 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
stoweidlem40.14 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
Assertion stoweidlem40 ( 𝜑 → 𝑄 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 stoweidlem40.1 ⊢ Ⅎ 𝑡 𝑃
2 stoweidlem40.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem40.3 ⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ 𝑀 ) )
4 stoweidlem40.4 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) )
5 stoweidlem40.5 ⊢ 𝐺 = ( 𝑡 ∈ 𝑇 ↦ 1 )
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 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℝ )
17 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
18 13 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ℕ0 )
20 17 19 reexpcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ∈ ℝ )
21 16 20 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ ℝ )
22 4 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ ℝ ) → ( 𝐹 ‘ 𝑡 ) = ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) )
23 15 21 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) = ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) )
24 23 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) = ( 𝐹 ‘ 𝑡 ) )
25 24 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ 𝑀 ) = ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑀 ) )
26 2 25 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ 𝑀 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑀 ) ) )
27 3 26 eqtrid ⊢ ( 𝜑 → 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑀 ) ) )
28 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) )
29 4 28 nfcxfr ⊢ Ⅎ 𝑡 𝐹
30 1re ⊢ 1 ∈ ℝ
31 5 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ 1 ∈ ℝ ) → ( 𝐺 ‘ 𝑡 ) = 1 )
32 30 31 mpan2 ⊢ ( 𝑡 ∈ 𝑇 → ( 𝐺 ‘ 𝑡 ) = 1 )
33 32 eqcomd ⊢ ( 𝑡 ∈ 𝑇 → 1 = ( 𝐺 ‘ 𝑡 ) )
34 33 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 1 = ( 𝐺 ‘ 𝑡 ) )
35 6 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ∈ ℝ ) → ( 𝐻 ‘ 𝑡 ) = ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) )
36 15 20 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) = ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) )
37 36 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) = ( 𝐻 ‘ 𝑡 ) )
38 34 37 oveq12d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) = ( ( 𝐺 ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) )
39 2 38 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) )
40 4 39 eqtrid ⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) )
41 12 stoweidlem4 ⊢ ( ( 𝜑 ∧ 1 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
42 30 41 mpan2 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
43 5 42 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
44 1 2 9 11 12 7 18 stoweidlem19 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ 𝐴 )
45 6 44 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ 𝐴 )
46 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ 1 )
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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
54 29 2 9 11 12 52 53 stoweidlem19 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑀 ) ) ∈ 𝐴 )
55 27 54 eqeltrd ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )