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 𝑆 = ( 𝑥C ↦ ( ( norm ‘ ( ( proj𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
strlem3.2 ( 𝜑 ↔ ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) )
strlem3.3 𝐴C
strlem3.4 𝐵C
Assertion strlem5 ( 𝜑 → ( 𝑆𝐵 ) < 1 )

Proof

Step Hyp Ref Expression
1 strlem3.1 𝑆 = ( 𝑥C ↦ ( ( norm ‘ ( ( proj𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
2 strlem3.2 ( 𝜑 ↔ ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) )
3 strlem3.3 𝐴C
4 strlem3.4 𝐵C
5 1 strlem2 ( 𝐵C → ( 𝑆𝐵 ) = ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ↑ 2 ) )
6 4 5 ax-mp ( 𝑆𝐵 ) = ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ↑ 2 )
7 eldif ( 𝑢 ∈ ( 𝐴𝐵 ) ↔ ( 𝑢𝐴 ∧ ¬ 𝑢𝐵 ) )
8 3 cheli ( 𝑢𝐴𝑢 ∈ ℋ )
9 pjnel ( ( 𝐵C𝑢 ∈ ℋ ) → ( ¬ 𝑢𝐵 ↔ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) ) )
10 4 9 mpan ( 𝑢 ∈ ℋ → ( ¬ 𝑢𝐵 ↔ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) ) )
11 10 biimpa ( ( 𝑢 ∈ ℋ ∧ ¬ 𝑢𝐵 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) )
12 8 11 sylan ( ( 𝑢𝐴 ∧ ¬ 𝑢𝐵 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) )
13 7 12 sylbi ( 𝑢 ∈ ( 𝐴𝐵 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) )
14 breq2 ( ( norm𝑢 ) = 1 → ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) ↔ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 ) )
15 13 14 syl5ib ( ( norm𝑢 ) = 1 → ( 𝑢 ∈ ( 𝐴𝐵 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 ) )
16 15 impcom ( ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 )
17 eldifi ( 𝑢 ∈ ( 𝐴𝐵 ) → 𝑢𝐴 )
18 4 pjhcli ( 𝑢 ∈ ℋ → ( ( proj𝐵 ) ‘ 𝑢 ) ∈ ℋ )
19 normcl ( ( ( proj𝐵 ) ‘ 𝑢 ) ∈ ℋ → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ∈ ℝ )
20 18 19 syl ( 𝑢 ∈ ℋ → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ∈ ℝ )
21 normge0 ( ( ( proj𝐵 ) ‘ 𝑢 ) ∈ ℋ → 0 ≤ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) )
22 18 21 syl ( 𝑢 ∈ ℋ → 0 ≤ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) )
23 1re 1 ∈ ℝ
24 0le1 0 ≤ 1
25 lt2sq ( ( ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ∈ ℝ ∧ 0 ≤ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 ↔ ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ↑ 2 ) < ( 1 ↑ 2 ) ) )
26 23 24 25 mpanr12 ( ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ∈ ℝ ∧ 0 ≤ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ) → ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 ↔ ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ↑ 2 ) < ( 1 ↑ 2 ) ) )
27 20 22 26 syl2anc ( 𝑢 ∈ ℋ → ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 ↔ ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ↑ 2 ) < ( 1 ↑ 2 ) ) )
28 17 8 27 3syl ( 𝑢 ∈ ( 𝐴𝐵 ) → ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 ↔ ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ↑ 2 ) < ( 1 ↑ 2 ) ) )
29 28 adantr ( ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) → ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 ↔ ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ↑ 2 ) < ( 1 ↑ 2 ) ) )
30 16 29 mpbid ( ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) → ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) ↑ 2 ) < ( 1 ↑ 2 ) )
31 6 30 eqbrtrid ( ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) → ( 𝑆𝐵 ) < ( 1 ↑ 2 ) )
32 sq1 ( 1 ↑ 2 ) = 1
33 31 32 breqtrdi ( ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) → ( 𝑆𝐵 ) < 1 )
34 2 33 sylbi ( 𝜑 → ( 𝑆𝐵 ) < 1 )