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ℋ