Metamath Proof Explorer

Theorem strlem1

Description: Lemma for strong state theorem: if closed subspace A is not contained in B , there is a unit vector u in their difference. (Contributed by NM, 25-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses strlem1.1 
|- A e. CH
strlem1.2 
|- B e. CH
Assertion strlem1 
|- ( -. A C_ B -> E. u e. ( A \ B ) ( normh ` u ) = 1 )

Proof

Step Hyp Ref Expression
1 strlem1.1 
 |-  A e. CH
2 strlem1.2 
 |-  B e. CH
3 neq0 
 |-  ( -. ( A \ B ) = (/) <-> E. x x e. ( A \ B ) )
4 ssdif0 
 |-  ( A C_ B <-> ( A \ B ) = (/) )
5 3 4 xchnxbir 
 |-  ( -. A C_ B <-> E. x x e. ( A \ B ) )
6 eldifi 
 |-  ( x e. ( A \ B ) -> x e. A )
7 1 cheli 
 |-  ( x e. A -> x e. ~H )
8 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
9 6 7 8 3syl 
 |-  ( x e. ( A \ B ) -> ( normh ` x ) e. RR )
10 ch0 
 |-  ( B e. CH -> 0h e. B )
11 2 10 ax-mp 
 |-  0h e. B
12 eldifn 
 |-  ( 0h e. ( A \ B ) -> -. 0h e. B )
13 11 12 mt2 
 |-  -. 0h e. ( A \ B )
14 eleq1 
 |-  ( x = 0h -> ( x e. ( A \ B ) <-> 0h e. ( A \ B ) ) )
15 13 14 mtbiri 
 |-  ( x = 0h -> -. x e. ( A \ B ) )
16 15 con2i 
 |-  ( x e. ( A \ B ) -> -. x = 0h )
17 norm-i 
 |-  ( x e. ~H -> ( ( normh ` x ) = 0 <-> x = 0h ) )
18 6 7 17 3syl 
 |-  ( x e. ( A \ B ) -> ( ( normh ` x ) = 0 <-> x = 0h ) )
19 16 18 mtbird 
 |-  ( x e. ( A \ B ) -> -. ( normh ` x ) = 0 )
20 19 neqned 
 |-  ( x e. ( A \ B ) -> ( normh ` x ) =/= 0 )
21 9 20 rereccld 
 |-  ( x e. ( A \ B ) -> ( 1 / ( normh ` x ) ) e. RR )
22 21 recnd 
 |-  ( x e. ( A \ B ) -> ( 1 / ( normh ` x ) ) e. CC )
23 1 chshii 
 |-  A e. SH
24 shmulcl 
 |-  ( ( A e. SH /\ ( 1 / ( normh ` x ) ) e. CC /\ x e. A ) -> ( ( 1 / ( normh ` x ) ) .h x ) e. A )
25 23 24 mp3an1 
 |-  ( ( ( 1 / ( normh ` x ) ) e. CC /\ x e. A ) -> ( ( 1 / ( normh ` x ) ) .h x ) e. A )
26 25 ex 
 |-  ( ( 1 / ( normh ` x ) ) e. CC -> ( x e. A -> ( ( 1 / ( normh ` x ) ) .h x ) e. A ) )
27 22 26 syl 
 |-  ( x e. ( A \ B ) -> ( x e. A -> ( ( 1 / ( normh ` x ) ) .h x ) e. A ) )
28 9 recnd 
 |-  ( x e. ( A \ B ) -> ( normh ` x ) e. CC )
29 2 chshii 
 |-  B e. SH
30 shmulcl 
 |-  ( ( B e. SH /\ ( normh ` x ) e. CC /\ ( ( 1 / ( normh ` x ) ) .h x ) e. B ) -> ( ( normh ` x ) .h ( ( 1 / ( normh ` x ) ) .h x ) ) e. B )
31 29 30 mp3an1 
 |-  ( ( ( normh ` x ) e. CC /\ ( ( 1 / ( normh ` x ) ) .h x ) e. B ) -> ( ( normh ` x ) .h ( ( 1 / ( normh ` x ) ) .h x ) ) e. B )
32 31 ex 
 |-  ( ( normh ` x ) e. CC -> ( ( ( 1 / ( normh ` x ) ) .h x ) e. B -> ( ( normh ` x ) .h ( ( 1 / ( normh ` x ) ) .h x ) ) e. B ) )
33 28 32 syl 
 |-  ( x e. ( A \ B ) -> ( ( ( 1 / ( normh ` x ) ) .h x ) e. B -> ( ( normh ` x ) .h ( ( 1 / ( normh ` x ) ) .h x ) ) e. B ) )
34 28 20 recidd 
 |-  ( x e. ( A \ B ) -> ( ( normh ` x ) x. ( 1 / ( normh ` x ) ) ) = 1 )
35 34 oveq1d 
 |-  ( x e. ( A \ B ) -> ( ( ( normh ` x ) x. ( 1 / ( normh ` x ) ) ) .h x ) = ( 1 .h x ) )
36 6 7 syl 
 |-  ( x e. ( A \ B ) -> x e. ~H )
37 ax-hvmulass 
 |-  ( ( ( normh ` x ) e. CC /\ ( 1 / ( normh ` x ) ) e. CC /\ x e. ~H ) -> ( ( ( normh ` x ) x. ( 1 / ( normh ` x ) ) ) .h x ) = ( ( normh ` x ) .h ( ( 1 / ( normh ` x ) ) .h x ) ) )
38 28 22 36 37 syl3anc 
 |-  ( x e. ( A \ B ) -> ( ( ( normh ` x ) x. ( 1 / ( normh ` x ) ) ) .h x ) = ( ( normh ` x ) .h ( ( 1 / ( normh ` x ) ) .h x ) ) )
39 ax-hvmulid 
 |-  ( x e. ~H -> ( 1 .h x ) = x )
40 6 7 39 3syl 
 |-  ( x e. ( A \ B ) -> ( 1 .h x ) = x )
41 35 38 40 3eqtr3d 
 |-  ( x e. ( A \ B ) -> ( ( normh ` x ) .h ( ( 1 / ( normh ` x ) ) .h x ) ) = x )
42 41 eleq1d 
 |-  ( x e. ( A \ B ) -> ( ( ( normh ` x ) .h ( ( 1 / ( normh ` x ) ) .h x ) ) e. B <-> x e. B ) )
43 33 42 sylibd 
 |-  ( x e. ( A \ B ) -> ( ( ( 1 / ( normh ` x ) ) .h x ) e. B -> x e. B ) )
44 43 con3d 
 |-  ( x e. ( A \ B ) -> ( -. x e. B -> -. ( ( 1 / ( normh ` x ) ) .h x ) e. B ) )
45 27 44 anim12d 
 |-  ( x e. ( A \ B ) -> ( ( x e. A /\ -. x e. B ) -> ( ( ( 1 / ( normh ` x ) ) .h x ) e. A /\ -. ( ( 1 / ( normh ` x ) ) .h x ) e. B ) ) )
46 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
47 eldif 
 |-  ( ( ( 1 / ( normh ` x ) ) .h x ) e. ( A \ B ) <-> ( ( ( 1 / ( normh ` x ) ) .h x ) e. A /\ -. ( ( 1 / ( normh ` x ) ) .h x ) e. B ) )
48 45 46 47 3imtr4g 
 |-  ( x e. ( A \ B ) -> ( x e. ( A \ B ) -> ( ( 1 / ( normh ` x ) ) .h x ) e. ( A \ B ) ) )
49 48 pm2.43i 
 |-  ( x e. ( A \ B ) -> ( ( 1 / ( normh ` x ) ) .h x ) e. ( A \ B ) )
50 norm-iii 
 |-  ( ( ( 1 / ( normh ` x ) ) e. CC /\ x e. ~H ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) = ( ( abs ` ( 1 / ( normh ` x ) ) ) x. ( normh ` x ) ) )
51 22 36 50 syl2anc 
 |-  ( x e. ( A \ B ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) = ( ( abs ` ( 1 / ( normh ` x ) ) ) x. ( normh ` x ) ) )
52 15 necon2ai 
 |-  ( x e. ( A \ B ) -> x =/= 0h )
53 normgt0 
 |-  ( x e. ~H -> ( x =/= 0h <-> 0 < ( normh ` x ) ) )
54 6 7 53 3syl 
 |-  ( x e. ( A \ B ) -> ( x =/= 0h <-> 0 < ( normh ` x ) ) )
55 52 54 mpbid 
 |-  ( x e. ( A \ B ) -> 0 < ( normh ` x ) )
56 1re 
 |-  1 e. RR
57 0le1 
 |-  0 <_ 1
58 divge0 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( normh ` x ) e. RR /\ 0 < ( normh ` x ) ) ) -> 0 <_ ( 1 / ( normh ` x ) ) )
59 56 57 58 mpanl12 
 |-  ( ( ( normh ` x ) e. RR /\ 0 < ( normh ` x ) ) -> 0 <_ ( 1 / ( normh ` x ) ) )
60 9 55 59 syl2anc 
 |-  ( x e. ( A \ B ) -> 0 <_ ( 1 / ( normh ` x ) ) )
61 21 60 absidd 
 |-  ( x e. ( A \ B ) -> ( abs ` ( 1 / ( normh ` x ) ) ) = ( 1 / ( normh ` x ) ) )
62 61 oveq1d 
 |-  ( x e. ( A \ B ) -> ( ( abs ` ( 1 / ( normh ` x ) ) ) x. ( normh ` x ) ) = ( ( 1 / ( normh ` x ) ) x. ( normh ` x ) ) )
63 28 20 recid2d 
 |-  ( x e. ( A \ B ) -> ( ( 1 / ( normh ` x ) ) x. ( normh ` x ) ) = 1 )
64 51 62 63 3eqtrd 
 |-  ( x e. ( A \ B ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) = 1 )
65 fveqeq2 
 |-  ( u = ( ( 1 / ( normh ` x ) ) .h x ) -> ( ( normh ` u ) = 1 <-> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) = 1 ) )
66 65 rspcev 
 |-  ( ( ( ( 1 / ( normh ` x ) ) .h x ) e. ( A \ B ) /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) = 1 ) -> E. u e. ( A \ B ) ( normh ` u ) = 1 )
67 49 64 66 syl2anc 
 |-  ( x e. ( A \ B ) -> E. u e. ( A \ B ) ( normh ` u ) = 1 )
68 67 exlimiv 
 |-  ( E. x x e. ( A \ B ) -> E. u e. ( A \ B ) ( normh ` u ) = 1 )
69 5 68 sylbi 
 |-  ( -. A C_ B -> E. u e. ( A \ B ) ( normh ` u ) = 1 )