# 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 ∈ C ℋ$
strlem1.2 $⊢ B ∈ C ℋ$
Assertion strlem1 $⊢ ¬ A ⊆ B → ∃ u ∈ A ∖ B norm ℎ ⁡ u = 1$

### Proof

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