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⁡u2
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⁡u2
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⁡u2
6 4 5 ax-mp ⊢S⁡B=normℎ⁡projℎ⁡B⁡u2
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⁡u2<12
26 23 24 25 mpanr12 ⊢normℎ⁡projℎ⁡B⁡u∈ℝ∧0≤normℎ⁡projℎ⁡B⁡u→normℎ⁡projℎ⁡B⁡u<1↔normℎ⁡projℎ⁡B⁡u2<12
27 20 22 26 syl2anc ⊢u∈ℋ→normℎ⁡projℎ⁡B⁡u<1↔normℎ⁡projℎ⁡B⁡u2<12
28 17 8 27 3syl ⊢u∈A∖B→normℎ⁡projℎ⁡B⁡u<1↔normℎ⁡projℎ⁡B⁡u2<12
29 28 adantr ⊢u∈A∖B∧normℎ⁡u=1→normℎ⁡projℎ⁡B⁡u<1↔normℎ⁡projℎ⁡B⁡u2<12
30 16 29 mpbid ⊢u∈A∖B∧normℎ⁡u=1→normℎ⁡projℎ⁡B⁡u2<12
31 6 30 eqbrtrid ⊢u∈A∖B∧normℎ⁡u=1→S⁡B<12
32 sq1 ⊢12=1
33 31 32 breqtrdi ⊢u∈A∖B∧normℎ⁡u=1→S⁡B<1
34 2 33 sylbi ⊢φ→S⁡B<1