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 e. CH
spansncv.2 
|- B e. CH
spansncv.3 
|- C e. ~H
Assertion spansncvi 
|- ( ( A C. B /\ B C_ ( A vH ( span ` { C } ) ) ) -> B = ( A vH ( span ` { C } ) ) )

Proof

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