Theorem stoweidlem18

Description: This theorem proves Lemma 2 in BrosowskiDeutsh p. 92 when A is empty, the trivial case. Here D is used to denote the set A of Lemma 2, because the variable A is used for the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem18.1	⊢ Ⅎ 𝑡 𝐷
	stoweidlem18.2	⊢ Ⅎ 𝑡 𝜑
	stoweidlem18.3	⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ 1 )
	stoweidlem18.4	⊢ 𝑇 = ∪ 𝐽
	stoweidlem18.5	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
	stoweidlem18.6	⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
	stoweidlem18.7	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	stoweidlem18.8	⊢ ( 𝜑 → 𝐷 = ∅ )
Assertion	stoweidlem18	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem18.1	⊢ Ⅎ 𝑡 𝐷
2		stoweidlem18.2	⊢ Ⅎ 𝑡 𝜑
3		stoweidlem18.3	⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ 1 )
4		stoweidlem18.4	⊢ 𝑇 = ∪ 𝐽
5		stoweidlem18.5	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
6		stoweidlem18.6	⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
7		stoweidlem18.7	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
8		stoweidlem18.8	⊢ ( 𝜑 → 𝐷 = ∅ )
9		1re	⊢ 1 ∈ ℝ
10	5	stoweidlem4	⊢ ( ( 𝜑 ∧ 1 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
11	9 10	mpan2	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
12	3 11	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
13		0le1	⊢ 0 ≤ 1
14		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
15	3	fvmpt2	⊢ ( ( 𝑡 ∈ 𝑇 ∧ 1 ∈ ℝ ) → ( 𝐹 ‘ 𝑡 ) = 1 )
16	14 9 15	sylancl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) = 1 )
17	13 16	breqtrrid	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝐹 ‘ 𝑡 ) )
18		1le1	⊢ 1 ≤ 1
19	16 18	eqbrtrdi	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ≤ 1 )
20	17 19	jca	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 1 ) )
21	20	ex	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → ( 0 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 1 ) ) )
22	2 21	ralrimi	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 1 ) )
23		nfcv	⊢ Ⅎ 𝑡 ∅
24	1 23	nfeq	⊢ Ⅎ 𝑡 𝐷 = ∅
25	24	rzalf	⊢ ( 𝐷 = ∅ → ∀ 𝑡 ∈ 𝐷 ( 𝐹 ‘ 𝑡 ) < 𝐸 )
26	8 25	syl	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐷 ( 𝐹 ‘ 𝑡 ) < 𝐸 )
27		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
28	27 7	ltsubrpd	⊢ ( 𝜑 → ( 1 − 𝐸 ) < 1 )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 1 − 𝐸 ) < 1 )
30	4	cldss	⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐵 ⊆ 𝑇 )
31	6 30	syl	⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
32	31	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → 𝑡 ∈ 𝑇 )
33	32 9 15	sylancl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑡 ) = 1 )
34	29 33	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 1 − 𝐸 ) < ( 𝐹 ‘ 𝑡 ) )
35	34	ex	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐵 → ( 1 − 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ) )
36	2 35	ralrimi	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝐹 ‘ 𝑡 ) )
37		nfcv	⊢ Ⅎ 𝑡 𝑥
38		nfmpt1	⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ 1 )
39	3 38	nfcxfr	⊢ Ⅎ 𝑡 𝐹
40	37 39	nfeq	⊢ Ⅎ 𝑡 𝑥 = 𝐹
41		fveq1	⊢ ( 𝑥 = 𝐹 → ( 𝑥 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
42	41	breq2d	⊢ ( 𝑥 = 𝐹 → ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ↔ 0 ≤ ( 𝐹 ‘ 𝑡 ) ) )
43	41	breq1d	⊢ ( 𝑥 = 𝐹 → ( ( 𝑥 ‘ 𝑡 ) ≤ 1 ↔ ( 𝐹 ‘ 𝑡 ) ≤ 1 ) )
44	42 43	anbi12d	⊢ ( 𝑥 = 𝐹 → ( ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 1 ) ) )
45	40 44	ralbid	⊢ ( 𝑥 = 𝐹 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 1 ) ) )
46	41	breq1d	⊢ ( 𝑥 = 𝐹 → ( ( 𝑥 ‘ 𝑡 ) < 𝐸 ↔ ( 𝐹 ‘ 𝑡 ) < 𝐸 ) )
47	40 46	ralbid	⊢ ( 𝑥 = 𝐹 → ( ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ↔ ∀ 𝑡 ∈ 𝐷 ( 𝐹 ‘ 𝑡 ) < 𝐸 ) )
48	41	breq2d	⊢ ( 𝑥 = 𝐹 → ( ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ↔ ( 1 − 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ) )
49	40 48	ralbid	⊢ ( 𝑥 = 𝐹 → ( ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ) )
50	45 47 49	3anbi123d	⊢ ( 𝑥 = 𝐹 → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝐹 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ) ) )
51	50	rspcev	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝐹 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )
52	12 22 26 36 51	syl13anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )