Metamath Proof Explorer


Theorem hlimadd

Description: Limit of the sum of two sequences in a Hilbert vector space. (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hlimadd.3 ( 𝜑𝐹 : ℕ ⟶ ℋ )
hlimadd.4 ( 𝜑𝐺 : ℕ ⟶ ℋ )
hlimadd.5 ( 𝜑𝐹𝑣 𝐴 )
hlimadd.6 ( 𝜑𝐺𝑣 𝐵 )
hlimadd.7 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐹𝑛 ) + ( 𝐺𝑛 ) ) )
Assertion hlimadd ( 𝜑𝐻𝑣 ( 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 hlimadd.3 ( 𝜑𝐹 : ℕ ⟶ ℋ )
2 hlimadd.4 ( 𝜑𝐺 : ℕ ⟶ ℋ )
3 hlimadd.5 ( 𝜑𝐹𝑣 𝐴 )
4 hlimadd.6 ( 𝜑𝐺𝑣 𝐵 )
5 hlimadd.7 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐹𝑛 ) + ( 𝐺𝑛 ) ) )
6 1 ffvelrnda ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ∈ ℋ )
7 2 ffvelrnda ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐺𝑛 ) ∈ ℋ )
8 hvaddcl ( ( ( 𝐹𝑛 ) ∈ ℋ ∧ ( 𝐺𝑛 ) ∈ ℋ ) → ( ( 𝐹𝑛 ) + ( 𝐺𝑛 ) ) ∈ ℋ )
9 6 7 8 syl2anc ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝐹𝑛 ) + ( 𝐺𝑛 ) ) ∈ ℋ )
10 9 5 fmptd ( 𝜑𝐻 : ℕ ⟶ ℋ )
11 ax-hilex ℋ ∈ V
12 nnex ℕ ∈ V
13 11 12 elmap ( 𝐻 ∈ ( ℋ ↑m ℕ ) ↔ 𝐻 : ℕ ⟶ ℋ )
14 10 13 sylibr ( 𝜑𝐻 ∈ ( ℋ ↑m ℕ ) )
15 nnuz ℕ = ( ℤ ‘ 1 )
16 1zzd ( 𝜑 → 1 ∈ ℤ )
17 eqid ⟨ ⟨ + , · ⟩ , norm ⟩ = ⟨ ⟨ + , · ⟩ , norm
18 eqid ( norm ∘ − ) = ( norm ∘ − )
19 17 18 hhims ( norm ∘ − ) = ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
20 17 19 hhxmet ( norm ∘ − ) ∈ ( ∞Met ‘ ℋ )
21 eqid ( MetOpen ‘ ( norm ∘ − ) ) = ( MetOpen ‘ ( norm ∘ − ) )
22 21 mopntopon ( ( norm ∘ − ) ∈ ( ∞Met ‘ ℋ ) → ( MetOpen ‘ ( norm ∘ − ) ) ∈ ( TopOn ‘ ℋ ) )
23 20 22 mp1i ( 𝜑 → ( MetOpen ‘ ( norm ∘ − ) ) ∈ ( TopOn ‘ ℋ ) )
24 17 hhnv ⟨ ⟨ + , · ⟩ , norm ⟩ ∈ NrmCVec
25 df-hba ℋ = ( BaseSet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
26 17 24 25 19 21 h2hlm 𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ↾ ( ℋ ↑m ℕ ) )
27 resss ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ↾ ( ℋ ↑m ℕ ) ) ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) )
28 26 27 eqsstri 𝑣 ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) )
29 28 ssbri ( 𝐹𝑣 𝐴𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) 𝐴 )
30 3 29 syl ( 𝜑𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) 𝐴 )
31 28 ssbri ( 𝐺𝑣 𝐵𝐺 ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) 𝐵 )
32 4 31 syl ( 𝜑𝐺 ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) 𝐵 )
33 17 hhva + = ( +𝑣 ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
34 19 21 33 vacn ( ⟨ ⟨ + , · ⟩ , norm ⟩ ∈ NrmCVec → + ∈ ( ( ( MetOpen ‘ ( norm ∘ − ) ) ×t ( MetOpen ‘ ( norm ∘ − ) ) ) Cn ( MetOpen ‘ ( norm ∘ − ) ) ) )
35 24 34 mp1i ( 𝜑 → + ∈ ( ( ( MetOpen ‘ ( norm ∘ − ) ) ×t ( MetOpen ‘ ( norm ∘ − ) ) ) Cn ( MetOpen ‘ ( norm ∘ − ) ) ) )
36 15 16 23 23 1 2 30 32 35 5 lmcn2 ( 𝜑𝐻 ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ( 𝐴 + 𝐵 ) )
37 26 breqi ( 𝐻𝑣 ( 𝐴 + 𝐵 ) ↔ 𝐻 ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ↾ ( ℋ ↑m ℕ ) ) ( 𝐴 + 𝐵 ) )
38 ovex ( 𝐴 + 𝐵 ) ∈ V
39 38 brresi ( 𝐻 ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ↾ ( ℋ ↑m ℕ ) ) ( 𝐴 + 𝐵 ) ↔ ( 𝐻 ∈ ( ℋ ↑m ℕ ) ∧ 𝐻 ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ( 𝐴 + 𝐵 ) ) )
40 37 39 bitri ( 𝐻𝑣 ( 𝐴 + 𝐵 ) ↔ ( 𝐻 ∈ ( ℋ ↑m ℕ ) ∧ 𝐻 ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ( 𝐴 + 𝐵 ) ) )
41 14 36 40 sylanbrc ( 𝜑𝐻𝑣 ( 𝐴 + 𝐵 ) )