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	⊢ 𝐴 ∈ Sℋ
Assertion	shatomistici	⊢ 𝐴 = ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		shatomistic.1	⊢ 𝐴 ∈ Sℋ
2		eleq1	⊢ ( 𝑦 = 0ℎ → ( 𝑦 ∈ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ↔ 0ℎ ∈ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) )
3	1	sheli	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ )
4		spansnsh	⊢ ( 𝑦 ∈ ℋ → ( span ‘ { 𝑦 } ) ∈ Sℋ )
5		spanid	⊢ ( ( span ‘ { 𝑦 } ) ∈ Sℋ → ( span ‘ ( span ‘ { 𝑦 } ) ) = ( span ‘ { 𝑦 } ) )
6	3 4 5	3syl	⊢ ( 𝑦 ∈ 𝐴 → ( span ‘ ( span ‘ { 𝑦 } ) ) = ( span ‘ { 𝑦 } ) )
7	6	adantr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → ( span ‘ ( span ‘ { 𝑦 } ) ) = ( span ‘ { 𝑦 } ) )
8		spansna	⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑦 ≠ 0ℎ ) → ( span ‘ { 𝑦 } ) ∈ HAtoms )
9	3 8	sylan	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → ( span ‘ { 𝑦 } ) ∈ HAtoms )
10		spansnss	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ 𝐴 ) → ( span ‘ { 𝑦 } ) ⊆ 𝐴 )
11	1 10	mpan	⊢ ( 𝑦 ∈ 𝐴 → ( span ‘ { 𝑦 } ) ⊆ 𝐴 )
12	11	adantr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → ( span ‘ { 𝑦 } ) ⊆ 𝐴 )
13		sseq1	⊢ ( 𝑥 = ( span ‘ { 𝑦 } ) → ( 𝑥 ⊆ 𝐴 ↔ ( span ‘ { 𝑦 } ) ⊆ 𝐴 ) )
14	13	elrab	⊢ ( ( span ‘ { 𝑦 } ) ∈ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ↔ ( ( span ‘ { 𝑦 } ) ∈ HAtoms ∧ ( span ‘ { 𝑦 } ) ⊆ 𝐴 ) )
15	9 12 14	sylanbrc	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → ( span ‘ { 𝑦 } ) ∈ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )
16		elssuni	⊢ ( ( span ‘ { 𝑦 } ) ∈ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → ( span ‘ { 𝑦 } ) ⊆ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )
17		atssch	⊢ HAtoms ⊆ Cℋ
18		chsssh	⊢ Cℋ ⊆ Sℋ
19	17 18	sstri	⊢ HAtoms ⊆ Sℋ
20		rabss2	⊢ ( HAtoms ⊆ Sℋ → { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } )
21		uniss	⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } → ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } )
22	19 20 21	mp2b	⊢ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 }
23		unimax	⊢ ( 𝐴 ∈ Sℋ → ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )
24	1 23	ax-mp	⊢ ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } = 𝐴
25	1	shssii	⊢ 𝐴 ⊆ ℋ
26	24 25	eqsstri	⊢ ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ ℋ
27	22 26	sstri	⊢ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ ℋ
28		spanss	⊢ ( ( ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ ℋ ∧ ( span ‘ { 𝑦 } ) ⊆ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) → ( span ‘ ( span ‘ { 𝑦 } ) ) ⊆ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
29	27 28	mpan	⊢ ( ( span ‘ { 𝑦 } ) ⊆ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → ( span ‘ ( span ‘ { 𝑦 } ) ) ⊆ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
30	15 16 29	3syl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → ( span ‘ ( span ‘ { 𝑦 } ) ) ⊆ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
31	7 30	eqsstrrd	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → ( span ‘ { 𝑦 } ) ⊆ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
32		spansnid	⊢ ( 𝑦 ∈ ℋ → 𝑦 ∈ ( span ‘ { 𝑦 } ) )
33	3 32	syl	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( span ‘ { 𝑦 } ) )
34	33	adantr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → 𝑦 ∈ ( span ‘ { 𝑦 } ) )
35	31 34	sseldd	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ≠ 0ℎ ) → 𝑦 ∈ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
36		spancl	⊢ ( ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ ℋ → ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∈ Sℋ )
37		sh0	⊢ ( ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∈ Sℋ → 0ℎ ∈ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
38	27 36 37	mp2b	⊢ 0ℎ ∈ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )
39	38	a1i	⊢ ( 𝑦 ∈ 𝐴 → 0ℎ ∈ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
40	2 35 39	pm2.61ne	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
41	40	ssriv	⊢ 𝐴 ⊆ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )
42		spanss	⊢ ( ( ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ ℋ ∧ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } ) → ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ⊆ ( span ‘ ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } ) )
43	26 22 42	mp2an	⊢ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ⊆ ( span ‘ ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } )
44	24	fveq2i	⊢ ( span ‘ ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } ) = ( span ‘ 𝐴 )
45		spanid	⊢ ( 𝐴 ∈ Sℋ → ( span ‘ 𝐴 ) = 𝐴 )
46	1 45	ax-mp	⊢ ( span ‘ 𝐴 ) = 𝐴
47	44 46	eqtri	⊢ ( span ‘ ∪ { 𝑥 ∈ Sℋ ∣ 𝑥 ⊆ 𝐴 } ) = 𝐴
48	43 47	sseqtri	⊢ ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ⊆ 𝐴
49	41 48	eqssi	⊢ 𝐴 = ( span ‘ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )