This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∣ 𝑥 ⊆ 𝐴 } )