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∖Bnormℎ⁡u=1

Proof

Step Hyp Ref Expression
1 strlem1.1 ⊢A∈Cℋ
2 strlem1.2 ⊢B∈Cℋ
3 neq0 ⊢¬A∖B=∅↔∃xx∈A∖B
4 ssdif0 ⊢A⊆B↔A∖B=∅
5 3 4 xchnxbir ⊢¬A⊆B↔∃xx∈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→1normℎ⁡x∈ℝ
22 21 recnd ⊢x∈A∖B→1normℎ⁡x∈ℂ
23 1 chshii ⊢A∈Sℋ
24 shmulcl ⊢A∈Sℋ∧1normℎ⁡x∈ℂ∧x∈A→1normℎ⁡x⋅ℎx∈A
25 23 24 mp3an1 ⊢1normℎ⁡x∈ℂ∧x∈A→1normℎ⁡x⋅ℎx∈A
26 25 ex ⊢1normℎ⁡x∈ℂ→x∈A→1normℎ⁡x⋅ℎx∈A
27 22 26 syl ⊢x∈A∖B→x∈A→1normℎ⁡x⋅ℎx∈A
28 9 recnd ⊢x∈A∖B→normℎ⁡x∈ℂ
29 2 chshii ⊢B∈Sℋ
30 shmulcl ⊢B∈Sℋ∧normℎ⁡x∈ℂ∧1normℎ⁡x⋅ℎx∈B→normℎ⁡x⋅ℎ1normℎ⁡x⋅ℎx∈B
31 29 30 mp3an1 ⊢normℎ⁡x∈ℂ∧1normℎ⁡x⋅ℎx∈B→normℎ⁡x⋅ℎ1normℎ⁡x⋅ℎx∈B
32 31 ex ⊢normℎ⁡x∈ℂ→1normℎ⁡x⋅ℎx∈B→normℎ⁡x⋅ℎ1normℎ⁡x⋅ℎx∈B
33 28 32 syl ⊢x∈A∖B→1normℎ⁡x⋅ℎx∈B→normℎ⁡x⋅ℎ1normℎ⁡x⋅ℎx∈B
34 28 20 recidd ⊢x∈A∖B→normℎ⁡x⁢1normℎ⁡x=1
35 34 oveq1d ⊢x∈A∖B→normℎ⁡x⁢1normℎ⁡x⋅ℎx=1⋅ℎx
36 6 7 syl ⊢x∈A∖B→x∈ℋ
37 ax-hvmulass ⊢normℎ⁡x∈ℂ∧1normℎ⁡x∈ℂ∧x∈ℋ→normℎ⁡x⁢1normℎ⁡x⋅ℎx=normℎ⁡x⋅ℎ1normℎ⁡x⋅ℎx
38 28 22 36 37 syl3anc ⊢x∈A∖B→normℎ⁡x⁢1normℎ⁡x⋅ℎx=normℎ⁡x⋅ℎ1normℎ⁡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⋅ℎ1normℎ⁡x⋅ℎx=x
42 41 eleq1d ⊢x∈A∖B→normℎ⁡x⋅ℎ1normℎ⁡x⋅ℎx∈B↔x∈B
43 33 42 sylibd ⊢x∈A∖B→1normℎ⁡x⋅ℎx∈B→x∈B
44 43 con3d ⊢x∈A∖B→¬x∈B→¬1normℎ⁡x⋅ℎx∈B
45 27 44 anim12d ⊢x∈A∖B→x∈A∧¬x∈B→1normℎ⁡x⋅ℎx∈A∧¬1normℎ⁡x⋅ℎx∈B
46 eldif ⊢x∈A∖B↔x∈A∧¬x∈B
47 eldif ⊢1normℎ⁡x⋅ℎx∈A∖B↔1normℎ⁡x⋅ℎx∈A∧¬1normℎ⁡x⋅ℎx∈B
48 45 46 47 3imtr4g ⊢x∈A∖B→x∈A∖B→1normℎ⁡x⋅ℎx∈A∖B
49 48 pm2.43i ⊢x∈A∖B→1normℎ⁡x⋅ℎx∈A∖B
50 norm-iii ⊢1normℎ⁡x∈ℂ∧x∈ℋ→normℎ⁡1normℎ⁡x⋅ℎx=1normℎ⁡x⁢normℎ⁡x
51 22 36 50 syl2anc ⊢x∈A∖B→normℎ⁡1normℎ⁡x⋅ℎx=1normℎ⁡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≤1normℎ⁡x
59 56 57 58 mpanl12 ⊢normℎ⁡x∈ℝ∧0<normℎ⁡x→0≤1normℎ⁡x
60 9 55 59 syl2anc ⊢x∈A∖B→0≤1normℎ⁡x
61 21 60 absidd ⊢x∈A∖B→1normℎ⁡x=1normℎ⁡x
62 61 oveq1d ⊢x∈A∖B→1normℎ⁡x⁢normℎ⁡x=1normℎ⁡x⁢normℎ⁡x
63 28 20 recid2d ⊢x∈A∖B→1normℎ⁡x⁢normℎ⁡x=1
64 51 62 63 3eqtrd ⊢x∈A∖B→normℎ⁡1normℎ⁡x⋅ℎx=1
65 fveqeq2 ⊢u=1normℎ⁡x⋅ℎx→normℎ⁡u=1↔normℎ⁡1normℎ⁡x⋅ℎx=1
66 65 rspcev ⊢1normℎ⁡x⋅ℎx∈A∖B∧normℎ⁡1normℎ⁡x⋅ℎx=1→∃u∈A∖Bnormℎ⁡u=1
67 49 64 66 syl2anc ⊢x∈A∖B→∃u∈A∖Bnormℎ⁡u=1
68 67 exlimiv ⊢∃xx∈A∖B→∃u∈A∖Bnormℎ⁡u=1
69 5 68 sylbi ⊢¬A⊆B→∃u∈A∖Bnormℎ⁡u=1