Metamath Proof Explorer


Theorem hstrlem4

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 hstrlem4 ( 𝜑 → ( 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 3 5 ax-mp ( 𝑆𝐴 ) = ( ( proj𝐴 ) ‘ 𝑢 )
7 6 fveq2i ( norm ‘ ( 𝑆𝐴 ) ) = ( norm ‘ ( ( proj𝐴 ) ‘ 𝑢 ) )
8 eldifi ( 𝑢 ∈ ( 𝐴𝐵 ) → 𝑢𝐴 )
9 pjid ( ( 𝐴C𝑢𝐴 ) → ( ( proj𝐴 ) ‘ 𝑢 ) = 𝑢 )
10 3 9 mpan ( 𝑢𝐴 → ( ( proj𝐴 ) ‘ 𝑢 ) = 𝑢 )
11 10 fveq2d ( 𝑢𝐴 → ( norm ‘ ( ( proj𝐴 ) ‘ 𝑢 ) ) = ( norm𝑢 ) )
12 eqeq2 ( ( norm𝑢 ) = 1 → ( ( norm ‘ ( ( proj𝐴 ) ‘ 𝑢 ) ) = ( norm𝑢 ) ↔ ( norm ‘ ( ( proj𝐴 ) ‘ 𝑢 ) ) = 1 ) )
13 11 12 syl5ib ( ( norm𝑢 ) = 1 → ( 𝑢𝐴 → ( norm ‘ ( ( proj𝐴 ) ‘ 𝑢 ) ) = 1 ) )
14 8 13 mpan9 ( ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) → ( norm ‘ ( ( proj𝐴 ) ‘ 𝑢 ) ) = 1 )
15 2 14 sylbi ( 𝜑 → ( norm ‘ ( ( proj𝐴 ) ‘ 𝑢 ) ) = 1 )
16 7 15 syl5eq ( 𝜑 → ( norm ‘ ( 𝑆𝐴 ) ) = 1 )