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