Theorem shatomistici

Description: The lattice of Hilbert subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 26-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypothesis	shatomistic.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shatomistici	$$⊢A=\mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		shatomistic.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		eleq1	$$⊢y=0_{ℎ}\to \left(y\in \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\leftrightarrow 0_{ℎ}\in \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)$$
3	1	sheli	$$⊢y\in A\to y\in \mathscr{H}$$
4		spansnsh	$$⊢y\in \mathscr{H}\to \mathrm{span}\left(\left\{y\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
5		spanid	$$⊢\mathrm{span}\left(\left\{y\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}\to \mathrm{span}\left(\mathrm{span}\left(\left\{y\right\}\right)\right)=\mathrm{span}\left(\left\{y\right\}\right)$$
6	3 4 5	3syl	$$⊢y\in A\to \mathrm{span}\left(\mathrm{span}\left(\left\{y\right\}\right)\right)=\mathrm{span}\left(\left\{y\right\}\right)$$
7	6	adantr	$$⊢\left(y\in A\wedge y\ne 0_{ℎ}\right)\to \mathrm{span}\left(\mathrm{span}\left(\left\{y\right\}\right)\right)=\mathrm{span}\left(\left\{y\right\}\right)$$
8		spansna	$$⊢\left(y\in \mathscr{H}\wedge y\ne 0_{ℎ}\right)\to \mathrm{span}\left(\left\{y\right\}\right)\in \mathrm{HAtoms}$$
9	3 8	sylan	$$⊢\left(y\in A\wedge y\ne 0_{ℎ}\right)\to \mathrm{span}\left(\left\{y\right\}\right)\in \mathrm{HAtoms}$$
10		spansnss	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge y\in A\right)\to \mathrm{span}\left(\left\{y\right\}\right)\subseteq A$$
11	1 10	mpan	$$⊢y\in A\to \mathrm{span}\left(\left\{y\right\}\right)\subseteq A$$
12	11	adantr	$$⊢\left(y\in A\wedge y\ne 0_{ℎ}\right)\to \mathrm{span}\left(\left\{y\right\}\right)\subseteq A$$
13		sseq1	$$⊢x=\mathrm{span}\left(\left\{y\right\}\right)\to \left(x\subseteq A\leftrightarrow \mathrm{span}\left(\left\{y\right\}\right)\subseteq A\right)$$
14	13	elrab	$$⊢\mathrm{span}\left(\left\{y\right\}\right)\in \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\leftrightarrow \left(\mathrm{span}\left(\left\{y\right\}\right)\in \mathrm{HAtoms}\wedge \mathrm{span}\left(\left\{y\right\}\right)\subseteq A\right)$$
15	9 12 14	sylanbrc	$$⊢\left(y\in A\wedge y\ne 0_{ℎ}\right)\to \mathrm{span}\left(\left\{y\right\}\right)\in \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}$$
16		elssuni	$$⊢\mathrm{span}\left(\left\{y\right\}\right)\in \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\to \mathrm{span}\left(\left\{y\right\}\right)\subseteq \bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}$$
17		atssch	$$⊢\mathrm{HAtoms}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
18		chsssh	$$⊢{\mathbf{C}}_{\mathscr{H}}\subseteq {\mathbf{S}}_{\mathscr{H}}$$
19	17 18	sstri	$$⊢\mathrm{HAtoms}\subseteq {\mathbf{S}}_{\mathscr{H}}$$
20		rabss2	$$⊢\mathrm{HAtoms}\subseteq {\mathbf{S}}_{\mathscr{H}}\to \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}$$
21		uniss	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}\to \bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}$$
22	19 20 21	mp2b	$$⊢\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}$$
23		unimax	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}=A$$
24	1 23	ax-mp	$$⊢\bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}=A$$
25	1	shssii	$$⊢A\subseteq \mathscr{H}$$
26	24 25	eqsstri	$$⊢\bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq \mathscr{H}$$
27	22 26	sstri	$$⊢\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \mathscr{H}$$
28		spanss	$$⊢\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \mathscr{H}\wedge \mathrm{span}\left(\left\{y\right\}\right)\subseteq \bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\to \mathrm{span}\left(\mathrm{span}\left(\left\{y\right\}\right)\right)\subseteq \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
29	27 28	mpan	$$⊢\mathrm{span}\left(\left\{y\right\}\right)\subseteq \bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\to \mathrm{span}\left(\mathrm{span}\left(\left\{y\right\}\right)\right)\subseteq \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
30	15 16 29	3syl	$$⊢\left(y\in A\wedge y\ne 0_{ℎ}\right)\to \mathrm{span}\left(\mathrm{span}\left(\left\{y\right\}\right)\right)\subseteq \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
31	7 30	eqsstrrd	$$⊢\left(y\in A\wedge y\ne 0_{ℎ}\right)\to \mathrm{span}\left(\left\{y\right\}\right)\subseteq \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
32		spansnid	$$⊢y\in \mathscr{H}\to y\in \mathrm{span}\left(\left\{y\right\}\right)$$
33	3 32	syl	$$⊢y\in A\to y\in \mathrm{span}\left(\left\{y\right\}\right)$$
34	33	adantr	$$⊢\left(y\in A\wedge y\ne 0_{ℎ}\right)\to y\in \mathrm{span}\left(\left\{y\right\}\right)$$
35	31 34	sseldd	$$⊢\left(y\in A\wedge y\ne 0_{ℎ}\right)\to y\in \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
36		spancl	$$⊢\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \mathscr{H}\to \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
37		sh0	$$⊢\mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}\to 0_{ℎ}\in \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
38	27 36 37	mp2b	$$⊢0_{ℎ}\in \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
39	38	a1i	$$⊢y\in A\to 0_{ℎ}\in \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
40	2 35 39	pm2.61ne	$$⊢y\in A\to y\in \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
41	40	ssriv	$$⊢A\subseteq \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
42		spanss	$$⊢\left(\bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq \mathscr{H}\wedge \bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}\right)\to \mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\subseteq \mathrm{span}\left(\bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}\right)$$
43	26 22 42	mp2an	$$⊢\mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\subseteq \mathrm{span}\left(\bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}\right)$$
44	24	fveq2i	$$⊢\mathrm{span}\left(\bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}\right)=\mathrm{span}\left(A\right)$$
45		spanid	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \mathrm{span}\left(A\right)=A$$
46	1 45	ax-mp	$$⊢\mathrm{span}\left(A\right)=A$$
47	44 46	eqtri	$$⊢\mathrm{span}\left(\bigcup \left\{x\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq A\right\}\right)=A$$
48	43 47	sseqtri	$$⊢\mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\subseteq A$$
49	41 48	eqssi	$$⊢A=\mathrm{span}\left(\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$