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 = ( BaseSet ` U )
ip1i.2 
|- G = ( +v ` U )
ip1i.4 
|- S = ( .sOLD ` U )
ip1i.7 
|- P = ( .iOLD ` U )
ip1i.9 
|- U e. CPreHilOLD
ipasslem7.a 
|- A e. X
ipasslem7.b 
|- B e. X
ipasslem7.f 
|- F = ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) )
ipasslem7.j 
|- J = ( topGen ` ran (,) )
ipasslem7.k 
|- K = ( TopOpen ` CCfld )
Assertion ipasslem7 
|- F e. ( J Cn K )

Proof

Step Hyp Ref Expression
1 ip1i.1 
 |-  X = ( BaseSet ` U )
2 ip1i.2 
 |-  G = ( +v ` U )
3 ip1i.4 
 |-  S = ( .sOLD ` U )
4 ip1i.7 
 |-  P = ( .iOLD ` U )
5 ip1i.9 
 |-  U e. CPreHilOLD
6 ipasslem7.a 
 |-  A e. X
7 ipasslem7.b 
 |-  B e. X
8 ipasslem7.f 
 |-  F = ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) )
9 ipasslem7.j 
 |-  J = ( topGen ` ran (,) )
10 ipasslem7.k 
 |-  K = ( TopOpen ` CCfld )
11 10 tgioo2 
 |-  ( topGen ` ran (,) ) = ( K |`t RR )
12 9 11 eqtri 
 |-  J = ( K |`t RR )
13 10 cnfldtopon 
 |-  K e. ( TopOn ` CC )
14 13 a1i 
 |-  ( T. -> K e. ( TopOn ` CC ) )
15 ax-resscn 
 |-  RR C_ CC
16 15 a1i 
 |-  ( T. -> RR C_ CC )
17 14 cnmptid 
 |-  ( T. -> ( w e. CC |-> w ) e. ( K Cn K ) )
18 5 phnvi 
 |-  U e. NrmCVec
19 eqid 
 |-  ( IndMet ` U ) = ( IndMet ` U )
20 1 19 imsxmet 
 |-  ( U e. NrmCVec -> ( IndMet ` U ) e. ( *Met ` X ) )
21 18 20 ax-mp 
 |-  ( IndMet ` U ) e. ( *Met ` X )
22 eqid 
 |-  ( MetOpen ` ( IndMet ` U ) ) = ( MetOpen ` ( IndMet ` U ) )
23 22 mopntopon 
 |-  ( ( IndMet ` U ) e. ( *Met ` X ) -> ( MetOpen ` ( IndMet ` U ) ) e. ( TopOn ` X ) )
24 21 23 mp1i 
 |-  ( T. -> ( MetOpen ` ( IndMet ` U ) ) e. ( TopOn ` X ) )
25 6 a1i 
 |-  ( T. -> A e. X )
26 14 24 25 cnmptc 
 |-  ( T. -> ( w e. CC |-> A ) e. ( K Cn ( MetOpen ` ( IndMet ` U ) ) ) )
27 19 22 3 10 smcn 
 |-  ( U e. NrmCVec -> S e. ( ( K tX ( MetOpen ` ( IndMet ` U ) ) ) Cn ( MetOpen ` ( IndMet ` U ) ) ) )
28 18 27 mp1i 
 |-  ( T. -> S e. ( ( K tX ( MetOpen ` ( IndMet ` U ) ) ) Cn ( MetOpen ` ( IndMet ` U ) ) ) )
29 14 17 26 28 cnmpt12f 
 |-  ( T. -> ( w e. CC |-> ( w S A ) ) e. ( K Cn ( MetOpen ` ( IndMet ` U ) ) ) )
30 7 a1i 
 |-  ( T. -> B e. X )
31 14 24 30 cnmptc 
 |-  ( T. -> ( w e. CC |-> B ) e. ( K Cn ( MetOpen ` ( IndMet ` U ) ) ) )
32 4 19 22 10 dipcn 
 |-  ( U e. NrmCVec -> P e. ( ( ( MetOpen ` ( IndMet ` U ) ) tX ( MetOpen ` ( IndMet ` U ) ) ) Cn K ) )
33 18 32 mp1i 
 |-  ( T. -> P e. ( ( ( MetOpen ` ( IndMet ` U ) ) tX ( MetOpen ` ( IndMet ` U ) ) ) Cn K ) )
34 14 29 31 33 cnmpt12f 
 |-  ( T. -> ( w e. CC |-> ( ( w S A ) P B ) ) e. ( K Cn K ) )
35 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
36 18 6 7 35 mp3an 
 |-  ( A P B ) e. CC
37 36 a1i 
 |-  ( T. -> ( A P B ) e. CC )
38 14 14 37 cnmptc 
 |-  ( T. -> ( w e. CC |-> ( A P B ) ) e. ( K Cn K ) )
39 10 mulcn 
 |-  x. e. ( ( K tX K ) Cn K )
40 39 a1i 
 |-  ( T. -> x. e. ( ( K tX K ) Cn K ) )
41 14 17 38 40 cnmpt12f 
 |-  ( T. -> ( w e. CC |-> ( w x. ( A P B ) ) ) e. ( K Cn K ) )
42 10 subcn 
 |-  - e. ( ( K tX K ) Cn K )
43 42 a1i 
 |-  ( T. -> - e. ( ( K tX K ) Cn K ) )
44 14 34 41 43 cnmpt12f 
 |-  ( T. -> ( w e. CC |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) ) e. ( K Cn K ) )
45 12 14 16 44 cnmpt1res 
 |-  ( T. -> ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) ) e. ( J Cn K ) )
46 45 mptru 
 |-  ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) ) e. ( J Cn K )
47 8 46 eqeltri 
 |-  F e. ( J Cn K )