This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
ipasslem7.a ⊢ 𝐴 ∈ 𝑋
ipasslem7.b ⊢ 𝐵 ∈ 𝑋
ipasslem7.f ⊢ 𝐹 = ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) )
ipasslem7.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
ipasslem7.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion ipasslem7 𝐹 ∈ ( 𝐽 Cn 𝐾 )

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
5 ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
6 ipasslem7.a ⊢ 𝐴 ∈ 𝑋
7 ipasslem7.b ⊢ 𝐵 ∈ 𝑋
8 ipasslem7.f ⊢ 𝐹 = ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) )
9 ipasslem7.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
10 ipasslem7.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
11 10 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( 𝐾 ↾t ℝ )
12 9 11 eqtri ⊢ 𝐽 = ( 𝐾 ↾t ℝ )
13 10 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
14 13 a1i ⊢ ( ⊤ → 𝐾 ∈ ( TopOn ‘ ℂ ) )
15 ax-resscn ⊢ ℝ ⊆ ℂ
16 15 a1i ⊢ ( ⊤ → ℝ ⊆ ℂ )
17 14 cnmptid ⊢ ( ⊤ → ( 𝑤 ∈ ℂ ↦ 𝑤 ) ∈ ( 𝐾 Cn 𝐾 ) )
18 5 phnvi ⊢ 𝑈 ∈ NrmCVec
19 eqid ⊢ ( IndMet ‘ 𝑈 ) = ( IndMet ‘ 𝑈 )
20 1 19 imsxmet ⊢ ( 𝑈 ∈ NrmCVec → ( IndMet ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝑋 ) )
21 18 20 ax-mp ⊢ ( IndMet ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝑋 )
22 eqid ⊢ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) = ( MetOpen ‘ ( IndMet ‘ 𝑈 ) )
23 22 mopntopon ⊢ ( ( IndMet ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝑋 ) → ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ∈ ( TopOn ‘ 𝑋 ) )
24 21 23 mp1i ⊢ ( ⊤ → ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ∈ ( TopOn ‘ 𝑋 ) )
25 6 a1i ⊢ ( ⊤ → 𝐴 ∈ 𝑋 )
26 14 24 25 cnmptc ⊢ ( ⊤ → ( 𝑤 ∈ ℂ ↦ 𝐴 ) ∈ ( 𝐾 Cn ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) )
27 19 22 3 10 smcn ⊢ ( 𝑈 ∈ NrmCVec → 𝑆 ∈ ( ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) Cn ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) )
28 18 27 mp1i ⊢ ( ⊤ → 𝑆 ∈ ( ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) Cn ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) )
29 14 17 26 28 cnmpt12f ⊢ ( ⊤ → ( 𝑤 ∈ ℂ ↦ ( 𝑤 𝑆 𝐴 ) ) ∈ ( 𝐾 Cn ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) )
30 7 a1i ⊢ ( ⊤ → 𝐵 ∈ 𝑋 )
31 14 24 30 cnmptc ⊢ ( ⊤ → ( 𝑤 ∈ ℂ ↦ 𝐵 ) ∈ ( 𝐾 Cn ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) )
32 4 19 22 10 dipcn ⊢ ( 𝑈 ∈ NrmCVec → 𝑃 ∈ ( ( ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ×t ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) Cn 𝐾 ) )
33 18 32 mp1i ⊢ ( ⊤ → 𝑃 ∈ ( ( ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ×t ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) Cn 𝐾 ) )
34 14 29 31 33 cnmpt12f ⊢ ( ⊤ → ( 𝑤 ∈ ℂ ↦ ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) ) ∈ ( 𝐾 Cn 𝐾 ) )
35 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
36 18 6 7 35 mp3an ⊢ ( 𝐴 𝑃 𝐵 ) ∈ ℂ
37 36 a1i ⊢ ( ⊤ → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
38 14 14 37 cnmptc ⊢ ( ⊤ → ( 𝑤 ∈ ℂ ↦ ( 𝐴 𝑃 𝐵 ) ) ∈ ( 𝐾 Cn 𝐾 ) )
39 10 mulcn ⊢ · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
40 39 a1i ⊢ ( ⊤ → · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
41 14 17 38 40 cnmpt12f ⊢ ( ⊤ → ( 𝑤 ∈ ℂ ↦ ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ∈ ( 𝐾 Cn 𝐾 ) )
42 10 subcn ⊢ − ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
43 42 a1i ⊢ ( ⊤ → − ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
44 14 34 41 43 cnmpt12f ⊢ ( ⊤ → ( 𝑤 ∈ ℂ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ) ∈ ( 𝐾 Cn 𝐾 ) )
45 12 14 16 44 cnmpt1res ⊢ ( ⊤ → ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ) ∈ ( 𝐽 Cn 𝐾 ) )
46 45 mptru ⊢ ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ) ∈ ( 𝐽 Cn 𝐾 )
47 8 46 eqeltri ⊢ 𝐹 ∈ ( 𝐽 Cn 𝐾 )