Metamath Proof Explorer


Theorem strlem4

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