Metamath Proof Explorer

Theorem ipasslem8

Description: Lemma for ipassi . By ipasslem5 , F is 0 for all QQ ; since it is continuous and QQ is dense in RR by qdensere2 , we conclude F is 0 for all RR . (Contributed by NM, 24-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 ) ) ) )
Assertion ipasslem8 
|- F : RR --> { 0 }

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 0cn 
 |-  0 e. CC
10 qre 
 |-  ( x e. QQ -> x e. RR )
11 oveq1 
 |-  ( w = x -> ( w S A ) = ( x S A ) )
12 11 oveq1d 
 |-  ( w = x -> ( ( w S A ) P B ) = ( ( x S A ) P B ) )
13 oveq1 
 |-  ( w = x -> ( w x. ( A P B ) ) = ( x x. ( A P B ) ) )
14 12 13 oveq12d 
 |-  ( w = x -> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) = ( ( ( x S A ) P B ) - ( x x. ( A P B ) ) ) )
15 ovex 
 |-  ( ( ( x S A ) P B ) - ( x x. ( A P B ) ) ) e. _V
16 14 8 15 fvmpt 
 |-  ( x e. RR -> ( F ` x ) = ( ( ( x S A ) P B ) - ( x x. ( A P B ) ) ) )
17 10 16 syl 
 |-  ( x e. QQ -> ( F ` x ) = ( ( ( x S A ) P B ) - ( x x. ( A P B ) ) ) )
18 qcn 
 |-  ( x e. QQ -> x e. CC )
19 5 phnvi 
 |-  U e. NrmCVec
20 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ x e. CC /\ A e. X ) -> ( x S A ) e. X )
21 19 20 mp3an1 
 |-  ( ( x e. CC /\ A e. X ) -> ( x S A ) e. X )
22 18 21 sylan 
 |-  ( ( x e. QQ /\ A e. X ) -> ( x S A ) e. X )
23 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ ( x S A ) e. X /\ B e. X ) -> ( ( x S A ) P B ) e. CC )
24 19 7 23 mp3an13 
 |-  ( ( x S A ) e. X -> ( ( x S A ) P B ) e. CC )
25 22 24 syl 
 |-  ( ( x e. QQ /\ A e. X ) -> ( ( x S A ) P B ) e. CC )
26 1 2 3 4 5 7 ipasslem5 
 |-  ( ( x e. QQ /\ A e. X ) -> ( ( x S A ) P B ) = ( x x. ( A P B ) ) )
27 25 26 subeq0bd 
 |-  ( ( x e. QQ /\ A e. X ) -> ( ( ( x S A ) P B ) - ( x x. ( A P B ) ) ) = 0 )
28 6 27 mpan2 
 |-  ( x e. QQ -> ( ( ( x S A ) P B ) - ( x x. ( A P B ) ) ) = 0 )
29 17 28 eqtrd 
 |-  ( x e. QQ -> ( F ` x ) = 0 )
30 29 rgen 
 |-  A. x e. QQ ( F ` x ) = 0
31 8 funmpt2 
 |-  Fun F
32 qssre 
 |-  QQ C_ RR
33 ovex 
 |-  ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) e. _V
34 33 8 dmmpti 
 |-  dom F = RR
35 32 34 sseqtrri 
 |-  QQ C_ dom F
36 funconstss 
 |-  ( ( Fun F /\ QQ C_ dom F ) -> ( A. x e. QQ ( F ` x ) = 0 <-> QQ C_ ( `' F " { 0 } ) ) )
37 31 35 36 mp2an 
 |-  ( A. x e. QQ ( F ` x ) = 0 <-> QQ C_ ( `' F " { 0 } ) )
38 30 37 mpbi 
 |-  QQ C_ ( `' F " { 0 } )
39 qdensere 
 |-  ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR
40 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
41 40 cnfldhaus 
 |-  ( TopOpen ` CCfld ) e. Haus
42 haust1 
 |-  ( ( TopOpen ` CCfld ) e. Haus -> ( TopOpen ` CCfld ) e. Fre )
43 41 42 ax-mp 
 |-  ( TopOpen ` CCfld ) e. Fre
44 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
45 1 2 3 4 5 6 7 8 44 40 ipasslem7 
 |-  F e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) )
46 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
47 40 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
48 47 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
49 46 48 dnsconst 
 |-  ( ( ( ( TopOpen ` CCfld ) e. Fre /\ F e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) ) /\ ( 0 e. CC /\ QQ C_ ( `' F " { 0 } ) /\ ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR ) ) -> F : RR --> { 0 } )
50 43 45 49 mpanl12 
 |-  ( ( 0 e. CC /\ QQ C_ ( `' F " { 0 } ) /\ ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR ) -> F : RR --> { 0 } )
51 9 38 39 50 mp3an 
 |-  F : RR --> { 0 }