# 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}\in {\mathbf{C}}_{ℋ}$
strlem1.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion strlem1 ${⊢}¬{A}\subseteq {B}\to \exists {u}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({u}\right)=1$

### Proof

Step Hyp Ref Expression
1 strlem1.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 strlem1.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 neq0 ${⊢}¬{A}\setminus {B}=\varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left({A}\setminus {B}\right)$
4 ssdif0 ${⊢}{A}\subseteq {B}↔{A}\setminus {B}=\varnothing$
5 3 4 xchnxbir ${⊢}¬{A}\subseteq {B}↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left({A}\setminus {B}\right)$
6 eldifi ${⊢}{x}\in \left({A}\setminus {B}\right)\to {x}\in {A}$
7 1 cheli ${⊢}{x}\in {A}\to {x}\in ℋ$
8 normcl ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({x}\right)\in ℝ$
9 6 7 8 3syl ${⊢}{x}\in \left({A}\setminus {B}\right)\to {norm}_{ℎ}\left({x}\right)\in ℝ$
10 ch0 ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to {0}_{ℎ}\in {B}$
11 2 10 ax-mp ${⊢}{0}_{ℎ}\in {B}$
12 eldifn ${⊢}{0}_{ℎ}\in \left({A}\setminus {B}\right)\to ¬{0}_{ℎ}\in {B}$
13 11 12 mt2 ${⊢}¬{0}_{ℎ}\in \left({A}\setminus {B}\right)$
14 eleq1 ${⊢}{x}={0}_{ℎ}\to \left({x}\in \left({A}\setminus {B}\right)↔{0}_{ℎ}\in \left({A}\setminus {B}\right)\right)$
15 13 14 mtbiri ${⊢}{x}={0}_{ℎ}\to ¬{x}\in \left({A}\setminus {B}\right)$
16 15 con2i ${⊢}{x}\in \left({A}\setminus {B}\right)\to ¬{x}={0}_{ℎ}$
17 norm-i ${⊢}{x}\in ℋ\to \left({norm}_{ℎ}\left({x}\right)=0↔{x}={0}_{ℎ}\right)$
18 6 7 17 3syl ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left({norm}_{ℎ}\left({x}\right)=0↔{x}={0}_{ℎ}\right)$
19 16 18 mtbird ${⊢}{x}\in \left({A}\setminus {B}\right)\to ¬{norm}_{ℎ}\left({x}\right)=0$
20 19 neqned ${⊢}{x}\in \left({A}\setminus {B}\right)\to {norm}_{ℎ}\left({x}\right)\ne 0$
21 9 20 rereccld ${⊢}{x}\in \left({A}\setminus {B}\right)\to \frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℝ$
22 21 recnd ${⊢}{x}\in \left({A}\setminus {B}\right)\to \frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ$
23 1 chshii ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
24 shmulcl ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge \frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ\wedge {x}\in {A}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {A}$
25 23 24 mp3an1 ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ\wedge {x}\in {A}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {A}$
26 25 ex ${⊢}\frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ\to \left({x}\in {A}\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {A}\right)$
27 22 26 syl ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left({x}\in {A}\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {A}\right)$
28 9 recnd ${⊢}{x}\in \left({A}\setminus {B}\right)\to {norm}_{ℎ}\left({x}\right)\in ℂ$
29 2 chshii ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
30 shmulcl ${⊢}\left({B}\in {\mathbf{S}}_{ℋ}\wedge {norm}_{ℎ}\left({x}\right)\in ℂ\wedge \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {B}\right)\to {norm}_{ℎ}\left({x}\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\in {B}$
31 29 30 mp3an1 ${⊢}\left({norm}_{ℎ}\left({x}\right)\in ℂ\wedge \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {B}\right)\to {norm}_{ℎ}\left({x}\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\in {B}$
32 31 ex ${⊢}{norm}_{ℎ}\left({x}\right)\in ℂ\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {B}\to {norm}_{ℎ}\left({x}\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\in {B}\right)$
33 28 32 syl ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {B}\to {norm}_{ℎ}\left({x}\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\in {B}\right)$
34 28 20 recidd ${⊢}{x}\in \left({A}\setminus {B}\right)\to {norm}_{ℎ}\left({x}\right)\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right)=1$
35 34 oveq1d ${⊢}{x}\in \left({A}\setminus {B}\right)\to {norm}_{ℎ}\left({x}\right)\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}=1{\cdot }_{ℎ}{x}$
36 6 7 syl ${⊢}{x}\in \left({A}\setminus {B}\right)\to {x}\in ℋ$
37 ax-hvmulass ${⊢}\left({norm}_{ℎ}\left({x}\right)\in ℂ\wedge \frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left({x}\right)\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}={norm}_{ℎ}\left({x}\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)$
38 28 22 36 37 syl3anc ${⊢}{x}\in \left({A}\setminus {B}\right)\to {norm}_{ℎ}\left({x}\right)\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}={norm}_{ℎ}\left({x}\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)$
39 ax-hvmulid ${⊢}{x}\in ℋ\to 1{\cdot }_{ℎ}{x}={x}$
40 6 7 39 3syl ${⊢}{x}\in \left({A}\setminus {B}\right)\to 1{\cdot }_{ℎ}{x}={x}$
41 35 38 40 3eqtr3d ${⊢}{x}\in \left({A}\setminus {B}\right)\to {norm}_{ℎ}\left({x}\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)={x}$
42 41 eleq1d ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left({norm}_{ℎ}\left({x}\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\in {B}↔{x}\in {B}\right)$
43 33 42 sylibd ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {B}\to {x}\in {B}\right)$
44 43 con3d ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left(¬{x}\in {B}\to ¬\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {B}\right)$
45 27 44 anim12d ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left(\left({x}\in {A}\wedge ¬{x}\in {B}\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {A}\wedge ¬\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {B}\right)\right)$
46 eldif ${⊢}{x}\in \left({A}\setminus {B}\right)↔\left({x}\in {A}\wedge ¬{x}\in {B}\right)$
47 eldif ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in \left({A}\setminus {B}\right)↔\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {A}\wedge ¬\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in {B}\right)$
48 45 46 47 3imtr4g ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left({x}\in \left({A}\setminus {B}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in \left({A}\setminus {B}\right)\right)$
49 48 pm2.43i ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in \left({A}\setminus {B}\right)$
50 norm-iii ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=\left|\frac{1}{{norm}_{ℎ}\left({x}\right)}\right|{norm}_{ℎ}\left({x}\right)$
51 22 36 50 syl2anc ${⊢}{x}\in \left({A}\setminus {B}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=\left|\frac{1}{{norm}_{ℎ}\left({x}\right)}\right|{norm}_{ℎ}\left({x}\right)$
52 15 necon2ai ${⊢}{x}\in \left({A}\setminus {B}\right)\to {x}\ne {0}_{ℎ}$
53 normgt0 ${⊢}{x}\in ℋ\to \left({x}\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left({x}\right)\right)$
54 6 7 53 3syl ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left({x}\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left({x}\right)\right)$
55 52 54 mpbid ${⊢}{x}\in \left({A}\setminus {B}\right)\to 0<{norm}_{ℎ}\left({x}\right)$
56 1re ${⊢}1\in ℝ$
57 0le1 ${⊢}0\le 1$
58 divge0 ${⊢}\left(\left(1\in ℝ\wedge 0\le 1\right)\wedge \left({norm}_{ℎ}\left({x}\right)\in ℝ\wedge 0<{norm}_{ℎ}\left({x}\right)\right)\right)\to 0\le \frac{1}{{norm}_{ℎ}\left({x}\right)}$
59 56 57 58 mpanl12 ${⊢}\left({norm}_{ℎ}\left({x}\right)\in ℝ\wedge 0<{norm}_{ℎ}\left({x}\right)\right)\to 0\le \frac{1}{{norm}_{ℎ}\left({x}\right)}$
60 9 55 59 syl2anc ${⊢}{x}\in \left({A}\setminus {B}\right)\to 0\le \frac{1}{{norm}_{ℎ}\left({x}\right)}$
61 21 60 absidd ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left|\frac{1}{{norm}_{ℎ}\left({x}\right)}\right|=\frac{1}{{norm}_{ℎ}\left({x}\right)}$
62 61 oveq1d ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left|\frac{1}{{norm}_{ℎ}\left({x}\right)}\right|{norm}_{ℎ}\left({x}\right)=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){norm}_{ℎ}\left({x}\right)$
63 28 20 recid2d ${⊢}{x}\in \left({A}\setminus {B}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){norm}_{ℎ}\left({x}\right)=1$
64 51 62 63 3eqtrd ${⊢}{x}\in \left({A}\setminus {B}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=1$
65 fveqeq2 ${⊢}{u}=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\to \left({norm}_{ℎ}\left({u}\right)=1↔{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=1\right)$
66 65 rspcev ${⊢}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in \left({A}\setminus {B}\right)\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=1\right)\to \exists {u}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({u}\right)=1$
67 49 64 66 syl2anc ${⊢}{x}\in \left({A}\setminus {B}\right)\to \exists {u}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({u}\right)=1$
68 67 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left({A}\setminus {B}\right)\to \exists {u}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({u}\right)=1$
69 5 68 sylbi ${⊢}¬{A}\subseteq {B}\to \exists {u}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({u}\right)=1$