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 = \cdot_{𝑠OLD} (U)$
	ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
	ipasslem7.a	$⊢ A \in X$
	ipasslem7.b	$⊢ B \in X$
	ipasslem7.f	$⊢ F = (w \in ℝ ⟼ ((w S A) P B) - w (A P B))$
	ipasslem7.j	$⊢ J = topGen (ran (.))$
	ipasslem7.k	$⊢ K = TopOpen (ℂ_{fld})$
Assertion	ipasslem7	$⊢ F \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	$⊢ X = BaseSet (U)$
2		ip1i.2	$⊢ G = +_{v} (U)$
3		ip1i.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
5		ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
6		ipasslem7.a	$⊢ A \in X$
7		ipasslem7.b	$⊢ B \in X$
8		ipasslem7.f	$⊢ F = (w \in ℝ ⟼ ((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 \in TopOn (ℂ)$
14	13	a1i	$⊢ ⊤ \to K \in TopOn (ℂ)$
15		ax-resscn	$⊢ ℝ \subseteq ℂ$
16	15	a1i	$⊢ ⊤ \to ℝ \subseteq ℂ$
17	14	cnmptid	$⊢ ⊤ \to (w \in ℂ ⟼ w) \in (K Cn K)$
18	5	phnvi	$⊢ U \in NrmCVec$
19		eqid	$⊢ IndMet (U) = IndMet (U)$
20	1 19	imsxmet	$⊢ U \in NrmCVec \to IndMet (U) \in ∞Met (X)$
21	18 20	ax-mp	$⊢ IndMet (U) \in ∞Met (X)$
22		eqid	$⊢ MetOpen (IndMet (U)) = MetOpen (IndMet (U))$
23	22	mopntopon	$⊢ IndMet (U) \in ∞Met (X) \to MetOpen (IndMet (U)) \in TopOn (X)$
24	21 23	mp1i	$⊢ ⊤ \to MetOpen (IndMet (U)) \in TopOn (X)$
25	6	a1i	$⊢ ⊤ \to A \in X$
26	14 24 25	cnmptc	$⊢ ⊤ \to (w \in ℂ ⟼ A) \in (K Cn MetOpen (IndMet (U)))$
27	19 22 3 10	smcn	$⊢ U \in NrmCVec \to S \in ((K \times_{t} MetOpen (IndMet (U))) Cn MetOpen (IndMet (U)))$
28	18 27	mp1i	$⊢ ⊤ \to S \in ((K \times_{t} MetOpen (IndMet (U))) Cn MetOpen (IndMet (U)))$
29	14 17 26 28	cnmpt12f	$⊢ ⊤ \to (w \in ℂ ⟼ w S A) \in (K Cn MetOpen (IndMet (U)))$
30	7	a1i	$⊢ ⊤ \to B \in X$
31	14 24 30	cnmptc	$⊢ ⊤ \to (w \in ℂ ⟼ B) \in (K Cn MetOpen (IndMet (U)))$
32	4 19 22 10	dipcn	$⊢ U \in NrmCVec \to P \in ((MetOpen (IndMet (U)) \times_{t} MetOpen (IndMet (U))) Cn K)$
33	18 32	mp1i	$⊢ ⊤ \to P \in ((MetOpen (IndMet (U)) \times_{t} MetOpen (IndMet (U))) Cn K)$
34	14 29 31 33	cnmpt12f	$⊢ ⊤ \to (w \in ℂ ⟼ (w S A) P B) \in (K Cn K)$
35	1 4	dipcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B \in ℂ$
36	18 6 7 35	mp3an	$⊢ A P B \in ℂ$
37	36	a1i	$⊢ ⊤ \to A P B \in ℂ$
38	14 14 37	cnmptc	$⊢ ⊤ \to (w \in ℂ ⟼ A P B) \in (K Cn K)$
39	10	mulcn	$⊢ \times \in ((K \times_{t} K) Cn K)$
40	39	a1i	$⊢ ⊤ \to \times \in ((K \times_{t} K) Cn K)$
41	14 17 38 40	cnmpt12f	$⊢ ⊤ \to (w \in ℂ ⟼ w (A P B)) \in (K Cn K)$
42	10	subcn	$⊢ - \in ((K \times_{t} K) Cn K)$
43	42	a1i	$⊢ ⊤ \to - \in ((K \times_{t} K) Cn K)$
44	14 34 41 43	cnmpt12f	$⊢ ⊤ \to (w \in ℂ ⟼ ((w S A) P B) - w (A P B)) \in (K Cn K)$
45	12 14 16 44	cnmpt1res	$⊢ ⊤ \to (w \in ℝ ⟼ ((w S A) P B) - w (A P B)) \in (J Cn K)$
46	45	mptru	$⊢ (w \in ℝ ⟼ ((w S A) P B) - w (A P B)) \in (J Cn K)$
47	8 46	eqeltri	$⊢ F \in (J Cn K)$

Metamath Proof Explorer

Theorem ipasslem7

Proof