Metamath Proof Explorer

Theorem stoweidlem23

Description: This lemma is used to prove the existence of a function p_t as in the beginning of Lemma 1 BrosowskiDeutsh p. 90: for all t in T - U, there exists a function p in the subalgebra, such that p_t ( t_0 ) = 0 , p_t ( t ) > 0, and 0 <= p_t <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem23.1 ⊢ Ⅎ 𝑡 𝜑
stoweidlem23.2 ⊢ Ⅎ 𝑡 𝐺
stoweidlem23.3 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑍 ) ) )
stoweidlem23.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem23.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem23.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem23.7 ⊢ ( 𝜑 → 𝑆 ∈ 𝑇 )
stoweidlem23.8 ⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
stoweidlem23.9 ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
stoweidlem23.10 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) ≠ ( 𝐺 ‘ 𝑍 ) )
Assertion stoweidlem23 ( 𝜑 → ( 𝐻 ∈ 𝐴 ∧ ( 𝐻 ‘ 𝑆 ) ≠ ( 𝐻 ‘ 𝑍 ) ∧ ( 𝐻 ‘ 𝑍 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem23.1 ⊢ Ⅎ 𝑡 𝜑
2 stoweidlem23.2 ⊢ Ⅎ 𝑡 𝐺
3 stoweidlem23.3 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑍 ) ) )
4 stoweidlem23.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
5 stoweidlem23.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
6 stoweidlem23.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
7 stoweidlem23.7 ⊢ ( 𝜑 → 𝑆 ∈ 𝑇 )
8 stoweidlem23.8 ⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
9 stoweidlem23.9 ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
10 stoweidlem23.10 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) ≠ ( 𝐺 ‘ 𝑍 ) )
11 9 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) )
12 eleq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴 ) )
13 12 anbi2d ⊢ ( 𝑓 = 𝐺 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) ) )
14 feq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐺 : 𝑇 ⟶ ℝ ) )
15 13 14 imbi12d ⊢ ( 𝑓 = 𝐺 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ ) ) )
16 15 4 vtoclg ⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ ) )
17 9 11 16 sylc ⊢ ( 𝜑 → 𝐺 : 𝑇 ⟶ ℝ )
18 17 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ )
19 18 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℂ )
20 17 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑍 ) ∈ ℝ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑍 ) ∈ ℝ )
22 21 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑍 ) ∈ ℂ )
23 19 22 negsubd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑍 ) ) = ( ( 𝐺 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑍 ) ) )
24 1 23 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑍 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑍 ) ) ) )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
26 20 renegcld ⊢ ( 𝜑 → - ( 𝐺 ‘ 𝑍 ) ∈ ℝ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → - ( 𝐺 ‘ 𝑍 ) ∈ ℝ )
28 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) = ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) )
29 28 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ - ( 𝐺 ‘ 𝑍 ) ∈ ℝ ) → ( ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ‘ 𝑡 ) = - ( 𝐺 ‘ 𝑍 ) )
30 25 27 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ‘ 𝑡 ) = - ( 𝐺 ‘ 𝑍 ) )
31 30 oveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ‘ 𝑡 ) ) = ( ( 𝐺 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑍 ) ) )
32 1 31 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑍 ) ) ) )
33 26 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ - ( 𝐺 ‘ 𝑍 ) ∈ ℝ ) )
34 eleq1 ⊢ ( 𝑥 = - ( 𝐺 ‘ 𝑍 ) → ( 𝑥 ∈ ℝ ↔ - ( 𝐺 ‘ 𝑍 ) ∈ ℝ ) )
35 34 anbi2d ⊢ ( 𝑥 = - ( 𝐺 ‘ 𝑍 ) → ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ↔ ( 𝜑 ∧ - ( 𝐺 ‘ 𝑍 ) ∈ ℝ ) ) )
36 nfcv ⊢ Ⅎ 𝑡 𝑍
37 2 36 nffv ⊢ Ⅎ 𝑡 ( 𝐺 ‘ 𝑍 )
38 37 nfneg ⊢ Ⅎ 𝑡 - ( 𝐺 ‘ 𝑍 )
39 38 nfeq2 ⊢ Ⅎ 𝑡 𝑥 = - ( 𝐺 ‘ 𝑍 )
40 simpl ⊢ ( ( 𝑥 = - ( 𝐺 ‘ 𝑍 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑥 = - ( 𝐺 ‘ 𝑍 ) )
41 39 40 mpteq2da ⊢ ( 𝑥 = - ( 𝐺 ‘ 𝑍 ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) = ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) )
42 41 eleq1d ⊢ ( 𝑥 = - ( 𝐺 ‘ 𝑍 ) → ( ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ∈ 𝐴 ) )
43 35 42 imbi12d ⊢ ( 𝑥 = - ( 𝐺 ‘ 𝑍 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ - ( 𝐺 ‘ 𝑍 ) ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ∈ 𝐴 ) ) )
44 43 6 vtoclg ⊢ ( - ( 𝐺 ‘ 𝑍 ) ∈ ℝ → ( ( 𝜑 ∧ - ( 𝐺 ‘ 𝑍 ) ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ∈ 𝐴 ) )
45 26 33 44 sylc ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ∈ 𝐴 )
46 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) )
47 5 2 46 stoweidlem8 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
48 9 45 47 mpd3an23 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ - ( 𝐺 ‘ 𝑍 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
49 32 48 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑍 ) ) ) ∈ 𝐴 )
50 24 49 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑍 ) ) ) ∈ 𝐴 )
51 3 50 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ 𝐴 )
52 17 7 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) ∈ ℝ )
53 52 recnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) ∈ ℂ )
54 20 recnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑍 ) ∈ ℂ )
55 53 54 10 subne0d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑆 ) − ( 𝐺 ‘ 𝑍 ) ) ≠ 0 )
56 52 20 resubcld ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑆 ) − ( 𝐺 ‘ 𝑍 ) ) ∈ ℝ )
57 nfcv ⊢ Ⅎ 𝑡 𝑆
58 2 57 nffv ⊢ Ⅎ 𝑡 ( 𝐺 ‘ 𝑆 )
59 nfcv ⊢ Ⅎ 𝑡 −
60 58 59 37 nfov ⊢ Ⅎ 𝑡 ( ( 𝐺 ‘ 𝑆 ) − ( 𝐺 ‘ 𝑍 ) )
61 fveq2 ⊢ ( 𝑡 = 𝑆 → ( 𝐺 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑆 ) )
62 61 oveq1d ⊢ ( 𝑡 = 𝑆 → ( ( 𝐺 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑍 ) ) = ( ( 𝐺 ‘ 𝑆 ) − ( 𝐺 ‘ 𝑍 ) ) )
63 57 60 62 3 fvmptf ⊢ ( ( 𝑆 ∈ 𝑇 ∧ ( ( 𝐺 ‘ 𝑆 ) − ( 𝐺 ‘ 𝑍 ) ) ∈ ℝ ) → ( 𝐻 ‘ 𝑆 ) = ( ( 𝐺 ‘ 𝑆 ) − ( 𝐺 ‘ 𝑍 ) ) )
64 7 56 63 syl2anc ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑆 ) = ( ( 𝐺 ‘ 𝑆 ) − ( 𝐺 ‘ 𝑍 ) ) )
65 20 20 resubcld ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑍 ) − ( 𝐺 ‘ 𝑍 ) ) ∈ ℝ )
66 37 59 37 nfov ⊢ Ⅎ 𝑡 ( ( 𝐺 ‘ 𝑍 ) − ( 𝐺 ‘ 𝑍 ) )
67 fveq2 ⊢ ( 𝑡 = 𝑍 → ( 𝐺 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑍 ) )
68 67 oveq1d ⊢ ( 𝑡 = 𝑍 → ( ( 𝐺 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑍 ) ) = ( ( 𝐺 ‘ 𝑍 ) − ( 𝐺 ‘ 𝑍 ) ) )
69 36 66 68 3 fvmptf ⊢ ( ( 𝑍 ∈ 𝑇 ∧ ( ( 𝐺 ‘ 𝑍 ) − ( 𝐺 ‘ 𝑍 ) ) ∈ ℝ ) → ( 𝐻 ‘ 𝑍 ) = ( ( 𝐺 ‘ 𝑍 ) − ( 𝐺 ‘ 𝑍 ) ) )
70 8 65 69 syl2anc ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑍 ) = ( ( 𝐺 ‘ 𝑍 ) − ( 𝐺 ‘ 𝑍 ) ) )
71 54 subidd ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑍 ) − ( 𝐺 ‘ 𝑍 ) ) = 0 )
72 70 71 eqtrd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑍 ) = 0 )
73 55 64 72 3netr4d ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑆 ) ≠ ( 𝐻 ‘ 𝑍 ) )
74 51 73 72 3jca ⊢ ( 𝜑 → ( 𝐻 ∈ 𝐴 ∧ ( 𝐻 ‘ 𝑆 ) ≠ ( 𝐻 ‘ 𝑍 ) ∧ ( 𝐻 ‘ 𝑍 ) = 0 ) )