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	$⊢ ℋ \in C_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		ssid	$⊢ ℋ \subseteq ℋ$
2		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
3	1 2	pm3.2i	$⊢ (ℋ \subseteq ℋ \land 0_{ℎ} \in ℋ)$
4		hvaddcl	$⊢ (x \in ℋ \land y \in ℋ) \to x +_{ℎ} y \in ℋ$
5	4	rgen2	$⊢ \forall x \in ℋ \forall y \in ℋ x +_{ℎ} y \in ℋ$
6		hvmulcl	$⊢ (x \in ℂ \land y \in ℋ) \to x \cdot_{ℎ} y \in ℋ$
7	6	rgen2	$⊢ \forall x \in ℂ \forall y \in ℋ x \cdot_{ℎ} y \in ℋ$
8	5 7	pm3.2i	$⊢ (\forall x \in ℋ \forall y \in ℋ x +_{ℎ} y \in ℋ \land \forall x \in ℂ \forall y \in ℋ x \cdot_{ℎ} y \in ℋ)$
9		issh2	$⊢ ℋ \in S_{ℋ} \leftrightarrow ((ℋ \subseteq ℋ \land 0_{ℎ} \in ℋ) \land (\forall x \in ℋ \forall y \in ℋ x +_{ℎ} y \in ℋ \land \forall x \in ℂ \forall y \in ℋ x \cdot_{ℎ} y \in ℋ))$
10	3 8 9	mpbir2an	$⊢ ℋ \in S_{ℋ}$
11		vex	$⊢ x \in V$
12	11	hlimveci	$⊢ f \underset{v}{⇝} x \to x \in ℋ$
13	12	adantl	$⊢ (f : ℕ ⟶ ℋ \land f \underset{v}{⇝} x) \to x \in ℋ$
14	13	gen2	$⊢ \forall f \forall x ((f : ℕ ⟶ ℋ \land f \underset{v}{⇝} x) \to x \in ℋ)$
15		isch2	$⊢ ℋ \in C_{ℋ} \leftrightarrow (ℋ \in S_{ℋ} \land \forall f \forall x ((f : ℕ ⟶ ℋ \land f \underset{v}{⇝} x) \to x \in ℋ))$
16	10 14 15	mpbir2an	$⊢ ℋ \in C_{ℋ}$