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 ⊢A∈Cℋ
spansncv.2 ⊢B∈Cℋ
spansncv.3 ⊢C∈ℋ
Assertion spansncvi ⊢A⊂B∧B⊆A∨ℋspan⁡C→B=A∨ℋspan⁡C

Proof

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