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

Proof

Step Hyp Ref Expression
1 hstrlem3.1 𝑆 = ( 𝑥C ↦ ( ( proj𝑥 ) ‘ 𝑢 ) )
2 hstrlem3.2 ( 𝜑 ↔ ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) )
3 hstrlem3.3 𝐴C
4 hstrlem3.4 𝐵C
5 1 hstrlem2 ( 𝐵C → ( 𝑆𝐵 ) = ( ( proj𝐵 ) ‘ 𝑢 ) )
6 5 fveq2d ( 𝐵C → ( norm ‘ ( 𝑆𝐵 ) ) = ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) )
7 4 6 ax-mp ( norm ‘ ( 𝑆𝐵 ) ) = ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) )
8 eldif ( 𝑢 ∈ ( 𝐴𝐵 ) ↔ ( 𝑢𝐴 ∧ ¬ 𝑢𝐵 ) )
9 3 cheli ( 𝑢𝐴𝑢 ∈ ℋ )
10 pjnel ( ( 𝐵C𝑢 ∈ ℋ ) → ( ¬ 𝑢𝐵 ↔ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) ) )
11 4 10 mpan ( 𝑢 ∈ ℋ → ( ¬ 𝑢𝐵 ↔ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) ) )
12 11 biimpa ( ( 𝑢 ∈ ℋ ∧ ¬ 𝑢𝐵 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) )
13 9 12 sylan ( ( 𝑢𝐴 ∧ ¬ 𝑢𝐵 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) )
14 8 13 sylbi ( 𝑢 ∈ ( 𝐴𝐵 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) )
15 breq2 ( ( norm𝑢 ) = 1 → ( ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < ( norm𝑢 ) ↔ ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 ) )
16 14 15 syl5ib ( ( norm𝑢 ) = 1 → ( 𝑢 ∈ ( 𝐴𝐵 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 ) )
17 16 impcom ( ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) → ( norm ‘ ( ( proj𝐵 ) ‘ 𝑢 ) ) < 1 )
18 7 17 eqbrtrid ( ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) → ( norm ‘ ( 𝑆𝐵 ) ) < 1 )
19 2 18 sylbi ( 𝜑 → ( norm ‘ ( 𝑆𝐵 ) ) < 1 )