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 𝐾 )