Metamath Proof Explorer

Theorem hsn0elch

Description: The zero subspace belongs to the set of closed subspaces of Hilbert space. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hsn0elch ⊢0ℎ∈Cℋ

Proof

Step Hyp Ref Expression
1 ax-hv0cl ⊢0ℎ∈ℋ
2 snssi ⊢0ℎ∈ℋ→0ℎ⊆ℋ
3 1 2 ax-mp ⊢0ℎ⊆ℋ
4 1 elexi ⊢0ℎ∈V
5 4 snid ⊢0ℎ∈0ℎ
6 3 5 pm3.2i ⊢0ℎ⊆ℋ∧0ℎ∈0ℎ
7 velsn ⊢x∈0ℎ↔x=0ℎ
8 velsn ⊢y∈0ℎ↔y=0ℎ
9 oveq12 ⊢x=0ℎ∧y=0ℎ→x+ℎy=0ℎ+ℎ0ℎ
10 1 hvaddlidi ⊢0ℎ+ℎ0ℎ=0ℎ
11 9 10 eqtrdi ⊢x=0ℎ∧y=0ℎ→x+ℎy=0ℎ
12 ovex ⊢x+ℎy∈V
13 12 elsn ⊢x+ℎy∈0ℎ↔x+ℎy=0ℎ
14 11 13 sylibr ⊢x=0ℎ∧y=0ℎ→x+ℎy∈0ℎ
15 7 8 14 syl2anb ⊢x∈0ℎ∧y∈0ℎ→x+ℎy∈0ℎ
16 15 rgen2 ⊢∀x∈0ℎ∀y∈0ℎx+ℎy∈0ℎ
17 oveq2 ⊢y=0ℎ→x⋅ℎy=x⋅ℎ0ℎ
18 hvmul0 ⊢x∈ℂ→x⋅ℎ0ℎ=0ℎ
19 17 18 sylan9eqr ⊢x∈ℂ∧y=0ℎ→x⋅ℎy=0ℎ
20 ovex ⊢x⋅ℎy∈V
21 20 elsn ⊢x⋅ℎy∈0ℎ↔x⋅ℎy=0ℎ
22 19 21 sylibr ⊢x∈ℂ∧y=0ℎ→x⋅ℎy∈0ℎ
23 8 22 sylan2b ⊢x∈ℂ∧y∈0ℎ→x⋅ℎy∈0ℎ
24 23 rgen2 ⊢∀x∈ℂ∀y∈0ℎx⋅ℎy∈0ℎ
25 16 24 pm3.2i ⊢∀x∈0ℎ∀y∈0ℎx+ℎy∈0ℎ∧∀x∈ℂ∀y∈0ℎx⋅ℎy∈0ℎ
26 issh2 ⊢0ℎ∈Sℋ↔0ℎ⊆ℋ∧0ℎ∈0ℎ∧∀x∈0ℎ∀y∈0ℎx+ℎy∈0ℎ∧∀x∈ℂ∀y∈0ℎx⋅ℎy∈0ℎ
27 6 25 26 mpbir2an ⊢0ℎ∈Sℋ
28 4 fconst2 ⊢f:ℕ⟶0ℎ↔f=ℕ×0ℎ
29 hlim0 ⊢ℕ×0ℎ⇝v0ℎ
30 breq1 ⊢f=ℕ×0ℎ→f⇝v0ℎ↔ℕ×0ℎ⇝v0ℎ
31 29 30 mpbiri ⊢f=ℕ×0ℎ→f⇝v0ℎ
32 28 31 sylbi ⊢f:ℕ⟶0ℎ→f⇝v0ℎ
33 hlimuni ⊢f⇝v0ℎ∧f⇝vx→0ℎ=x
34 33 eleq1d ⊢f⇝v0ℎ∧f⇝vx→0ℎ∈0ℎ↔x∈0ℎ
35 32 34 sylan ⊢f:ℕ⟶0ℎ∧f⇝vx→0ℎ∈0ℎ↔x∈0ℎ
36 5 35 mpbii ⊢f:ℕ⟶0ℎ∧f⇝vx→x∈0ℎ
37 36 gen2 ⊢∀f∀xf:ℕ⟶0ℎ∧f⇝vx→x∈0ℎ
38 isch2 ⊢0ℎ∈Cℋ↔0ℎ∈Sℋ∧∀f∀xf:ℕ⟶0ℎ∧f⇝vx→x∈0ℎ
39 27 37 38 mpbir2an ⊢0ℎ∈Cℋ