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 imbitrid ⊢ ( ( 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 )