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 S = x C norm proj x u 2
strlem3.2 φ u A B norm u = 1
strlem3.3 A C
strlem3.4 B C
Assertion strlem4 φ S A = 1

Proof

Step Hyp Ref Expression
1 strlem3.1 S = x C norm proj x u 2
2 strlem3.2 φ u A B norm u = 1
3 strlem3.3 A C
4 strlem3.4 B C
5 1 strlem2 A C S A = norm proj A u 2
6 3 5 ax-mp S A = norm proj A u 2
7 eldifi u A B u A
8 pjid A C u A proj A u = u
9 3 8 mpan u A proj A u = u
10 9 fveq2d u A norm proj A u = norm u
11 eqeq2 norm u = 1 norm proj A u = norm u norm proj A u = 1
12 10 11 syl5ib norm u = 1 u A norm proj A u = 1
13 7 12 mpan9 u A B norm u = 1 norm proj A u = 1
14 2 13 sylbi φ norm proj A u = 1
15 14 oveq1d φ norm proj A u 2 = 1 2
16 sq1 1 2 = 1
17 15 16 eqtrdi φ norm proj A u 2 = 1
18 6 17 syl5eq φ S A = 1