This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑥 ∈ { 0ℎ } ↔ 𝑥 = 0ℎ )
8 velsn ⊢ ( 𝑦 ∈ { 0ℎ } ↔ 𝑦 = 0ℎ )
9 oveq12 ⊢ ( ( 𝑥 = 0ℎ ∧ 𝑦 = 0ℎ ) → ( 𝑥 +ℎ 𝑦 ) = ( 0ℎ +ℎ 0ℎ ) )
10 1 hvaddlidi ⊢ ( 0ℎ +ℎ 0ℎ ) = 0ℎ
11 9 10 eqtrdi ⊢ ( ( 𝑥 = 0ℎ ∧ 𝑦 = 0ℎ ) → ( 𝑥 +ℎ 𝑦 ) = 0ℎ )
12 ovex ⊢ ( 𝑥 +ℎ 𝑦 ) ∈ V
13 12 elsn ⊢ ( ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } ↔ ( 𝑥 +ℎ 𝑦 ) = 0ℎ )
14 11 13 sylibr ⊢ ( ( 𝑥 = 0ℎ ∧ 𝑦 = 0ℎ ) → ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } )
15 7 8 14 syl2anb ⊢ ( ( 𝑥 ∈ { 0ℎ } ∧ 𝑦 ∈ { 0ℎ } ) → ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } )
16 15 rgen2 ⊢ ∀ 𝑥 ∈ { 0ℎ } ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ }
17 oveq2 ⊢ ( 𝑦 = 0ℎ → ( 𝑥 ·ℎ 𝑦 ) = ( 𝑥 ·ℎ 0ℎ ) )
18 hvmul0 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ·ℎ 0ℎ ) = 0ℎ )
19 17 18 sylan9eqr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 = 0ℎ ) → ( 𝑥 ·ℎ 𝑦 ) = 0ℎ )
20 ovex ⊢ ( 𝑥 ·ℎ 𝑦 ) ∈ V
21 20 elsn ⊢ ( ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } ↔ ( 𝑥 ·ℎ 𝑦 ) = 0ℎ )
22 19 21 sylibr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 = 0ℎ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } )
23 8 22 sylan2b ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ { 0ℎ } ) → ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } )
24 23 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ }
25 16 24 pm3.2i ⊢ ( ∀ 𝑥 ∈ { 0ℎ } ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } )
26 issh2 ⊢ ( { 0ℎ } ∈ Sℋ ↔ ( ( { 0ℎ } ⊆ ℋ ∧ 0ℎ ∈ { 0ℎ } ) ∧ ( ∀ 𝑥 ∈ { 0ℎ } ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } ) ) )
27 6 25 26 mpbir2an ⊢ { 0ℎ } ∈ Sℋ
28 4 fconst2 ⊢ ( 𝑓 : ℕ ⟶ { 0ℎ } ↔ 𝑓 = ( ℕ × { 0ℎ } ) )
29 hlim0 ⊢ ( ℕ × { 0ℎ } ) ⇝𝑣 0ℎ
30 breq1 ⊢ ( 𝑓 = ( ℕ × { 0ℎ } ) → ( 𝑓 ⇝𝑣 0ℎ ↔ ( ℕ × { 0ℎ } ) ⇝𝑣 0ℎ ) )
31 29 30 mpbiri ⊢ ( 𝑓 = ( ℕ × { 0ℎ } ) → 𝑓 ⇝𝑣 0ℎ )
32 28 31 sylbi ⊢ ( 𝑓 : ℕ ⟶ { 0ℎ } → 𝑓 ⇝𝑣 0ℎ )
33 hlimuni ⊢ ( ( 𝑓 ⇝𝑣 0ℎ ∧ 𝑓 ⇝𝑣 𝑥 ) → 0ℎ = 𝑥 )
34 33 eleq1d ⊢ ( ( 𝑓 ⇝𝑣 0ℎ ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 0ℎ ∈ { 0ℎ } ↔ 𝑥 ∈ { 0ℎ } ) )
35 32 34 sylan ⊢ ( ( 𝑓 : ℕ ⟶ { 0ℎ } ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 0ℎ ∈ { 0ℎ } ↔ 𝑥 ∈ { 0ℎ } ) )
36 5 35 mpbii ⊢ ( ( 𝑓 : ℕ ⟶ { 0ℎ } ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ { 0ℎ } )
37 36 gen2 ⊢ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ { 0ℎ } ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ { 0ℎ } )
38 isch2 ⊢ ( { 0ℎ } ∈ Cℋ ↔ ( { 0ℎ } ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ { 0ℎ } ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ { 0ℎ } ) ) )
39 27 37 38 mpbir2an ⊢ { 0ℎ } ∈ Cℋ