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	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )