Metamath Proof Explorer

Theorem strlem5

Description: Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses strlem3.1 ⊢ S = x ∈ C ℋ ⟼ norm ℎ ⁡ proj ℎ ⁡ x ⁡ u 2
strlem3.2 ⊢ φ ↔ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1
strlem3.3 ⊢ A ∈ C ℋ
strlem3.4 ⊢ B ∈ C ℋ
Assertion strlem5 ⊢ φ → S ⁡ B < 1

Proof

Step Hyp Ref Expression
1 strlem3.1 ⊢ S = x ∈ C ℋ ⟼ norm ℎ ⁡ proj ℎ ⁡ x ⁡ u 2
2 strlem3.2 ⊢ φ ↔ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1
3 strlem3.3 ⊢ A ∈ C ℋ
4 strlem3.4 ⊢ B ∈ C ℋ
5 1 strlem2 ⊢ B ∈ C ℋ → S ⁡ B = norm ℎ ⁡ proj ℎ ⁡ B ⁡ u 2
6 4 5 ax-mp ⊢ S ⁡ B = norm ℎ ⁡ proj ℎ ⁡ B ⁡ u 2
7 eldif ⊢ u ∈ A ∖ B ↔ u ∈ A ∧ ¬ u ∈ B
8 3 cheli ⊢ u ∈ A → u ∈ ℋ
9 pjnel ⊢ B ∈ C ℋ ∧ u ∈ ℋ → ¬ u ∈ B ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
10 4 9 mpan ⊢ u ∈ ℋ → ¬ u ∈ B ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
11 10 biimpa ⊢ u ∈ ℋ ∧ ¬ u ∈ B → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
12 8 11 sylan ⊢ u ∈ A ∧ ¬ u ∈ B → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
13 7 12 sylbi ⊢ u ∈ A ∖ B → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
14 breq2 ⊢ norm ℎ ⁡ u = 1 → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1
15 13 14 imbitrid ⊢ norm ℎ ⁡ u = 1 → u ∈ A ∖ B → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1
16 15 impcom ⊢ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1 → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1
17 eldifi ⊢ u ∈ A ∖ B → u ∈ A
18 4 pjhcli ⊢ u ∈ ℋ → proj ℎ ⁡ B ⁡ u ∈ ℋ
19 normcl ⊢ proj ℎ ⁡ B ⁡ u ∈ ℋ → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u ∈ ℝ
20 18 19 syl ⊢ u ∈ ℋ → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u ∈ ℝ
21 normge0 ⊢ proj ℎ ⁡ B ⁡ u ∈ ℋ → 0 ≤ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u
22 18 21 syl ⊢ u ∈ ℋ → 0 ≤ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u
23 1re ⊢ 1 ∈ ℝ
24 0le1 ⊢ 0 ≤ 1
25 lt2sq ⊢ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u ∧ 1 ∈ ℝ ∧ 0 ≤ 1 → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1 ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u 2 < 1 2
26 23 24 25 mpanr12 ⊢ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1 ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u 2 < 1 2
27 20 22 26 syl2anc ⊢ u ∈ ℋ → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1 ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u 2 < 1 2
28 17 8 27 3syl ⊢ u ∈ A ∖ B → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1 ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u 2 < 1 2
29 28 adantr ⊢ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1 → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1 ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u 2 < 1 2
30 16 29 mpbid ⊢ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1 → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u 2 < 1 2
31 6 30 eqbrtrid ⊢ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1 → S ⁡ B < 1 2
32 sq1 ⊢ 1 2 = 1
33 31 32 breqtrdi ⊢ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1 → S ⁡ B < 1
34 2 33 sylbi ⊢ φ → S ⁡ B < 1