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 S
Assertion shatomici A 0 x HAtoms x A

Proof

Step Hyp Ref Expression
1 shatomic.1 A S
2 1 shne0i A 0 y A y 0
3 1 sheli y A y
4 h1da y y 0 y HAtoms
5 3 4 sylan y A y 0 y HAtoms
6 sh1dle A S y A y A
7 1 6 mpan y A y A
8 7 adantr y A y 0 y A
9 sseq1 x = y x A y A
10 9 rspcev y HAtoms y A x HAtoms x A
11 5 8 10 syl2anc y A y 0 x HAtoms x A
12 11 rexlimiva y A y 0 x HAtoms x A
13 2 12 sylbi A 0 x HAtoms x A