# 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 )`