Metamath Proof Explorer


Theorem atom1d

Description: The 1-dimensional subspaces of Hilbert space are its atoms. Part of Remark 10.3.5 of BeltramettiCassinelli p. 107. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atom1d
|- ( A e. HAtoms <-> E. x e. ~H ( x =/= 0h /\ A = ( span ` { x } ) ) )

Proof

Step Hyp Ref Expression
1 elat2
 |-  ( A e. HAtoms <-> ( A e. CH /\ ( A =/= 0H /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) )
2 chne0
 |-  ( A e. CH -> ( A =/= 0H <-> E. x e. A x =/= 0h ) )
3 nfv
 |-  F/ x A e. CH
4 nfv
 |-  F/ x A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) )
5 nfre1
 |-  F/ x E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) )
6 4 5 nfim
 |-  F/ x ( A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) -> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) )
7 chel
 |-  ( ( A e. CH /\ x e. A ) -> x e. ~H )
8 7 adantrr
 |-  ( ( A e. CH /\ ( x e. A /\ x =/= 0h ) ) -> x e. ~H )
9 8 adantrr
 |-  ( ( A e. CH /\ ( ( x e. A /\ x =/= 0h ) /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> x e. ~H )
10 simprlr
 |-  ( ( A e. CH /\ ( ( x e. A /\ x =/= 0h ) /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> x =/= 0h )
11 h1dn0
 |-  ( ( x e. ~H /\ x =/= 0h ) -> ( _|_ ` ( _|_ ` { x } ) ) =/= 0H )
12 7 11 sylan
 |-  ( ( ( A e. CH /\ x e. A ) /\ x =/= 0h ) -> ( _|_ ` ( _|_ ` { x } ) ) =/= 0H )
13 12 anasss
 |-  ( ( A e. CH /\ ( x e. A /\ x =/= 0h ) ) -> ( _|_ ` ( _|_ ` { x } ) ) =/= 0H )
14 13 adantrr
 |-  ( ( A e. CH /\ ( ( x e. A /\ x =/= 0h ) /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> ( _|_ ` ( _|_ ` { x } ) ) =/= 0H )
15 ch1dle
 |-  ( ( A e. CH /\ x e. A ) -> ( _|_ ` ( _|_ ` { x } ) ) C_ A )
16 snssi
 |-  ( x e. ~H -> { x } C_ ~H )
17 occl
 |-  ( { x } C_ ~H -> ( _|_ ` { x } ) e. CH )
18 7 16 17 3syl
 |-  ( ( A e. CH /\ x e. A ) -> ( _|_ ` { x } ) e. CH )
19 choccl
 |-  ( ( _|_ ` { x } ) e. CH -> ( _|_ ` ( _|_ ` { x } ) ) e. CH )
20 sseq1
 |-  ( y = ( _|_ ` ( _|_ ` { x } ) ) -> ( y C_ A <-> ( _|_ ` ( _|_ ` { x } ) ) C_ A ) )
21 eqeq1
 |-  ( y = ( _|_ ` ( _|_ ` { x } ) ) -> ( y = A <-> ( _|_ ` ( _|_ ` { x } ) ) = A ) )
22 eqeq1
 |-  ( y = ( _|_ ` ( _|_ ` { x } ) ) -> ( y = 0H <-> ( _|_ ` ( _|_ ` { x } ) ) = 0H ) )
23 21 22 orbi12d
 |-  ( y = ( _|_ ` ( _|_ ` { x } ) ) -> ( ( y = A \/ y = 0H ) <-> ( ( _|_ ` ( _|_ ` { x } ) ) = A \/ ( _|_ ` ( _|_ ` { x } ) ) = 0H ) ) )
24 20 23 imbi12d
 |-  ( y = ( _|_ ` ( _|_ ` { x } ) ) -> ( ( y C_ A -> ( y = A \/ y = 0H ) ) <-> ( ( _|_ ` ( _|_ ` { x } ) ) C_ A -> ( ( _|_ ` ( _|_ ` { x } ) ) = A \/ ( _|_ ` ( _|_ ` { x } ) ) = 0H ) ) ) )
25 24 rspcv
 |-  ( ( _|_ ` ( _|_ ` { x } ) ) e. CH -> ( A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) -> ( ( _|_ ` ( _|_ ` { x } ) ) C_ A -> ( ( _|_ ` ( _|_ ` { x } ) ) = A \/ ( _|_ ` ( _|_ ` { x } ) ) = 0H ) ) ) )
26 18 19 25 3syl
 |-  ( ( A e. CH /\ x e. A ) -> ( A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) -> ( ( _|_ ` ( _|_ ` { x } ) ) C_ A -> ( ( _|_ ` ( _|_ ` { x } ) ) = A \/ ( _|_ ` ( _|_ ` { x } ) ) = 0H ) ) ) )
27 15 26 mpid
 |-  ( ( A e. CH /\ x e. A ) -> ( A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) -> ( ( _|_ ` ( _|_ ` { x } ) ) = A \/ ( _|_ ` ( _|_ ` { x } ) ) = 0H ) ) )
28 27 impr
 |-  ( ( A e. CH /\ ( x e. A /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> ( ( _|_ ` ( _|_ ` { x } ) ) = A \/ ( _|_ ` ( _|_ ` { x } ) ) = 0H ) )
29 28 adantrlr
 |-  ( ( A e. CH /\ ( ( x e. A /\ x =/= 0h ) /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> ( ( _|_ ` ( _|_ ` { x } ) ) = A \/ ( _|_ ` ( _|_ ` { x } ) ) = 0H ) )
30 29 ord
 |-  ( ( A e. CH /\ ( ( x e. A /\ x =/= 0h ) /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> ( -. ( _|_ ` ( _|_ ` { x } ) ) = A -> ( _|_ ` ( _|_ ` { x } ) ) = 0H ) )
31 nne
 |-  ( -. ( _|_ ` ( _|_ ` { x } ) ) =/= 0H <-> ( _|_ ` ( _|_ ` { x } ) ) = 0H )
32 30 31 syl6ibr
 |-  ( ( A e. CH /\ ( ( x e. A /\ x =/= 0h ) /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> ( -. ( _|_ ` ( _|_ ` { x } ) ) = A -> -. ( _|_ ` ( _|_ ` { x } ) ) =/= 0H ) )
33 14 32 mt4d
 |-  ( ( A e. CH /\ ( ( x e. A /\ x =/= 0h ) /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> ( _|_ ` ( _|_ ` { x } ) ) = A )
34 33 eqcomd
 |-  ( ( A e. CH /\ ( ( x e. A /\ x =/= 0h ) /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> A = ( _|_ ` ( _|_ ` { x } ) ) )
35 rspe
 |-  ( ( x e. ~H /\ ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) ) -> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) )
36 9 10 34 35 syl12anc
 |-  ( ( A e. CH /\ ( ( x e. A /\ x =/= 0h ) /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) )
37 36 exp44
 |-  ( A e. CH -> ( x e. A -> ( x =/= 0h -> ( A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) -> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) ) ) ) )
38 3 6 37 rexlimd
 |-  ( A e. CH -> ( E. x e. A x =/= 0h -> ( A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) -> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) ) ) )
39 2 38 sylbid
 |-  ( A e. CH -> ( A =/= 0H -> ( A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) -> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) ) ) )
40 39 imp32
 |-  ( ( A e. CH /\ ( A =/= 0H /\ A. y e. CH ( y C_ A -> ( y = A \/ y = 0H ) ) ) ) -> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) )
41 1 40 sylbi
 |-  ( A e. HAtoms -> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) )
42 h1da
 |-  ( ( x e. ~H /\ x =/= 0h ) -> ( _|_ ` ( _|_ ` { x } ) ) e. HAtoms )
43 eleq1
 |-  ( A = ( _|_ ` ( _|_ ` { x } ) ) -> ( A e. HAtoms <-> ( _|_ ` ( _|_ ` { x } ) ) e. HAtoms ) )
44 42 43 syl5ibr
 |-  ( A = ( _|_ ` ( _|_ ` { x } ) ) -> ( ( x e. ~H /\ x =/= 0h ) -> A e. HAtoms ) )
45 44 expdcom
 |-  ( x e. ~H -> ( x =/= 0h -> ( A = ( _|_ ` ( _|_ ` { x } ) ) -> A e. HAtoms ) ) )
46 45 impd
 |-  ( x e. ~H -> ( ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) -> A e. HAtoms ) )
47 46 rexlimiv
 |-  ( E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) -> A e. HAtoms )
48 41 47 impbii
 |-  ( A e. HAtoms <-> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) )
49 spansn
 |-  ( x e. ~H -> ( span ` { x } ) = ( _|_ ` ( _|_ ` { x } ) ) )
50 49 eqeq2d
 |-  ( x e. ~H -> ( A = ( span ` { x } ) <-> A = ( _|_ ` ( _|_ ` { x } ) ) ) )
51 50 anbi2d
 |-  ( x e. ~H -> ( ( x =/= 0h /\ A = ( span ` { x } ) ) <-> ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) ) )
52 51 rexbiia
 |-  ( E. x e. ~H ( x =/= 0h /\ A = ( span ` { x } ) ) <-> E. x e. ~H ( x =/= 0h /\ A = ( _|_ ` ( _|_ ` { x } ) ) ) )
53 48 52 bitr4i
 |-  ( A e. HAtoms <-> E. x e. ~H ( x =/= 0h /\ A = ( span ` { x } ) ) )