Theorem ipasslem6 8491

Description: Lemma for ipassi 8497. Show that ((wSA)PB) - (w x. (APB)) is continuous in w.

Hypotheses

Ref	Expression
ip1i.1	|- X = (Base` U)
ip1i.2	|- G = (+v` U)
ip1i.4	|- S = (.s` U)
ip1i.7	|- P = (.i` U)
ip1i.9	|- U e. CPreHil
ipasslem6.a	|- A e. X
ipasslem6.b	|- B e. X
ipasslem6.d	|- D = (abs o. - )
ipasslem6.8	|- C = (IndMet` U)
ipasslem6.j	|- J = (Open` D)
ipasslem6.f	|- F = {<.w, v>. | (w e. CC /\ v = (((wSA)PB) - (w x. (APB))))}

Assertion

Ref	Expression
ipasslem6	|- F e. (J Cn J)

Distinct variable groups:   w,v,A   v,B,w   w,D   w,J   v,P,w   v,S,w

Proof of Theorem ipasslem6

Step	Hyp	Ref	Expression
1		ip1i.9	. . . . . . . 8 |- U e. CPreHil
2	1	phnvi 8471	. . . . . . 7 |- U e. NrmCVec
3		ipasslem6.a	. . . . . . 7 |- A e. X
4		ip1i.1	. . . . . . . 8 |- X = (Base` U)
5		ip1i.4	. . . . . . . 8 |- S = (.s` U)
6	4, 5	nvscl 8243	. . . . . . 7 |- ((U e. NrmCVec /\ u e. CC /\ A e. X) -> (uSA) e. X)
7	2, 3, 6	mp3an13 909	. . . . . 6 |- (u e. CC -> (uSA) e. X)
8	7	rgen 1701	. . . . 5 |- A.u e. CC (uSA) e. X
9		eqid 1478	. . . . . 6 |- {<.u, t>. | (u e. CC /\ t = (uSA))} = {<.u, t>. | (u e. CC /\ t = (uSA))}
10		oprex 3989	. . . . . 6 |- (uSA) e. V
11	9, 10	rnssopab 3831	. . . . 5 |- (A.u e. CC (uSA) e. X <-> ran {<.u, t>. | (u e. CC /\ t = (uSA))} (_ X)
12	8, 11	mpbi 189	. . . 4 |- ran {<.u, t>. | (u e. CC /\ t = (uSA))} (_ X
13		oprex 3989	. . . . 5 |- (sPB) e. V
14		oprex 3989	. . . . 5 |- ((uSA)PB) e. V
15		opreq1 3974	. . . . 5 |- (s = (uSA) -> (sPB) = ((uSA)PB))
16		eqid 1478	. . . . 5 |- {<.s, r>. | (s e. X /\ r = (sPB))} = {<.s, r>. | (s e. X /\ r = (sPB))}
17		eqid 1478	. . . . 5 |- {<.u, t>. | (u e. CC /\ t = ((uSA)PB))} = {<.u, t>. | (u e. CC /\ t = ((uSA)PB))}
18	10, 13, 14, 15, 9, 16, 17	fopabco 3838	. . . 4 |- (ran {<.u, t>. | (u e. CC /\ t = (uSA))} (_ X -> ({<.s, r>. | (s e. X /\ r = (sPB))} o. {<.u, t>. | (u e. CC /\ t = (uSA))}) = {<.u, t>. | (u e. CC /\ t = ((uSA)PB))})
19	12, 18	ax-mp 7	. . 3 |- ({<.s, r>. | (s e. X /\ r = (sPB))} o. {<.u, t>. | (u e. CC /\ t = (uSA))}) = {<.u, t>. | (u e. CC /\ t = ((uSA)PB))}
20		ipasslem6.d	. . . . . 6 |- D = (abs o. - )
21	20	cnmet 7901	. . . . 5 |- D e. Met
22		ipasslem6.8	. . . . . . 7 |- C = (IndMet` U)
23	22	imsmet 8320	. . . . . 6 |- (U e. NrmCVec -> C e. Met)
24	2, 23	ax-mp 7	. . . . 5 |- C e. Met
25	21, 24, 21	3pm3.2i 820	. . . 4 |- (D e. Met /\ C e. Met /\ D e. Met)
26		ipasslem6.j	. . . . . 6 |- J = (Open` D)
27		eqid 1478	. . . . . 6 |- (Open` C) = (Open` C)
28	4, 5, 20, 22, 26, 27, 9, 2, 3	sm1cni 8344	. . . . 5 |- {<.u, t>. | (u e. CC /\ t = (uSA))} e. (J Cn (Open` C))
29		ip1i.2	. . . . . 6 |- G = (+v` U)
30		ip1i.7	. . . . . 6 |- P = (.i` U)
31		ipasslem6.b	. . . . . 6 |- B e. X
32	4, 29, 30, 22, 20, 27, 26, 16, 2, 31	ip1cni 8375	. . . . 5 |- {<.s, r>. | (s e. X /\ r = (sPB))} e. ((Open` C) Cn J)
33	28, 32	pm3.2i 285	. . . 4 |- ({<.u, t>. | (u e. CC /\ t = (uSA))} e. (J Cn (Open` C)) /\ {<.s, r>. | (s e. X /\ r = (sPB))} e. ((Open` C) Cn J))
34	26, 27, 26	metcnco 7894	. . . 4 |- (((D e. Met /\ C e. Met /\ D e. Met) /\ ({<.u, t>. | (u e. CC /\ t = (uSA))} e. (J Cn (Open` C)) /\ {<.s, r>. | (s e. X /\ r = (sPB))} e. ((Open` C) Cn J))) -> ({<.s, r>. | (s e. X /\ r = (sPB))} o. {<.u, t>. | (u e. CC /\ t = (uSA))}) e. (J Cn J))
35	25, 33, 34	mp2an 699	. . 3 |- ({<.s, r>. | (s e. X /\ r = (sPB))} o. {<.u, t>. | (u e. CC /\ t = (uSA))}) e. (J Cn J)
36	19, 35	eqeltrr 1548	. 2 |- {<.u, t>. | (u e. CC /\ t = ((uSA)PB))} e. (J Cn J)
37	4, 30	ipcl 8361	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) e. CC)
38	2, 3, 31, 37	mp3an 918	. . 3 |- (APB) e. CC
39	20	cnmetba 7900	. . . 4 |- CC = dom dom D
40		eqid 1478	. . . 4 |- {<.<.s, r>., q>. | ((s e. (CC X. CC) /\ r e. (CC X. CC)) /\ q = sup({((1st` s)D(1st` r)), ((2nd` s)D(2nd` r))}, RR, < ))} = {<.<.s, r>., q>. | ((s e. (CC X. CC) /\ r e. (CC X. CC)) /\ q = sup({((1st` s)D(1st` r)), ((2nd` s)D(2nd` r))}, RR, < ))}
41		eqid 1478	. . . 4 |- (Open` {<.<.s, r>., q>. | ((s e. (CC X. CC) /\ r e. (CC X. CC)) /\ q = sup({((1st` s)D(1st` r)), ((2nd` s)D(2nd` r))}, RR, < ))}) = (Open` {<.<.s, r>., q>. | ((s e. (CC X. CC) /\ r e. (CC X. CC)) /\ q = sup({((1st` s)D(1st` r)), ((2nd` s)D(2nd` r))}, RR, < ))})
42	20, 40, 26, 41	mulcn 7985	. . . 4 |- x. e. ((Open` {<.<.s, r>., q>. | ((s e. (CC X. CC) /\ r e. (CC X. CC)) /\ q = sup({((1st` s)D(1st` r)), ((2nd` s)D(2nd` r))}, RR, < ))}) Cn J)
43		eqid 1478	. . . 4 |- {<.u, t>. | (u e. CC /\ t = (u x. (APB)))} = {<.u, t>. | (u e. CC /\ t = (u x. (APB)))}
44	39, 39, 21, 21, 21, 40, 26, 26, 41, 42, 43	opr1scn 7977	. . 3 |- ((APB) e. CC -> {<.u, t>. | (u e. CC /\ t = (u x. (APB)))} e. (J Cn J))
45	38, 44	ax-mp 7	. 2 |- {<.u, t>. | (u e. CC /\ t = (u x. (APB)))} e. (J Cn J)
46	20, 40, 26, 41	subcn 7984	. . 3 |- - e. ((Open` {<.<.s, r>., q>. | ((s e. (CC X. CC) /\ r e. (CC X. CC)) /\ q = sup({((1st` s)D(1st` r)), ((2nd` s)D(2nd` r))}, RR, < ))}) Cn J)
47		ipasslem6.f	. . . 4 |- F = {<.w, v>. | (w e. CC /\ v = (((wSA)PB) - (w x. (APB))))}
48		opreq1 3974	. . . . . . . . . 10 |- (u = w -> (uSA) = (wSA))
49	48	opreq1d 3981	. . . . . . . . 9 |- (u = w -> ((uSA)PB) = ((wSA)PB))
50		oprex 3989	. . . . . . . . 9 |- ((wSA)PB) e. V
51	49, 17, 50	fvopab4 3786	. . . . . . . 8 |- (w e. CC -> ({<.u, t>. | (u e. CC /\ t = ((uSA)PB))}` w) = ((wSA)PB))
52		opreq1 3974	. . . . . . . . 9 |- (u = w -> (u x. (APB)) = (w x. (APB)))
53		oprex 3989	. . . . . . . . 9 |- (w x. (APB)) e. V
54	52, 43, 53	fvopab4 3786	. . . . . . . 8 |- (w e. CC -> ({<.u, t>. | (u e. CC /\ t = (u x. (APB)))}` w) = (w x. (APB)))
55	51, 54	opreq12d 3984	. . . . . . 7 |- (w e. CC -> (({<.u, t>. | (u e. CC /\ t = ((uSA)PB))}` w) - ({<.u, t>. | (u e. CC /\ t = (u x. (APB)))}` w)) = (((wSA)PB) - (w x. (APB))))
56	55	eqeq2d 1489	. . . . . 6 |- (w e. CC -> (v = (({<.u, t>. | (u e. CC /\ t = ((uSA)PB))}` w) - ({<.u, t>. | (