Metamath Proof Explorer

Theorem stoweidlem43

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_t in the subalgebra, such that p_t( t_0 ) = 0 , p_t ( t ) > 0, and 0 <= p_t <= 1. Hera Z is used for t_0 , S is used for t e. T - U , h is used for p_t. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem43.1 ⊢ Ⅎ 𝑔 𝜑
stoweidlem43.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem43.3 ⊢ Ⅎ ℎ 𝑄
stoweidlem43.4 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem43.5 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
stoweidlem43.6 ⊢ 𝑇 = ∪ 𝐽
stoweidlem43.7 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
stoweidlem43.8 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
stoweidlem43.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem43.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem43.11 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem43.12 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑟 ) ≠ ( 𝑔 ‘ 𝑡 ) )
stoweidlem43.13 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
stoweidlem43.14 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
stoweidlem43.15 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑇 ∖ 𝑈 ) )
Assertion stoweidlem43 ( 𝜑 → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem43.1 ⊢ Ⅎ 𝑔 𝜑
2 stoweidlem43.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem43.3 ⊢ Ⅎ ℎ 𝑄
4 stoweidlem43.4 ⊢ 𝐾 = ( topGen ‘ ran (,) )
5 stoweidlem43.5 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
6 stoweidlem43.6 ⊢ 𝑇 = ∪ 𝐽
7 stoweidlem43.7 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
8 stoweidlem43.8 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
9 stoweidlem43.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10 stoweidlem43.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 )
11 stoweidlem43.11 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
12 stoweidlem43.12 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑟 ) ≠ ( 𝑔 ‘ 𝑡 ) )
13 stoweidlem43.13 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
14 stoweidlem43.14 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
15 stoweidlem43.15 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑇 ∖ 𝑈 ) )
16 nfv ⊢ Ⅎ 𝑔 ∃ 𝑓 ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 )
17 15 eldifad ⊢ ( 𝜑 → 𝑆 ∈ 𝑇 )
18 elunii ⊢ ( ( 𝑍 ∈ 𝑈 ∧ 𝑈 ∈ 𝐽 ) → 𝑍 ∈ ∪ 𝐽 )
19 14 13 18 syl2anc ⊢ ( 𝜑 → 𝑍 ∈ ∪ 𝐽 )
20 19 6 eleqtrrdi ⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
21 15 eldifbd ⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝑈 )
22 nelne2 ⊢ ( ( 𝑍 ∈ 𝑈 ∧ ¬ 𝑆 ∈ 𝑈 ) → 𝑍 ≠ 𝑆 )
23 14 21 22 syl2anc ⊢ ( 𝜑 → 𝑍 ≠ 𝑆 )
24 23 necomd ⊢ ( 𝜑 → 𝑆 ≠ 𝑍 )
25 17 20 24 3jca ⊢ ( 𝜑 → ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) )
26 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) ) → 𝑍 ∈ 𝑇 )
27 nfv ⊢ Ⅎ 𝑡 ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 )
28 2 27 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) )
29 nfv ⊢ Ⅎ 𝑡 ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 )
30 28 29 nfim ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) )
31 eleq1 ⊢ ( 𝑡 = 𝑍 → ( 𝑡 ∈ 𝑇 ↔ 𝑍 ∈ 𝑇 ) )
32 neeq2 ⊢ ( 𝑡 = 𝑍 → ( 𝑆 ≠ 𝑡 ↔ 𝑆 ≠ 𝑍 ) )
33 31 32 3anbi23d ⊢ ( 𝑡 = 𝑍 → ( ( 𝑆 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑆 ≠ 𝑡 ) ↔ ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) ) )
34 33 anbi2d ⊢ ( 𝑡 = 𝑍 → ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑆 ≠ 𝑡 ) ) ↔ ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) ) ) )
35 fveq2 ⊢ ( 𝑡 = 𝑍 → ( 𝑔 ‘ 𝑡 ) = ( 𝑔 ‘ 𝑍 ) )
36 35 neeq2d ⊢ ( 𝑡 = 𝑍 → ( ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑡 ) ↔ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) )
37 36 rexbidv ⊢ ( 𝑡 = 𝑍 → ( ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑡 ) ↔ ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) )
38 34 37 imbi12d ⊢ ( 𝑡 = 𝑍 → ( ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑆 ≠ 𝑡 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑡 ) ) ↔ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) )
39 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑆 ≠ 𝑡 ) ) → 𝑆 ∈ 𝑇 )
40 eleq1 ⊢ ( 𝑟 = 𝑆 → ( 𝑟 ∈ 𝑇 ↔ 𝑆 ∈ 𝑇 ) )
41 neeq1 ⊢ ( 𝑟 = 𝑆 → ( 𝑟 ≠ 𝑡 ↔ 𝑆 ≠ 𝑡 ) )
42 40 41 3anbi13d ⊢ ( 𝑟 = 𝑆 → ( ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ↔ ( 𝑆 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑆 ≠ 𝑡 ) ) )
43 42 anbi2d ⊢ ( 𝑟 = 𝑆 → ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) ↔ ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑆 ≠ 𝑡 ) ) ) )
44 fveq2 ⊢ ( 𝑟 = 𝑆 → ( 𝑔 ‘ 𝑟 ) = ( 𝑔 ‘ 𝑆 ) )
45 44 neeq1d ⊢ ( 𝑟 = 𝑆 → ( ( 𝑔 ‘ 𝑟 ) ≠ ( 𝑔 ‘ 𝑡 ) ↔ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑡 ) ) )
46 45 rexbidv ⊢ ( 𝑟 = 𝑆 → ( ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑟 ) ≠ ( 𝑔 ‘ 𝑡 ) ↔ ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑡 ) ) )
47 43 46 imbi12d ⊢ ( 𝑟 = 𝑆 → ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑟 ) ≠ ( 𝑔 ‘ 𝑡 ) ) ↔ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑆 ≠ 𝑡 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑡 ) ) ) )
48 12 a1i ⊢ ( 𝑟 ∈ 𝑇 → ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑟 ) ≠ ( 𝑔 ‘ 𝑡 ) ) )
49 47 48 vtoclga ⊢ ( 𝑆 ∈ 𝑇 → ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑆 ≠ 𝑡 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑡 ) ) )
50 39 49 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑆 ≠ 𝑡 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑡 ) )
51 30 38 50 vtoclg1f ⊢ ( 𝑍 ∈ 𝑇 → ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) )
52 26 51 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) )
53 df-rex ⊢ ( ∃ 𝑔 ∈ 𝐴 ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ↔ ∃ 𝑔 ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) )
54 52 53 sylib ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑇 ∧ 𝑍 ∈ 𝑇 ∧ 𝑆 ≠ 𝑍 ) ) → ∃ 𝑔 ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) )
55 25 54 mpdan ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) )
56 nfv ⊢ Ⅎ 𝑡 ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) )
57 2 56 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) )
58 nfcv ⊢ Ⅎ 𝑡 𝑔
59 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) )
60 eqid ⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 )
61 8 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
62 4 6 60 61 fcnre ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
63 62 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
64 9 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 )
65 11 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
66 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) → 𝑆 ∈ 𝑇 )
67 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) → 𝑍 ∈ 𝑇 )
68 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) → 𝑔 ∈ 𝐴 )
69 simprr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) → ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) )
70 57 58 59 63 64 65 66 67 68 69 stoweidlem23 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ∈ 𝐴 ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑆 ) ≠ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) = 0 ) )
71 eleq1 ⊢ ( 𝑓 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) → ( 𝑓 ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ∈ 𝐴 ) )
72 fveq1 ⊢ ( 𝑓 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) → ( 𝑓 ‘ 𝑆 ) = ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑆 ) )
73 fveq1 ⊢ ( 𝑓 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) → ( 𝑓 ‘ 𝑍 ) = ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) )
74 72 73 neeq12d ⊢ ( 𝑓 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) → ( ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ↔ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑆 ) ≠ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) ) )
75 73 eqeq1d ⊢ ( 𝑓 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) → ( ( 𝑓 ‘ 𝑍 ) = 0 ↔ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) = 0 ) )
76 71 74 75 3anbi123d ⊢ ( 𝑓 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) → ( ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ↔ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ∈ 𝐴 ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑆 ) ≠ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) = 0 ) ) )
77 76 spcegv ⊢ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ∈ 𝐴 → ( ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ∈ 𝐴 ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑆 ) ≠ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) = 0 ) → ∃ 𝑓 ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) )
78 77 3ad2ant1 ⊢ ( ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ∈ 𝐴 ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑆 ) ≠ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) = 0 ) → ( ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ∈ 𝐴 ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑆 ) ≠ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) = 0 ) → ∃ 𝑓 ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) )
79 78 pm2.43i ⊢ ( ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ∈ 𝐴 ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑆 ) ≠ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) ∧ ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑔 ‘ 𝑡 ) − ( 𝑔 ‘ 𝑍 ) ) ) ‘ 𝑍 ) = 0 ) → ∃ 𝑓 ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) )
80 70 79 syl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ( 𝑔 ‘ 𝑆 ) ≠ ( 𝑔 ‘ 𝑍 ) ) ) → ∃ 𝑓 ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) )
81 1 16 55 80 exlimdd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) )
82 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) ) ‘ 𝑡 ) / sup ( ran ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) ) , ℝ , < ) ) )
83 nfcv ⊢ Ⅎ 𝑡 𝑓
84 nfcv ⊢ Ⅎ 𝑡 ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) )
85 nfv ⊢ Ⅎ 𝑡 ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 )
86 2 85 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) )
87 fveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝑓 ‘ 𝑠 ) = ( 𝑓 ‘ 𝑡 ) )
88 87 87 oveq12d ⊢ ( 𝑠 = 𝑡 → ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) = ( ( 𝑓 ‘ 𝑡 ) · ( 𝑓 ‘ 𝑡 ) ) )
89 88 cbvmptv ⊢ ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑓 ‘ 𝑡 ) ) )
90 eqid ⊢ sup ( ran ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) ) , ℝ , < ) = sup ( ran ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) ) , ℝ , < )
91 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) ) ‘ 𝑡 ) / sup ( ran ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) ) , ℝ , < ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) ) ‘ 𝑡 ) / sup ( ran ( 𝑠 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑠 ) · ( 𝑓 ‘ 𝑠 ) ) ) , ℝ , < ) ) )
92 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) → 𝐽 ∈ Comp )
93 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
94 eleq1 ⊢ ( 𝑓 = 𝑘 → ( 𝑓 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
95 94 3anbi2d ⊢ ( 𝑓 = 𝑘 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) ) )
96 fveq1 ⊢ ( 𝑓 = 𝑘 → ( 𝑓 ‘ 𝑡 ) = ( 𝑘 ‘ 𝑡 ) )
97 96 oveq1d ⊢ ( 𝑓 = 𝑘 → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) = ( ( 𝑘 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) )
98 97 mpteq2dv ⊢ ( 𝑓 = 𝑘 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑘 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) )
99 98 eleq1d ⊢ ( 𝑓 = 𝑘 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑘 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
100 95 99 imbi12d ⊢ ( 𝑓 = 𝑘 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑘 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
101 100 10 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑘 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 )
102 101 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) ∧ 𝑘 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑘 ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝐴 )
103 11 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
104 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) → 𝑆 ∈ 𝑇 )
105 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) → 𝑍 ∈ 𝑇 )
106 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) → 𝑓 ∈ 𝐴 )
107 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) → ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) )
108 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) → ( 𝑓 ‘ 𝑍 ) = 0 )
109 3 82 83 84 86 4 5 6 89 90 91 92 93 102 103 104 105 106 107 108 stoweidlem36 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) ) → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) )
110 109 ex ⊢ ( 𝜑 → ( ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) ) )
111 110 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑆 ) ≠ ( 𝑓 ‘ 𝑍 ) ∧ ( 𝑓 ‘ 𝑍 ) = 0 ) → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) ) )
112 81 111 mpd ⊢ ( 𝜑 → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑆 ) ) )