Metamath Proof Explorer

Theorem ipasslem7

Description: Lemma for ipassi . Show that ( ( w S A ) P B ) - ( w x. ( A P B ) ) is continuous on RR . (Contributed by NM, 23-Aug-2007) (Revised by Mario Carneiro, 6-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 ⊢ X = BaseSet ⁡ U
ip1i.2 ⊢ G = + v ⁡ U
ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
ip1i.9 ⊢ U ∈ CPreHil OLD
ipasslem7.a ⊢ A ∈ X
ipasslem7.b ⊢ B ∈ X
ipasslem7.f ⊢ F = w ∈ ℝ ⟼ w S A P B − w ⁢ A P B
ipasslem7.j ⊢ J = topGen ⁡ ran ⁡ .
ipasslem7.k ⊢ K = TopOpen ⁡ ℂ fld
Assertion ipasslem7 ⊢ F ∈ J Cn K

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ X = BaseSet ⁡ U
2 ip1i.2 ⊢ G = + v ⁡ U
3 ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
5 ip1i.9 ⊢ U ∈ CPreHil OLD
6 ipasslem7.a ⊢ A ∈ X
7 ipasslem7.b ⊢ B ∈ X
8 ipasslem7.f ⊢ F = w ∈ ℝ ⟼ w S A P B − w ⁢ A P B
9 ipasslem7.j ⊢ J = topGen ⁡ ran ⁡ .
10 ipasslem7.k ⊢ K = TopOpen ⁡ ℂ fld
11 10 tgioo2 ⊢ topGen ⁡ ran ⁡ . = K ↾ 𝑡 ℝ
12 9 11 eqtri ⊢ J = K ↾ 𝑡 ℝ
13 10 cnfldtopon ⊢ K ∈ TopOn ⁡ ℂ
14 13 a1i ⊢ ⊤ → K ∈ TopOn ⁡ ℂ
15 ax-resscn ⊢ ℝ ⊆ ℂ
16 15 a1i ⊢ ⊤ → ℝ ⊆ ℂ
17 14 cnmptid ⊢ ⊤ → w ∈ ℂ ⟼ w ∈ K Cn K
18 5 phnvi ⊢ U ∈ NrmCVec
19 eqid ⊢ IndMet ⁡ U = IndMet ⁡ U
20 1 19 imsxmet ⊢ U ∈ NrmCVec → IndMet ⁡ U ∈ ∞Met ⁡ X
21 18 20 ax-mp ⊢ IndMet ⁡ U ∈ ∞Met ⁡ X
22 eqid ⊢ MetOpen ⁡ IndMet ⁡ U = MetOpen ⁡ IndMet ⁡ U
23 22 mopntopon ⊢ IndMet ⁡ U ∈ ∞Met ⁡ X → MetOpen ⁡ IndMet ⁡ U ∈ TopOn ⁡ X
24 21 23 mp1i ⊢ ⊤ → MetOpen ⁡ IndMet ⁡ U ∈ TopOn ⁡ X
25 6 a1i ⊢ ⊤ → A ∈ X
26 14 24 25 cnmptc ⊢ ⊤ → w ∈ ℂ ⟼ A ∈ K Cn MetOpen ⁡ IndMet ⁡ U
27 19 22 3 10 smcn ⊢ U ∈ NrmCVec → S ∈ K × t MetOpen ⁡ IndMet ⁡ U Cn MetOpen ⁡ IndMet ⁡ U
28 18 27 mp1i ⊢ ⊤ → S ∈ K × t MetOpen ⁡ IndMet ⁡ U Cn MetOpen ⁡ IndMet ⁡ U
29 14 17 26 28 cnmpt12f ⊢ ⊤ → w ∈ ℂ ⟼ w S A ∈ K Cn MetOpen ⁡ IndMet ⁡ U
30 7 a1i ⊢ ⊤ → B ∈ X
31 14 24 30 cnmptc ⊢ ⊤ → w ∈ ℂ ⟼ B ∈ K Cn MetOpen ⁡ IndMet ⁡ U
32 4 19 22 10 dipcn ⊢ U ∈ NrmCVec → P ∈ MetOpen ⁡ IndMet ⁡ U × t MetOpen ⁡ IndMet ⁡ U Cn K
33 18 32 mp1i ⊢ ⊤ → P ∈ MetOpen ⁡ IndMet ⁡ U × t MetOpen ⁡ IndMet ⁡ U Cn K
34 14 29 31 33 cnmpt12f ⊢ ⊤ → w ∈ ℂ ⟼ w S A P B ∈ K Cn K
35 1 4 dipcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ∈ ℂ
36 18 6 7 35 mp3an ⊢ A P B ∈ ℂ
37 36 a1i ⊢ ⊤ → A P B ∈ ℂ
38 14 14 37 cnmptc ⊢ ⊤ → w ∈ ℂ ⟼ A P B ∈ K Cn K
39 10 mulcn ⊢ × ∈ K × t K Cn K
40 39 a1i ⊢ ⊤ → × ∈ K × t K Cn K
41 14 17 38 40 cnmpt12f ⊢ ⊤ → w ∈ ℂ ⟼ w ⁢ A P B ∈ K Cn K
42 10 subcn ⊢ − ∈ K × t K Cn K
43 42 a1i ⊢ ⊤ → − ∈ K × t K Cn K
44 14 34 41 43 cnmpt12f ⊢ ⊤ → w ∈ ℂ ⟼ w S A P B − w ⁢ A P B ∈ K Cn K
45 12 14 16 44 cnmpt1res ⊢ ⊤ → w ∈ ℝ ⟼ w S A P B − w ⁢ A P B ∈ J Cn K
46 45 mptru ⊢ w ∈ ℝ ⟼ w S A P B − w ⁢ A P B ∈ J Cn K
47 8 46 eqeltri ⊢ F ∈ J Cn K