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 HAtoms x x 0 A = span x

Proof

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