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=BaseSetU
ip1i.2 G=+vU
ip1i.4 S=𝑠OLDU
ip1i.7 P=𝑖OLDU
ip1i.9 UCPreHilOLD
ipasslem7.a AX
ipasslem7.b BX
ipasslem7.f F=wwSAPBwAPB
ipasslem7.j J=topGenran.
ipasslem7.k K=TopOpenfld
Assertion ipasslem7 FJCnK

Proof

Step Hyp Ref Expression
1 ip1i.1 X=BaseSetU
2 ip1i.2 G=+vU
3 ip1i.4 S=𝑠OLDU
4 ip1i.7 P=𝑖OLDU
5 ip1i.9 UCPreHilOLD
6 ipasslem7.a AX
7 ipasslem7.b BX
8 ipasslem7.f F=wwSAPBwAPB
9 ipasslem7.j J=topGenran.
10 ipasslem7.k K=TopOpenfld
11 10 tgioo2 topGenran.=K𝑡
12 9 11 eqtri J=K𝑡
13 10 cnfldtopon KTopOn
14 13 a1i KTopOn
15 ax-resscn
16 15 a1i
17 14 cnmptid wwKCnK
18 5 phnvi UNrmCVec
19 eqid IndMetU=IndMetU
20 1 19 imsxmet UNrmCVecIndMetU∞MetX
21 18 20 ax-mp IndMetU∞MetX
22 eqid MetOpenIndMetU=MetOpenIndMetU
23 22 mopntopon IndMetU∞MetXMetOpenIndMetUTopOnX
24 21 23 mp1i MetOpenIndMetUTopOnX
25 6 a1i AX
26 14 24 25 cnmptc wAKCnMetOpenIndMetU
27 19 22 3 10 smcn UNrmCVecSK×tMetOpenIndMetUCnMetOpenIndMetU
28 18 27 mp1i SK×tMetOpenIndMetUCnMetOpenIndMetU
29 14 17 26 28 cnmpt12f wwSAKCnMetOpenIndMetU
30 7 a1i BX
31 14 24 30 cnmptc wBKCnMetOpenIndMetU
32 4 19 22 10 dipcn UNrmCVecPMetOpenIndMetU×tMetOpenIndMetUCnK
33 18 32 mp1i PMetOpenIndMetU×tMetOpenIndMetUCnK
34 14 29 31 33 cnmpt12f wwSAPBKCnK
35 1 4 dipcl UNrmCVecAXBXAPB
36 18 6 7 35 mp3an APB
37 36 a1i APB
38 14 14 37 cnmptc wAPBKCnK
39 10 mulcn ×K×tKCnK
40 39 a1i ×K×tKCnK
41 14 17 38 40 cnmpt12f wwAPBKCnK
42 10 subcn K×tKCnK
43 42 a1i K×tKCnK
44 14 34 41 43 cnmpt12f wwSAPBwAPBKCnK
45 12 14 16 44 cnmpt1res wwSAPBwAPBJCnK
46 45 mptru wwSAPBwAPBJCnK
47 8 46 eqeltri FJCnK