Metamath Proof Explorer

Theorem spansncvi

Description: Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of Kalmbach p. 153. (Contributed by NM, 7-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses spansncv.1 ⊢ 𝐴 ∈ Cℋ
spansncv.2 ⊢ 𝐵 ∈ Cℋ
spansncv.3 ⊢ 𝐶 ∈ ℋ
Assertion spansncvi ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ) → 𝐵 = ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) )

Proof

Step Hyp Ref Expression
1 spansncv.1 ⊢ 𝐴 ∈ Cℋ
2 spansncv.2 ⊢ 𝐵 ∈ Cℋ
3 spansncv.3 ⊢ 𝐶 ∈ ℋ
4 simpr ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ) → 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) )
5 pssss ⊢ ( 𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵 )
6 5 adantr ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ) → 𝐴 ⊆ 𝐵 )
7 pssnel ⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) )
8 ssel2 ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) )
9 1 3 spansnji ⊢ ( 𝐴 +ℋ ( span ‘ { 𝐶 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) )
10 9 eleq2i ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐶 } ) ) ↔ 𝑥 ∈ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) )
11 3 spansnchi ⊢ ( span ‘ { 𝐶 } ) ∈ Cℋ
12 1 11 chseli ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ ( span ‘ { 𝐶 } ) ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ ( span ‘ { 𝐶 } ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
13 10 12 bitr3i ⊢ ( 𝑥 ∈ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ ( span ‘ { 𝐶 } ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
14 eleq1 ⊢ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( 𝑥 ∈ 𝐵 ↔ ( 𝑦 +ℎ 𝑧 ) ∈ 𝐵 ) )
15 14 biimpac ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) → ( 𝑦 +ℎ 𝑧 ) ∈ 𝐵 )
16 5 sselda ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 )
17 2 chshii ⊢ 𝐵 ∈ Sℋ
18 shsubcl ⊢ ( ( 𝐵 ∈ Sℋ ∧ ( 𝑦 +ℎ 𝑧 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 +ℎ 𝑧 ) −ℎ 𝑦 ) ∈ 𝐵 )
19 17 18 mp3an1 ⊢ ( ( ( 𝑦 +ℎ 𝑧 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 +ℎ 𝑧 ) −ℎ 𝑦 ) ∈ 𝐵 )
20 15 16 19 syl2an ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∧ ( 𝐴 ⊊ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑦 +ℎ 𝑧 ) −ℎ 𝑦 ) ∈ 𝐵 )
21 20 exp43 ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( 𝐴 ⊊ 𝐵 → ( 𝑦 ∈ 𝐴 → ( ( 𝑦 +ℎ 𝑧 ) −ℎ 𝑦 ) ∈ 𝐵 ) ) ) )
22 21 com14 ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( 𝐴 ⊊ 𝐵 → ( 𝑥 ∈ 𝐵 → ( ( 𝑦 +ℎ 𝑧 ) −ℎ 𝑦 ) ∈ 𝐵 ) ) ) )
23 22 imp45 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) ∧ ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ) → ( ( 𝑦 +ℎ 𝑧 ) −ℎ 𝑦 ) ∈ 𝐵 )
24 1 cheli ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ )
25 11 cheli ⊢ ( 𝑧 ∈ ( span ‘ { 𝐶 } ) → 𝑧 ∈ ℋ )
26 hvpncan2 ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑦 +ℎ 𝑧 ) −ℎ 𝑦 ) = 𝑧 )
27 24 25 26 syl2an ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) → ( ( 𝑦 +ℎ 𝑧 ) −ℎ 𝑦 ) = 𝑧 )
28 27 eleq1d ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) → ( ( ( 𝑦 +ℎ 𝑧 ) −ℎ 𝑦 ) ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
29 23 28 syl5ib ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) → ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) ∧ ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ) → 𝑧 ∈ 𝐵 ) )
30 29 imp ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) ∧ ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ) ) → 𝑧 ∈ 𝐵 )
31 30 anandis ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ ( span ‘ { 𝐶 } ) ∧ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) ∧ ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ) ) → 𝑧 ∈ 𝐵 )
32 31 exp45 ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑧 ∈ ( span ‘ { 𝐶 } ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 ) ) ) )
33 32 imp41 ⊢ ( ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∧ ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
34 33 adantrr ⊢ ( ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∧ ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ) → 𝑧 ∈ 𝐵 )
35 oveq2 ⊢ ( 𝑧 = 0ℎ → ( 𝑦 +ℎ 𝑧 ) = ( 𝑦 +ℎ 0ℎ ) )
36 ax-hvaddid ⊢ ( 𝑦 ∈ ℋ → ( 𝑦 +ℎ 0ℎ ) = 𝑦 )
37 24 36 syl ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑦 +ℎ 0ℎ ) = 𝑦 )
38 35 37 sylan9eqr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 0ℎ ) → ( 𝑦 +ℎ 𝑧 ) = 𝑦 )
39 38 eqeq2d ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 0ℎ ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) ↔ 𝑥 = 𝑦 ) )
40 eleq1a ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝑥 ∈ 𝐴 ) )
41 40 adantr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 0ℎ ) → ( 𝑥 = 𝑦 → 𝑥 ∈ 𝐴 ) )
42 39 41 sylbid ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 0ℎ ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ 𝐴 ) )
43 42 impancom ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) → ( 𝑧 = 0ℎ → 𝑥 ∈ 𝐴 ) )
44 43 necon3bd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) → ( ¬ 𝑥 ∈ 𝐴 → 𝑧 ≠ 0ℎ ) )
45 44 imp ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝑧 ≠ 0ℎ )
46 spansnss ⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝑧 ∈ 𝐵 ) → ( span ‘ { 𝑧 } ) ⊆ 𝐵 )
47 17 46 mpan ⊢ ( 𝑧 ∈ 𝐵 → ( span ‘ { 𝑧 } ) ⊆ 𝐵 )
48 spansneleq ⊢ ( ( 𝐶 ∈ ℋ ∧ 𝑧 ≠ 0ℎ ) → ( 𝑧 ∈ ( span ‘ { 𝐶 } ) → ( span ‘ { 𝑧 } ) = ( span ‘ { 𝐶 } ) ) )
49 3 48 mpan ⊢ ( 𝑧 ≠ 0ℎ → ( 𝑧 ∈ ( span ‘ { 𝐶 } ) → ( span ‘ { 𝑧 } ) = ( span ‘ { 𝐶 } ) ) )
50 49 imp ⊢ ( ( 𝑧 ≠ 0ℎ ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) → ( span ‘ { 𝑧 } ) = ( span ‘ { 𝐶 } ) )
51 50 sseq1d ⊢ ( ( 𝑧 ≠ 0ℎ ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) → ( ( span ‘ { 𝑧 } ) ⊆ 𝐵 ↔ ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
52 47 51 syl5ib ⊢ ( ( 𝑧 ≠ 0ℎ ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) → ( 𝑧 ∈ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
53 52 ancoms ⊢ ( ( 𝑧 ∈ ( span ‘ { 𝐶 } ) ∧ 𝑧 ≠ 0ℎ ) → ( 𝑧 ∈ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
54 45 53 sylan2 ⊢ ( ( 𝑧 ∈ ( span ‘ { 𝐶 } ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ) → ( 𝑧 ∈ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
55 54 exp44 ⊢ ( 𝑧 ∈ ( span ‘ { 𝐶 } ) → ( 𝑦 ∈ 𝐴 → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( ¬ 𝑥 ∈ 𝐴 → ( 𝑧 ∈ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) ) ) ) )
56 55 com12 ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑧 ∈ ( span ‘ { 𝐶 } ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( ¬ 𝑥 ∈ 𝐴 → ( 𝑧 ∈ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) ) ) ) )
57 56 imp41 ⊢ ( ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
58 57 adantrl ⊢ ( ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∧ ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ) → ( 𝑧 ∈ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
59 34 58 mpd ⊢ ( ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) ∧ 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∧ ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ) → ( span ‘ { 𝐶 } ) ⊆ 𝐵 )
60 59 exp43 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( span ‘ { 𝐶 } ) ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ 𝐴 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) ) ) )
61 60 rexlimivv ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ ( span ‘ { 𝐶 } ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ 𝐴 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) ) )
62 13 61 sylbi ⊢ ( 𝑥 ∈ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) → ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ 𝐴 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) ) )
63 8 62 syl ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ 𝐴 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) ) )
64 63 imp ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( ¬ 𝑥 ∈ 𝐴 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
65 64 anandirs ⊢ ( ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ∧ 𝐴 ⊊ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ 𝐴 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
66 65 expimpd ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ∧ 𝐴 ⊊ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
67 66 exlimdv ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ∧ 𝐴 ⊊ 𝐵 ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
68 7 67 syl5 ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ∧ 𝐴 ⊊ 𝐵 ) → ( 𝐴 ⊊ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
69 68 ex ⊢ ( 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) → ( 𝐴 ⊊ 𝐵 → ( 𝐴 ⊊ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) ) )
70 69 pm2.43d ⊢ ( 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) → ( 𝐴 ⊊ 𝐵 → ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) )
71 70 impcom ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ) → ( span ‘ { 𝐶 } ) ⊆ 𝐵 )
72 1 11 2 chlubii ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( span ‘ { 𝐶 } ) ⊆ 𝐵 ) → ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ⊆ 𝐵 )
73 6 71 72 syl2anc ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ) → ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ⊆ 𝐵 )
74 4 73 eqssd ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) ) → 𝐵 = ( 𝐴 ∨ℋ ( span ‘ { 𝐶 } ) ) )