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 ⊢ ( 𝜑 → 𝐻 ⇝𝑣 ( 𝐴 +ℎ 𝐵 ) )