Metamath Proof Explorer

Theorem occllem

Description: Lemma for occl . (Contributed by NM, 7-Aug-2000) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses occl.1 ⊢φ→A⊆ℋ
occl.2 ⊢φ→F∈Cauchy
occl.3 ⊢φ→F:ℕ⟶⊥⁡A
occl.4 ⊢φ→B∈A
Assertion occllem ⊢φ→⇝v⁡F⋅ihB=0

Proof

Step Hyp Ref Expression
1 occl.1 ⊢φ→A⊆ℋ
2 occl.2 ⊢φ→F∈Cauchy
3 occl.3 ⊢φ→F:ℕ⟶⊥⁡A
4 occl.4 ⊢φ→B∈A
5 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
6 5 cnfldhaus ⊢TopOpen⁡ℂfld∈Haus
7 6 a1i ⊢φ→TopOpen⁡ℂfld∈Haus
8 ax-hcompl ⊢F∈Cauchy→∃x∈ℋF⇝vx
9 hlimf ⊢⇝v:dom⁡⇝v⟶ℋ
10 ffn ⊢⇝v:dom⁡⇝v⟶ℋ→⇝vFndom⁡⇝v
11 9 10 ax-mp ⊢⇝vFndom⁡⇝v
12 fnbr ⊢⇝vFndom⁡⇝v∧F⇝vx→F∈dom⁡⇝v
13 11 12 mpan ⊢F⇝vx→F∈dom⁡⇝v
14 13 rexlimivw ⊢∃x∈ℋF⇝vx→F∈dom⁡⇝v
15 2 8 14 3syl ⊢φ→F∈dom⁡⇝v
16 ffun ⊢⇝v:dom⁡⇝v⟶ℋ→Fun⁡⇝v
17 funfvbrb ⊢Fun⁡⇝v→F∈dom⁡⇝v↔F⇝v⇝v⁡F
18 9 16 17 mp2b ⊢F∈dom⁡⇝v↔F⇝v⇝v⁡F
19 15 18 sylib ⊢φ→F⇝v⇝v⁡F
20 eqid ⊢+ℎ⋅ℎnormℎ=+ℎ⋅ℎnormℎ
21 eqid ⊢normℎ∘-ℎ=normℎ∘-ℎ
22 20 21 hhims ⊢normℎ∘-ℎ=IndMet⁡+ℎ⋅ℎnormℎ
23 eqid ⊢MetOpen⁡normℎ∘-ℎ=MetOpen⁡normℎ∘-ℎ
24 20 22 23 hhlm ⊢⇝v=⇝t⁡MetOpen⁡normℎ∘-ℎ↾ℋℕ
25 resss ⊢⇝t⁡MetOpen⁡normℎ∘-ℎ↾ℋℕ⊆⇝t⁡MetOpen⁡normℎ∘-ℎ
26 24 25 eqsstri ⊢⇝v⊆⇝t⁡MetOpen⁡normℎ∘-ℎ
27 26 ssbri ⊢F⇝v⇝v⁡F→F⇝t⁡MetOpen⁡normℎ∘-ℎ⇝v⁡F
28 19 27 syl ⊢φ→F⇝t⁡MetOpen⁡normℎ∘-ℎ⇝v⁡F
29 21 hilxmet ⊢normℎ∘-ℎ∈∞Met⁡ℋ
30 23 mopntopon ⊢normℎ∘-ℎ∈∞Met⁡ℋ→MetOpen⁡normℎ∘-ℎ∈TopOn⁡ℋ
31 29 30 mp1i ⊢φ→MetOpen⁡normℎ∘-ℎ∈TopOn⁡ℋ
32 31 cnmptid ⊢φ→x∈ℋ⟼x∈MetOpen⁡normℎ∘-ℎCnMetOpen⁡normℎ∘-ℎ
33 1 4 sseldd ⊢φ→B∈ℋ
34 31 31 33 cnmptc ⊢φ→x∈ℋ⟼B∈MetOpen⁡normℎ∘-ℎCnMetOpen⁡normℎ∘-ℎ
35 20 hhnv ⊢+ℎ⋅ℎnormℎ∈NrmCVec
36 20 hhip ⊢⋅ih=⋅𝑖OLD⁡+ℎ⋅ℎnormℎ
37 36 22 23 5 dipcn ⊢+ℎ⋅ℎnormℎ∈NrmCVec→⋅ih∈MetOpen⁡normℎ∘-ℎ×tMetOpen⁡normℎ∘-ℎCnTopOpen⁡ℂfld
38 35 37 mp1i ⊢φ→⋅ih∈MetOpen⁡normℎ∘-ℎ×tMetOpen⁡normℎ∘-ℎCnTopOpen⁡ℂfld
39 31 32 34 38 cnmpt12f ⊢φ→x∈ℋ⟼x⋅ihB∈MetOpen⁡normℎ∘-ℎCnTopOpen⁡ℂfld
40 28 39 lmcn ⊢φ→x∈ℋ⟼x⋅ihB∘F⇝t⁡TopOpen⁡ℂfldx∈ℋ⟼x⋅ihB⁡⇝v⁡F
41 3 ffvelcdmda ⊢φ∧k∈ℕ→F⁡k∈⊥⁡A
42 ocel ⊢A⊆ℋ→F⁡k∈⊥⁡A↔F⁡k∈ℋ∧∀x∈AF⁡k⋅ihx=0
43 1 42 syl ⊢φ→F⁡k∈⊥⁡A↔F⁡k∈ℋ∧∀x∈AF⁡k⋅ihx=0
44 43 adantr ⊢φ∧k∈ℕ→F⁡k∈⊥⁡A↔F⁡k∈ℋ∧∀x∈AF⁡k⋅ihx=0
45 41 44 mpbid ⊢φ∧k∈ℕ→F⁡k∈ℋ∧∀x∈AF⁡k⋅ihx=0
46 45 simpld ⊢φ∧k∈ℕ→F⁡k∈ℋ
47 oveq1 ⊢x=F⁡k→x⋅ihB=F⁡k⋅ihB
48 eqid ⊢x∈ℋ⟼x⋅ihB=x∈ℋ⟼x⋅ihB
49 ovex ⊢F⁡k⋅ihB∈V
50 47 48 49 fvmpt ⊢F⁡k∈ℋ→x∈ℋ⟼x⋅ihB⁡F⁡k=F⁡k⋅ihB
51 46 50 syl ⊢φ∧k∈ℕ→x∈ℋ⟼x⋅ihB⁡F⁡k=F⁡k⋅ihB
52 oveq2 ⊢x=B→F⁡k⋅ihx=F⁡k⋅ihB
53 52 eqeq1d ⊢x=B→F⁡k⋅ihx=0↔F⁡k⋅ihB=0
54 45 simprd ⊢φ∧k∈ℕ→∀x∈AF⁡k⋅ihx=0
55 4 adantr ⊢φ∧k∈ℕ→B∈A
56 53 54 55 rspcdva ⊢φ∧k∈ℕ→F⁡k⋅ihB=0
57 51 56 eqtrd ⊢φ∧k∈ℕ→x∈ℋ⟼x⋅ihB⁡F⁡k=0
58 ocss ⊢A⊆ℋ→⊥⁡A⊆ℋ
59 1 58 syl ⊢φ→⊥⁡A⊆ℋ
60 3 59 fssd ⊢φ→F:ℕ⟶ℋ
61 fvco3 ⊢F:ℕ⟶ℋ∧k∈ℕ→x∈ℋ⟼x⋅ihB∘F⁡k=x∈ℋ⟼x⋅ihB⁡F⁡k
62 60 61 sylan ⊢φ∧k∈ℕ→x∈ℋ⟼x⋅ihB∘F⁡k=x∈ℋ⟼x⋅ihB⁡F⁡k
63 c0ex ⊢0∈V
64 63 fvconst2 ⊢k∈ℕ→ℕ×0⁡k=0
65 64 adantl ⊢φ∧k∈ℕ→ℕ×0⁡k=0
66 57 62 65 3eqtr4d ⊢φ∧k∈ℕ→x∈ℋ⟼x⋅ihB∘F⁡k=ℕ×0⁡k
67 66 ralrimiva ⊢φ→∀k∈ℕx∈ℋ⟼x⋅ihB∘F⁡k=ℕ×0⁡k
68 ovex ⊢x⋅ihB∈V
69 68 48 fnmpti ⊢x∈ℋ⟼x⋅ihBFnℋ
70 fnfco ⊢x∈ℋ⟼x⋅ihBFnℋ∧F:ℕ⟶ℋ→x∈ℋ⟼x⋅ihB∘FFnℕ
71 69 60 70 sylancr ⊢φ→x∈ℋ⟼x⋅ihB∘FFnℕ
72 63 fconst ⊢ℕ×0:ℕ⟶0
73 ffn ⊢ℕ×0:ℕ⟶0→ℕ×0Fnℕ
74 72 73 ax-mp ⊢ℕ×0Fnℕ
75 eqfnfv ⊢x∈ℋ⟼x⋅ihB∘FFnℕ∧ℕ×0Fnℕ→x∈ℋ⟼x⋅ihB∘F=ℕ×0↔∀k∈ℕx∈ℋ⟼x⋅ihB∘F⁡k=ℕ×0⁡k
76 71 74 75 sylancl ⊢φ→x∈ℋ⟼x⋅ihB∘F=ℕ×0↔∀k∈ℕx∈ℋ⟼x⋅ihB∘F⁡k=ℕ×0⁡k
77 67 76 mpbird ⊢φ→x∈ℋ⟼x⋅ihB∘F=ℕ×0
78 fvex ⊢⇝v⁡F∈V
79 78 hlimveci ⊢F⇝v⇝v⁡F→⇝v⁡F∈ℋ
80 oveq1 ⊢x=⇝v⁡F→x⋅ihB=⇝v⁡F⋅ihB
81 ovex ⊢⇝v⁡F⋅ihB∈V
82 80 48 81 fvmpt ⊢⇝v⁡F∈ℋ→x∈ℋ⟼x⋅ihB⁡⇝v⁡F=⇝v⁡F⋅ihB
83 19 79 82 3syl ⊢φ→x∈ℋ⟼x⋅ihB⁡⇝v⁡F=⇝v⁡F⋅ihB
84 40 77 83 3brtr3d ⊢φ→ℕ×0⇝t⁡TopOpen⁡ℂfld⇝v⁡F⋅ihB
85 5 cnfldtopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ
86 85 a1i ⊢φ→TopOpen⁡ℂfld∈TopOn⁡ℂ
87 0cnd ⊢φ→0∈ℂ
88 1zzd ⊢φ→1∈ℤ
89 nnuz ⊢ℕ=ℤ≥1
90 89 lmconst ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ∧0∈ℂ∧1∈ℤ→ℕ×0⇝t⁡TopOpen⁡ℂfld0
91 86 87 88 90 syl3anc ⊢φ→ℕ×0⇝t⁡TopOpen⁡ℂfld0
92 7 84 91 lmmo ⊢φ→⇝v⁡F⋅ihB=0