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 ( 𝐴 ∈ HAtoms ↔ ∃ 𝑥 ∈ ℋ ( 𝑥 ≠ 0𝐴 = ( span ‘ { 𝑥 } ) ) )

Proof

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