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 ⊢ 𝐴 ∈ Cℋ
strlem1.2 ⊢ 𝐵 ∈ Cℋ
Assertion strlem1 ( ¬ 𝐴 ⊆ 𝐵 → ∃ 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ( normℎ ‘ 𝑢 ) = 1 )

Proof

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