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

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 imbitrrdi 
 |-  ( ( 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 imbitrrid 
 |-  ( 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 } ) ) )