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	⊢ 𝐴 ∈ Sℋ
Assertion	shatomici	⊢ ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		shatomic.1	⊢ 𝐴 ∈ Sℋ
2	1	shne0i	⊢ ( 𝐴 ≠ 0ℋ ↔ ∃ 𝑦 ∈ 𝐴 𝑦 ≠ 0ℎ )
3	1	sheli	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ )
4		h1da	⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑦 ≠ 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝑦 } ) ) ∈ HAtoms )
5	3 4	sylan	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝑦 } ) ) ∈ HAtoms )
6		sh1dle	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ { 𝑦 } ) ) ⊆ 𝐴 )
7	1 6	mpan	⊢ ( 𝑦 ∈ 𝐴 → ( ⊥ ‘ ( ⊥ ‘ { 𝑦 } ) ) ⊆ 𝐴 )
8	7	adantr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝑦 } ) ) ⊆ 𝐴 )
9		sseq1	⊢ ( 𝑥 = ( ⊥ ‘ ( ⊥ ‘ { 𝑦 } ) ) → ( 𝑥 ⊆ 𝐴 ↔ ( ⊥ ‘ ( ⊥ ‘ { 𝑦 } ) ) ⊆ 𝐴 ) )
10	9	rspcev	⊢ ( ( ( ⊥ ‘ ( ⊥ ‘ { 𝑦 } ) ) ∈ HAtoms ∧ ( ⊥ ‘ ( ⊥ ‘ { 𝑦 } ) ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )
11	5 8 10	syl2anc	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )
12	11	rexlimiva	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑦 ≠ 0ℎ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )
13	2 12	sylbi	⊢ ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )