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

Metamath Proof Explorer

Theorem helch

Description: The Hilbert lattice one (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of Kalmbach p. 65. (Contributed by NM, 6-Sep-1999) (New usage is discouraged.)

Ref Expression
Assertion helch ⊢ ℋ ∈ C ℋ

Proof

Step Hyp Ref Expression
1 ssid ⊢ ℋ ⊆ ℋ
2 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
3 1 2 pm3.2i ⊢ ℋ ⊆ ℋ ∧ 0 ℎ ∈ ℋ
4 hvaddcl ⊢ x ∈ ℋ ∧ y ∈ ℋ → x + ℎ y ∈ ℋ
5 4 rgen2 ⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ x + ℎ y ∈ ℋ
6 hvmulcl ⊢ x ∈ ℂ ∧ y ∈ ℋ → x ⋅ ℎ y ∈ ℋ
7 6 rgen2 ⊢ ∀ x ∈ ℂ ∀ y ∈ ℋ x ⋅ ℎ y ∈ ℋ
8 5 7 pm3.2i ⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ x + ℎ y ∈ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ x ⋅ ℎ y ∈ ℋ
9 issh2 ⊢ ℋ ∈ S ℋ ↔ ℋ ⊆ ℋ ∧ 0 ℎ ∈ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x + ℎ y ∈ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ x ⋅ ℎ y ∈ ℋ
10 3 8 9 mpbir2an ⊢ ℋ ∈ S ℋ
11 vex ⊢ x ∈ V
12 11 hlimveci ⊢ f ⇝v x → x ∈ ℋ
13 12 adantl ⊢ f : ℕ ⟶ ℋ ∧ f ⇝v x → x ∈ ℋ
14 13 gen2 ⊢ ∀ f ∀ x f : ℕ ⟶ ℋ ∧ f ⇝v x → x ∈ ℋ
15 isch2 ⊢ ℋ ∈ C ℋ ↔ ℋ ∈ S ℋ ∧ ∀ f ∀ x f : ℕ ⟶ ℋ ∧ f ⇝v x → x ∈ ℋ
16 10 14 15 mpbir2an ⊢ ℋ ∈ C ℋ