Metamath Proof Explorer

Theorem stoweidlem36

Description: This lemma is used to prove the existence of a function p_t as in Lemma 1 of BrosowskiDeutsh p. 90 (at the beginning of Lemma 1): 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. Z is used for t_0 , S is used for t e. T - U , h is used for p_t . G is used for (h_t)^2 and the final h is a normalized version of G ( divided by its norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem36.1 ⊢ Ⅎ ℎ 𝑄
stoweidlem36.2 ⊢ Ⅎ 𝑡 𝐻
stoweidlem36.3 ⊢ Ⅎ 𝑡 𝐹
stoweidlem36.4 ⊢ Ⅎ 𝑡 𝐺
stoweidlem36.5 ⊢ Ⅎ 𝑡 𝜑
stoweidlem36.6 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem36.7 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
stoweidlem36.8 ⊢ 𝑇 = ∪ 𝐽
stoweidlem36.9 ⊢ 𝐺 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) )
stoweidlem36.10 ⊢ 𝑁 = sup ( ran 𝐺 , ℝ , < )
stoweidlem36.11 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) )
stoweidlem36.12 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
stoweidlem36.13 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
stoweidlem36.14 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem36.15 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem36.16 ⊢ ( 𝜑 → 𝑆 ∈ 𝑇 )
stoweidlem36.17 ⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
stoweidlem36.18 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
stoweidlem36.19 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑆 ) ≠ ( 𝐹 ‘ 𝑍 ) )
stoweidlem36.20 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑍 ) = 0 )
Assertion stoweidlem36 ( 𝜑 → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem36.1 ⊢ Ⅎ ℎ 𝑄
2 stoweidlem36.2 ⊢ Ⅎ 𝑡 𝐻
3 stoweidlem36.3 ⊢ Ⅎ 𝑡 𝐹
4 stoweidlem36.4 ⊢ Ⅎ 𝑡 𝐺
5 stoweidlem36.5 ⊢ Ⅎ 𝑡 𝜑
6 stoweidlem36.6 ⊢ 𝐾 = ( topGen ‘ ran (,) )
7 stoweidlem36.7 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
8 stoweidlem36.8 ⊢ 𝑇 = ∪ 𝐽
9 stoweidlem36.9 ⊢ 𝐺 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) )
10 stoweidlem36.10 ⊢ 𝑁 = sup ( ran 𝐺 , ℝ , < )
11 stoweidlem36.11 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) )
12 stoweidlem36.12 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
13 stoweidlem36.13 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
14 stoweidlem36.14 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
15 stoweidlem36.15 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
16 stoweidlem36.16 ⊢ ( 𝜑 → 𝑆 ∈ 𝑇 )
17 stoweidlem36.17 ⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
18 stoweidlem36.18 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
19 stoweidlem36.19 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑆 ) ≠ ( 𝐹 ‘ 𝑍 ) )
20 stoweidlem36.20 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑍 ) = 0 )
21 eqid ⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 )
22 3 nfeq2 ⊢ Ⅎ 𝑡 𝑓 = 𝐹
23 3 nfeq2 ⊢ Ⅎ 𝑡 𝑔 = 𝐹
24 22 23 14 stoweidlem6 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) ) ∈ 𝐴 )
25 18 18 24 mpd3an23 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) ) ∈ 𝐴 )
26 9 25 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
27 13 26 sseldd ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
28 6 8 21 27 fcnre ⊢ ( 𝜑 → 𝐺 : 𝑇 ⟶ ℝ )
29 28 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ )
30 29 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℂ )
31 16 ne0d ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
32 8 6 12 27 31 cncmpmax ⊢ ( 𝜑 → ( sup ( ran 𝐺 , ℝ , < ) ∈ ran 𝐺 ∧ sup ( ran 𝐺 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑠 ∈ 𝑇 ( 𝐺 ‘ 𝑠 ) ≤ sup ( ran 𝐺 , ℝ , < ) ) )
33 32 simp2d ⊢ ( 𝜑 → sup ( ran 𝐺 , ℝ , < ) ∈ ℝ )
34 10 33 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
35 34 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ℂ )
37 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
38 28 16 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) ∈ ℝ )
39 13 18 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
40 6 8 21 39 fcnre ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
41 40 16 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑆 ) ∈ ℝ )
42 19 20 neeqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑆 ) ≠ 0 )
43 41 42 msqgt0d ⊢ ( 𝜑 → 0 < ( ( 𝐹 ‘ 𝑆 ) · ( 𝐹 ‘ 𝑆 ) ) )
44 41 41 remulcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑆 ) · ( 𝐹 ‘ 𝑆 ) ) ∈ ℝ )
45 nfcv ⊢ Ⅎ 𝑡 𝑆
46 3 45 nffv ⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑆 )
47 nfcv ⊢ Ⅎ 𝑡 ·
48 46 47 46 nfov ⊢ Ⅎ 𝑡 ( ( 𝐹 ‘ 𝑆 ) · ( 𝐹 ‘ 𝑆 ) )
49 fveq2 ⊢ ( 𝑡 = 𝑆 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑆 ) )
50 49 49 oveq12d ⊢ ( 𝑡 = 𝑆 → ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑆 ) · ( 𝐹 ‘ 𝑆 ) ) )
51 45 48 50 9 fvmptf ⊢ ( ( 𝑆 ∈ 𝑇 ∧ ( ( 𝐹 ‘ 𝑆 ) · ( 𝐹 ‘ 𝑆 ) ) ∈ ℝ ) → ( 𝐺 ‘ 𝑆 ) = ( ( 𝐹 ‘ 𝑆 ) · ( 𝐹 ‘ 𝑆 ) ) )
52 16 44 51 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = ( ( 𝐹 ‘ 𝑆 ) · ( 𝐹 ‘ 𝑆 ) ) )
53 43 52 breqtrrd ⊢ ( 𝜑 → 0 < ( 𝐺 ‘ 𝑆 ) )
54 32 simp3d ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑇 ( 𝐺 ‘ 𝑠 ) ≤ sup ( ran 𝐺 , ℝ , < ) )
55 fveq2 ⊢ ( 𝑠 = 𝑆 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑆 ) )
56 55 breq1d ⊢ ( 𝑠 = 𝑆 → ( ( 𝐺 ‘ 𝑠 ) ≤ sup ( ran 𝐺 , ℝ , < ) ↔ ( 𝐺 ‘ 𝑆 ) ≤ sup ( ran 𝐺 , ℝ , < ) ) )
57 56 rspccva ⊢ ( ( ∀ 𝑠 ∈ 𝑇 ( 𝐺 ‘ 𝑠 ) ≤ sup ( ran 𝐺 , ℝ , < ) ∧ 𝑆 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑆 ) ≤ sup ( ran 𝐺 , ℝ , < ) )
58 54 16 57 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) ≤ sup ( ran 𝐺 , ℝ , < ) )
59 37 38 33 53 58 ltletrd ⊢ ( 𝜑 → 0 < sup ( ran 𝐺 , ℝ , < ) )
60 59 gt0ne0d ⊢ ( 𝜑 → sup ( ran 𝐺 , ℝ , < ) ≠ 0 )
61 10 neeq1i ⊢ ( 𝑁 ≠ 0 ↔ sup ( ran 𝐺 , ℝ , < ) ≠ 0 )
62 60 61 sylibr ⊢ ( 𝜑 → 𝑁 ≠ 0 )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ≠ 0 )
64 30 36 63 divrecd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) = ( ( 𝐺 ‘ 𝑡 ) · ( 1 / 𝑁 ) ) )
65 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
66 34 62 rereccld ⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 / 𝑁 ) ∈ ℝ )
68 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) )
69 68 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( 1 / 𝑁 ) ∈ ℝ ) → ( ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ‘ 𝑡 ) = ( 1 / 𝑁 ) )
70 65 67 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ‘ 𝑡 ) = ( 1 / 𝑁 ) )
71 70 oveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) · ( ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ‘ 𝑡 ) ) = ( ( 𝐺 ‘ 𝑡 ) · ( 1 / 𝑁 ) ) )
72 64 71 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) = ( ( 𝐺 ‘ 𝑡 ) · ( ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ‘ 𝑡 ) ) )
73 5 72 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) · ( ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ‘ 𝑡 ) ) ) )
74 11 73 syl5eq ⊢ ( 𝜑 → 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) · ( ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ‘ 𝑡 ) ) ) )
75 15 stoweidlem4 ⊢ ( ( 𝜑 ∧ ( 1 / 𝑁 ) ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ∈ 𝐴 )
76 66 75 mpdan ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ∈ 𝐴 )
77 4 nfeq2 ⊢ Ⅎ 𝑡 𝑓 = 𝐺
78 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) )
79 78 nfeq2 ⊢ Ⅎ 𝑡 𝑔 = ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) )
80 77 79 14 stoweidlem6 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) · ( ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
81 26 76 80 mpd3an23 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐺 ‘ 𝑡 ) · ( ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑁 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
82 74 81 eqeltrd ⊢ ( 𝜑 → 𝐻 ∈ 𝐴 )
83 28 17 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑍 ) ∈ ℝ )
84 83 34 62 redivcld ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑍 ) / 𝑁 ) ∈ ℝ )
85 nfcv ⊢ Ⅎ 𝑡 𝑍
86 4 85 nffv ⊢ Ⅎ 𝑡 ( 𝐺 ‘ 𝑍 )
87 nfcv ⊢ Ⅎ 𝑡 /
88 nfcv ⊢ Ⅎ 𝑡 𝑁
89 86 87 88 nfov ⊢ Ⅎ 𝑡 ( ( 𝐺 ‘ 𝑍 ) / 𝑁 )
90 fveq2 ⊢ ( 𝑡 = 𝑍 → ( 𝐺 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑍 ) )
91 90 oveq1d ⊢ ( 𝑡 = 𝑍 → ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) = ( ( 𝐺 ‘ 𝑍 ) / 𝑁 ) )
92 85 89 91 11 fvmptf ⊢ ( ( 𝑍 ∈ 𝑇 ∧ ( ( 𝐺 ‘ 𝑍 ) / 𝑁 ) ∈ ℝ ) → ( 𝐻 ‘ 𝑍 ) = ( ( 𝐺 ‘ 𝑍 ) / 𝑁 ) )
93 17 84 92 syl2anc ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑍 ) = ( ( 𝐺 ‘ 𝑍 ) / 𝑁 ) )
94 0re ⊢ 0 ∈ ℝ
95 20 94 eqeltrdi ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑍 ) ∈ ℝ )
96 95 95 remulcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑍 ) · ( 𝐹 ‘ 𝑍 ) ) ∈ ℝ )
97 3 85 nffv ⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑍 )
98 97 47 97 nfov ⊢ Ⅎ 𝑡 ( ( 𝐹 ‘ 𝑍 ) · ( 𝐹 ‘ 𝑍 ) )
99 fveq2 ⊢ ( 𝑡 = 𝑍 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑍 ) )
100 99 99 oveq12d ⊢ ( 𝑡 = 𝑍 → ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑍 ) · ( 𝐹 ‘ 𝑍 ) ) )
101 85 98 100 9 fvmptf ⊢ ( ( 𝑍 ∈ 𝑇 ∧ ( ( 𝐹 ‘ 𝑍 ) · ( 𝐹 ‘ 𝑍 ) ) ∈ ℝ ) → ( 𝐺 ‘ 𝑍 ) = ( ( 𝐹 ‘ 𝑍 ) · ( 𝐹 ‘ 𝑍 ) ) )
102 17 96 101 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑍 ) = ( ( 𝐹 ‘ 𝑍 ) · ( 𝐹 ‘ 𝑍 ) ) )
103 20 20 oveq12d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑍 ) · ( 𝐹 ‘ 𝑍 ) ) = ( 0 · 0 ) )
104 0cn ⊢ 0 ∈ ℂ
105 104 mul02i ⊢ ( 0 · 0 ) = 0
106 103 105 eqtrdi ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑍 ) · ( 𝐹 ‘ 𝑍 ) ) = 0 )
107 102 106 eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑍 ) = 0 )
108 107 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑍 ) / 𝑁 ) = ( 0 / 𝑁 ) )
109 35 62 div0d ⊢ ( 𝜑 → ( 0 / 𝑁 ) = 0 )
110 93 108 109 3eqtrd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑍 ) = 0 )
111 40 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
112 111 msqge0d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) )
113 111 111 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
114 9 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ) → ( 𝐺 ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) )
115 65 113 114 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) )
116 112 115 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝐺 ‘ 𝑡 ) )
117 34 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ℝ )
118 59 10 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑁 )
119 118 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 < 𝑁 )
120 divge0 ⊢ ( ( ( ( 𝐺 ‘ 𝑡 ) ∈ ℝ ∧ 0 ≤ ( 𝐺 ‘ 𝑡 ) ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → 0 ≤ ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) )
121 29 116 117 119 120 syl22anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) )
122 29 117 63 redivcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) ∈ ℝ )
123 11 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) ∈ ℝ ) → ( 𝐻 ‘ 𝑡 ) = ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) )
124 65 122 123 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) = ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) )
125 121 124 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝐻 ‘ 𝑡 ) )
126 30 div1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) / 1 ) = ( 𝐺 ‘ 𝑡 ) )
127 fveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑡 ) )
128 127 breq1d ⊢ ( 𝑠 = 𝑡 → ( ( 𝐺 ‘ 𝑠 ) ≤ sup ( ran 𝐺 , ℝ , < ) ↔ ( 𝐺 ‘ 𝑡 ) ≤ sup ( ran 𝐺 , ℝ , < ) ) )
129 128 rspccva ⊢ ( ( ∀ 𝑠 ∈ 𝑇 ( 𝐺 ‘ 𝑠 ) ≤ sup ( ran 𝐺 , ℝ , < ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ≤ sup ( ran 𝐺 , ℝ , < ) )
130 54 129 sylan ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ≤ sup ( ran 𝐺 , ℝ , < ) )
131 130 10 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ≤ 𝑁 )
132 126 131 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) / 1 ) ≤ 𝑁 )
133 1red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℝ )
134 0lt1 ⊢ 0 < 1
135 134 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 < 1 )
136 lediv23 ⊢ ( ( ( 𝐺 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ∧ ( 1 ∈ ℝ ∧ 0 < 1 ) ) → ( ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) ≤ 1 ↔ ( ( 𝐺 ‘ 𝑡 ) / 1 ) ≤ 𝑁 ) )
137 29 117 119 133 135 136 syl122anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) ≤ 1 ↔ ( ( 𝐺 ‘ 𝑡 ) / 1 ) ≤ 𝑁 ) )
138 132 137 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) ≤ 1 )
139 124 138 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) ≤ 1 )
140 125 139 jca ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) )
141 140 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) )
142 5 141 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) )
143 110 142 jca ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) )
144 fveq1 ⊢ ( ℎ = 𝐻 → ( ℎ ‘ 𝑍 ) = ( 𝐻 ‘ 𝑍 ) )
145 144 eqeq1d ⊢ ( ℎ = 𝐻 → ( ( ℎ ‘ 𝑍 ) = 0 ↔ ( 𝐻 ‘ 𝑍 ) = 0 ) )
146 2 nfeq2 ⊢ Ⅎ 𝑡 ℎ = 𝐻
147 fveq1 ⊢ ( ℎ = 𝐻 → ( ℎ ‘ 𝑡 ) = ( 𝐻 ‘ 𝑡 ) )
148 147 breq2d ⊢ ( ℎ = 𝐻 → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( 𝐻 ‘ 𝑡 ) ) )
149 147 breq1d ⊢ ( ℎ = 𝐻 → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) )
150 148 149 anbi12d ⊢ ( ℎ = 𝐻 → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) )
151 146 150 ralbid ⊢ ( ℎ = 𝐻 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) )
152 145 151 anbi12d ⊢ ( ℎ = 𝐻 → ( ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) ↔ ( ( 𝐻 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) ) )
153 152 elrab ⊢ ( 𝐻 ∈ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } ↔ ( 𝐻 ∈ 𝐴 ∧ ( ( 𝐻 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) ) )
154 82 143 153 sylanbrc ⊢ ( 𝜑 → 𝐻 ∈ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } )
155 154 7 eleqtrrdi ⊢ ( 𝜑 → 𝐻 ∈ 𝑄 )
156 38 34 53 118 divgt0d ⊢ ( 𝜑 → 0 < ( ( 𝐺 ‘ 𝑆 ) / 𝑁 ) )
157 38 34 62 redivcld ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑆 ) / 𝑁 ) ∈ ℝ )
158 4 45 nffv ⊢ Ⅎ 𝑡 ( 𝐺 ‘ 𝑆 )
159 158 87 88 nfov ⊢ Ⅎ 𝑡 ( ( 𝐺 ‘ 𝑆 ) / 𝑁 )
160 fveq2 ⊢ ( 𝑡 = 𝑆 → ( 𝐺 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑆 ) )
161 160 oveq1d ⊢ ( 𝑡 = 𝑆 → ( ( 𝐺 ‘ 𝑡 ) / 𝑁 ) = ( ( 𝐺 ‘ 𝑆 ) / 𝑁 ) )
162 45 159 161 11 fvmptf ⊢ ( ( 𝑆 ∈ 𝑇 ∧ ( ( 𝐺 ‘ 𝑆 ) / 𝑁 ) ∈ ℝ ) → ( 𝐻 ‘ 𝑆 ) = ( ( 𝐺 ‘ 𝑆 ) / 𝑁 ) )
163 16 157 162 syl2anc ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑆 ) = ( ( 𝐺 ‘ 𝑆 ) / 𝑁 ) )
164 156 163 breqtrrd ⊢ ( 𝜑 → 0 < ( 𝐻 ‘ 𝑆 ) )
165 nfcv ⊢ Ⅎ ℎ 𝐻
166 1 nfel2 ⊢ Ⅎ ℎ 𝐻 ∈ 𝑄
167 nfv ⊢ Ⅎ ℎ 0 < ( 𝐻 ‘ 𝑆 )
168 166 167 nfan ⊢ Ⅎ ℎ ( 𝐻 ∈ 𝑄 ∧ 0 < ( 𝐻 ‘ 𝑆 ) )
169 eleq1 ⊢ ( ℎ = 𝐻 → ( ℎ ∈ 𝑄 ↔ 𝐻 ∈ 𝑄 ) )
170 fveq1 ⊢ ( ℎ = 𝐻 → ( ℎ ‘ 𝑆 ) = ( 𝐻 ‘ 𝑆 ) )
171 170 breq2d ⊢ ( ℎ = 𝐻 → ( 0 < ( ℎ ‘ 𝑆 ) ↔ 0 < ( 𝐻 ‘ 𝑆 ) ) )
172 169 171 anbi12d ⊢ ( ℎ = 𝐻 → ( ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) ↔ ( 𝐻 ∈ 𝑄 ∧ 0 < ( 𝐻 ‘ 𝑆 ) ) ) )
173 165 168 172 spcegf ⊢ ( 𝐻 ∈ 𝑄 → ( ( 𝐻 ∈ 𝑄 ∧ 0 < ( 𝐻 ‘ 𝑆 ) ) → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) ) )
174 173 anabsi5 ⊢ ( ( 𝐻 ∈ 𝑄 ∧ 0 < ( 𝐻 ‘ 𝑆 ) ) → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) )
175 155 164 174 syl2anc ⊢ ( 𝜑 → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) )