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 ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) ∈ ℋ )
5 4 rgen2 ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 +ℎ 𝑦 ) ∈ ℋ
6 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
7 6 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ
8 5 7 pm3.2i ⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
9 issh2 ⊢ ( ℋ ∈ Sℋ ↔ ( ( ℋ ⊆ ℋ ∧ 0ℎ ∈ ℋ ) ∧ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ) ) )
10 3 8 9 mpbir2an ⊢ ℋ ∈ Sℋ
11 vex ⊢ 𝑥 ∈ V
12 11 hlimveci ⊢ ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ ℋ )
13 12 adantl ⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ℋ )
14 13 gen2 ⊢ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ℋ )
15 isch2 ⊢ ( ℋ ∈ Cℋ ↔ ( ℋ ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ℋ ) ) )
16 10 14 15 mpbir2an ⊢ ℋ ∈ Cℋ