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 
|- A e. SH
Assertion shatomistici 
|- A = ( span ` U. { x e. HAtoms | x C_ A } )

Proof

Step Hyp Ref Expression
1 shatomistic.1 
 |-  A e. SH
2 eleq1 
 |-  ( y = 0h -> ( y e. ( span ` U. { x e. HAtoms | x C_ A } ) <-> 0h e. ( span ` U. { x e. HAtoms | x C_ A } ) ) )
3 1 sheli 
 |-  ( y e. A -> y e. ~H )
4 spansnsh 
 |-  ( y e. ~H -> ( span ` { y } ) e. SH )
5 spanid 
 |-  ( ( span ` { y } ) e. SH -> ( span ` ( span ` { y } ) ) = ( span ` { y } ) )
6 3 4 5 3syl 
 |-  ( y e. A -> ( span ` ( span ` { y } ) ) = ( span ` { y } ) )
7 6 adantr 
 |-  ( ( y e. A /\ y =/= 0h ) -> ( span ` ( span ` { y } ) ) = ( span ` { y } ) )
8 spansna 
 |-  ( ( y e. ~H /\ y =/= 0h ) -> ( span ` { y } ) e. HAtoms )
9 3 8 sylan 
 |-  ( ( y e. A /\ y =/= 0h ) -> ( span ` { y } ) e. HAtoms )
10 spansnss 
 |-  ( ( A e. SH /\ y e. A ) -> ( span ` { y } ) C_ A )
11 1 10 mpan 
 |-  ( y e. A -> ( span ` { y } ) C_ A )
12 11 adantr 
 |-  ( ( y e. A /\ y =/= 0h ) -> ( span ` { y } ) C_ A )
13 sseq1 
 |-  ( x = ( span ` { y } ) -> ( x C_ A <-> ( span ` { y } ) C_ A ) )
14 13 elrab 
 |-  ( ( span ` { y } ) e. { x e. HAtoms | x C_ A } <-> ( ( span ` { y } ) e. HAtoms /\ ( span ` { y } ) C_ A ) )
15 9 12 14 sylanbrc 
 |-  ( ( y e. A /\ y =/= 0h ) -> ( span ` { y } ) e. { x e. HAtoms | x C_ A } )
16 elssuni 
 |-  ( ( span ` { y } ) e. { x e. HAtoms | x C_ A } -> ( span ` { y } ) C_ U. { x e. HAtoms | x C_ A } )
17 atssch 
 |-  HAtoms C_ CH
18 chsssh 
 |-  CH C_ SH
19 17 18 sstri 
 |-  HAtoms C_ SH
20 rabss2 
 |-  ( HAtoms C_ SH -> { x e. HAtoms | x C_ A } C_ { x e. SH | x C_ A } )
21 uniss 
 |-  ( { x e. HAtoms | x C_ A } C_ { x e. SH | x C_ A } -> U. { x e. HAtoms | x C_ A } C_ U. { x e. SH | x C_ A } )
22 19 20 21 mp2b 
 |-  U. { x e. HAtoms | x C_ A } C_ U. { x e. SH | x C_ A }
23 unimax 
 |-  ( A e. SH -> U. { x e. SH | x C_ A } = A )
24 1 23 ax-mp 
 |-  U. { x e. SH | x C_ A } = A
25 1 shssii 
 |-  A C_ ~H
26 24 25 eqsstri 
 |-  U. { x e. SH | x C_ A } C_ ~H
27 22 26 sstri 
 |-  U. { x e. HAtoms | x C_ A } C_ ~H
28 spanss 
 |-  ( ( U. { x e. HAtoms | x C_ A } C_ ~H /\ ( span ` { y } ) C_ U. { x e. HAtoms | x C_ A } ) -> ( span ` ( span ` { y } ) ) C_ ( span ` U. { x e. HAtoms | x C_ A } ) )
29 27 28 mpan 
 |-  ( ( span ` { y } ) C_ U. { x e. HAtoms | x C_ A } -> ( span ` ( span ` { y } ) ) C_ ( span ` U. { x e. HAtoms | x C_ A } ) )
30 15 16 29 3syl 
 |-  ( ( y e. A /\ y =/= 0h ) -> ( span ` ( span ` { y } ) ) C_ ( span ` U. { x e. HAtoms | x C_ A } ) )
31 7 30 eqsstrrd 
 |-  ( ( y e. A /\ y =/= 0h ) -> ( span ` { y } ) C_ ( span ` U. { x e. HAtoms | x C_ A } ) )
32 spansnid 
 |-  ( y e. ~H -> y e. ( span ` { y } ) )
33 3 32 syl 
 |-  ( y e. A -> y e. ( span ` { y } ) )
34 33 adantr 
 |-  ( ( y e. A /\ y =/= 0h ) -> y e. ( span ` { y } ) )
35 31 34 sseldd 
 |-  ( ( y e. A /\ y =/= 0h ) -> y e. ( span ` U. { x e. HAtoms | x C_ A } ) )
36 spancl 
 |-  ( U. { x e. HAtoms | x C_ A } C_ ~H -> ( span ` U. { x e. HAtoms | x C_ A } ) e. SH )
37 sh0 
 |-  ( ( span ` U. { x e. HAtoms | x C_ A } ) e. SH -> 0h e. ( span ` U. { x e. HAtoms | x C_ A } ) )
38 27 36 37 mp2b 
 |-  0h e. ( span ` U. { x e. HAtoms | x C_ A } )
39 38 a1i 
 |-  ( y e. A -> 0h e. ( span ` U. { x e. HAtoms | x C_ A } ) )
40 2 35 39 pm2.61ne 
 |-  ( y e. A -> y e. ( span ` U. { x e. HAtoms | x C_ A } ) )
41 40 ssriv 
 |-  A C_ ( span ` U. { x e. HAtoms | x C_ A } )
42 spanss 
 |-  ( ( U. { x e. SH | x C_ A } C_ ~H /\ U. { x e. HAtoms | x C_ A } C_ U. { x e. SH | x C_ A } ) -> ( span ` U. { x e. HAtoms | x C_ A } ) C_ ( span ` U. { x e. SH | x C_ A } ) )
43 26 22 42 mp2an 
 |-  ( span ` U. { x e. HAtoms | x C_ A } ) C_ ( span ` U. { x e. SH | x C_ A } )
44 24 fveq2i 
 |-  ( span ` U. { x e. SH | x C_ A } ) = ( span ` A )
45 spanid 
 |-  ( A e. SH -> ( span ` A ) = A )
46 1 45 ax-mp 
 |-  ( span ` A ) = A
47 44 46 eqtri 
 |-  ( span ` U. { x e. SH | x C_ A } ) = A
48 43 47 sseqtri 
 |-  ( span ` U. { x e. HAtoms | x C_ A } ) C_ A
49 41 48 eqssi 
 |-  A = ( span ` U. { x e. HAtoms | x C_ A } )