Metamath Proof Explorer

Theorem shatomici

Description: The lattice of Hilbert subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. Part of proof of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 24-Nov-2004) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	shatomic.1	$⊢ A \in S_{ℋ}$
	Assertion	shatomici	$⊢ A \neq 0_{ℋ} \to \exists x \in HAtoms x \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		shatomic.1	$⊢ A \in S_{ℋ}$
2	1	shne0i	$⊢ A \neq 0_{ℋ} \leftrightarrow \exists y \in A y \neq 0_{ℎ}$
3	1	sheli	$⊢ y \in A \to y \in ℋ$
4		h1da	$⊢ (y \in ℋ \land y \neq 0_{ℎ}) \to ⊥ (⊥ (\{y\})) \in HAtoms$
5	3 4	sylan	$⊢ (y \in A \land y \neq 0_{ℎ}) \to ⊥ (⊥ (\{y\})) \in HAtoms$
6		sh1dle	$⊢ (A \in S_{ℋ} \land y \in A) \to ⊥ (⊥ (\{y\})) \subseteq A$
7	1 6	mpan	$⊢ y \in A \to ⊥ (⊥ (\{y\})) \subseteq A$
8	7	adantr	$⊢ (y \in A \land y \neq 0_{ℎ}) \to ⊥ (⊥ (\{y\})) \subseteq A$
9		sseq1	$⊢ x = ⊥ (⊥ (\{y\})) \to (x \subseteq A \leftrightarrow ⊥ (⊥ (\{y\})) \subseteq A)$
10	9	rspcev	$⊢ (⊥ (⊥ (\{y\})) \in HAtoms \land ⊥ (⊥ (\{y\})) \subseteq A) \to \exists x \in HAtoms x \subseteq A$
11	5 8 10	syl2anc	$⊢ (y \in A \land y \neq 0_{ℎ}) \to \exists x \in HAtoms x \subseteq A$
12	11	rexlimiva	$⊢ \exists y \in A y \neq 0_{ℎ} \to \exists x \in HAtoms x \subseteq A$
13	2 12	sylbi	$⊢ A \neq 0_{ℋ} \to \exists x \in HAtoms x \subseteq A$