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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
ipasslem7.a ⊢ 𝐴 ∈ 𝑋
ipasslem7.b ⊢ 𝐵 ∈ 𝑋
ipasslem7.f ⊢ 𝐹 = ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) )
Assertion ipasslem8 𝐹 : ℝ ⟶ { 0 }

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
5 ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
6 ipasslem7.a ⊢ 𝐴 ∈ 𝑋
7 ipasslem7.b ⊢ 𝐵 ∈ 𝑋
8 ipasslem7.f ⊢ 𝐹 = ( 𝑤 ∈ ℝ ↦ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) )
9 0cn ⊢ 0 ∈ ℂ
10 qre ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ )
11 oveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝑆 𝐴 ) = ( 𝑥 𝑆 𝐴 ) )
12 11 oveq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) )
13 oveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) )
14 12 13 oveq12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) ) )
15 ovex ⊢ ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) ) ∈ V
16 14 8 15 fvmpt ⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) ) )
17 10 16 syl ⊢ ( 𝑥 ∈ ℚ → ( 𝐹 ‘ 𝑥 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) ) )
18 qcn ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℂ )
19 5 phnvi ⊢ 𝑈 ∈ NrmCVec
20 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 )
21 19 20 mp3an1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 )
22 18 21 sylan ⊢ ( ( 𝑥 ∈ ℚ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 )
23 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
24 19 7 23 mp3an13 ⊢ ( ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 → ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
25 22 24 syl ⊢ ( ( 𝑥 ∈ ℚ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
26 1 2 3 4 5 7 ipasslem5 ⊢ ( ( 𝑥 ∈ ℚ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) )
27 25 26 subeq0bd ⊢ ( ( 𝑥 ∈ ℚ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) ) = 0 )
28 6 27 mpan2 ⊢ ( 𝑥 ∈ ℚ → ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) ) = 0 )
29 17 28 eqtrd ⊢ ( 𝑥 ∈ ℚ → ( 𝐹 ‘ 𝑥 ) = 0 )
30 29 rgen ⊢ ∀ 𝑥 ∈ ℚ ( 𝐹 ‘ 𝑥 ) = 0
31 8 funmpt2 ⊢ Fun 𝐹
32 qssre ⊢ ℚ ⊆ ℝ
33 ovex ⊢ ( ( ( 𝑤 𝑆 𝐴 ) 𝑃 𝐵 ) − ( 𝑤 · ( 𝐴 𝑃 𝐵 ) ) ) ∈ V
34 33 8 dmmpti ⊢ dom 𝐹 = ℝ
35 32 34 sseqtrri ⊢ ℚ ⊆ dom 𝐹
36 funconstss ⊢ ( ( Fun 𝐹 ∧ ℚ ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ ℚ ( 𝐹 ‘ 𝑥 ) = 0 ↔ ℚ ⊆ ( ◡ 𝐹 “ { 0 } ) ) )
37 31 35 36 mp2an ⊢ ( ∀ 𝑥 ∈ ℚ ( 𝐹 ‘ 𝑥 ) = 0 ↔ ℚ ⊆ ( ◡ 𝐹 “ { 0 } ) )
38 30 37 mpbi ⊢ ℚ ⊆ ( ◡ 𝐹 “ { 0 } )
39 qdensere ⊢ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ℝ
40 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
41 40 cnfldhaus ⊢ ( TopOpen ‘ ℂfld ) ∈ Haus
42 haust1 ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Haus → ( TopOpen ‘ ℂfld ) ∈ Fre )
43 41 42 ax-mp ⊢ ( TopOpen ‘ ℂfld ) ∈ Fre
44 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
45 1 2 3 4 5 6 7 8 44 40 ipasslem7 ⊢ 𝐹 ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) )
46 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
47 40 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
48 47 toponunii ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
49 46 48 dnsconst ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ∈ Fre ∧ 𝐹 ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) ) ∧ ( 0 ∈ ℂ ∧ ℚ ⊆ ( ◡ 𝐹 “ { 0 } ) ∧ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ℝ ) ) → 𝐹 : ℝ ⟶ { 0 } )
50 43 45 49 mpanl12 ⊢ ( ( 0 ∈ ℂ ∧ ℚ ⊆ ( ◡ 𝐹 “ { 0 } ) ∧ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ℝ ) → 𝐹 : ℝ ⟶ { 0 } )
51 9 38 39 50 mp3an ⊢ 𝐹 : ℝ ⟶ { 0 }