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 imbitrrdi ⊢ ( ( 𝐴 ∈ 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 imbitrrid ⊢ ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) → ( ( 𝑥 ∈ ℋ ∧ 𝑥 ≠ 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 ‘ { 𝑥 } ) ) )