Metamath Proof Explorer

Theorem hstrlem5

Description: Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hstrlem3.1 ⊢ S = x ∈ C ℋ ⟼ proj ℎ ⁡ x ⁡ u
2 hstrlem3.2 ⊢ φ ↔ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1
3 hstrlem3.3 ⊢ A ∈ C ℋ
4 hstrlem3.4 ⊢ B ∈ C ℋ
5 1 hstrlem2 ⊢ B ∈ C ℋ → S ⁡ B = proj ℎ ⁡ B ⁡ u
6 5 fveq2d ⊢ B ∈ C ℋ → norm ℎ ⁡ S ⁡ B = norm ℎ ⁡ proj ℎ ⁡ B ⁡ u
7 4 6 ax-mp ⊢ norm ℎ ⁡ S ⁡ B = norm ℎ ⁡ proj ℎ ⁡ B ⁡ u
8 eldif ⊢ u ∈ A ∖ B ↔ u ∈ A ∧ ¬ u ∈ B
9 3 cheli ⊢ u ∈ A → u ∈ ℋ
10 pjnel ⊢ B ∈ C ℋ ∧ u ∈ ℋ → ¬ u ∈ B ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
11 4 10 mpan ⊢ u ∈ ℋ → ¬ u ∈ B ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
12 11 biimpa ⊢ u ∈ ℋ ∧ ¬ u ∈ B → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
13 9 12 sylan ⊢ u ∈ A ∧ ¬ u ∈ B → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
14 8 13 sylbi ⊢ u ∈ A ∖ B → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u
15 breq2 ⊢ norm ℎ ⁡ u = 1 → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < norm ℎ ⁡ u ↔ norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1
16 14 15 syl5ib ⊢ norm ℎ ⁡ u = 1 → u ∈ A ∖ B → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1
17 16 impcom ⊢ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1 → norm ℎ ⁡ proj ℎ ⁡ B ⁡ u < 1
18 7 17 eqbrtrid ⊢ u ∈ A ∖ B ∧ norm ℎ ⁡ u = 1 → norm ℎ ⁡ S ⁡ B < 1
19 2 18 sylbi ⊢ φ → norm ℎ ⁡ S ⁡ B < 1