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=xCnormprojxu2
strlem3.2 φuABnormu=1
strlem3.3 AC
strlem3.4 BC
Assertion strlem4 φSA=1

Proof

Step Hyp Ref Expression
1 strlem3.1 S=xCnormprojxu2
2 strlem3.2 φuABnormu=1
3 strlem3.3 AC
4 strlem3.4 BC
5 1 strlem2 ACSA=normprojAu2
6 3 5 ax-mp SA=normprojAu2
7 eldifi uABuA
8 pjid ACuAprojAu=u
9 3 8 mpan uAprojAu=u
10 9 fveq2d uAnormprojAu=normu
11 eqeq2 normu=1normprojAu=normunormprojAu=1
12 10 11 syl5ib normu=1uAnormprojAu=1
13 7 12 mpan9 uABnormu=1normprojAu=1
14 2 13 sylbi φnormprojAu=1
15 14 oveq1d φnormprojAu2=12
16 sq1 12=1
17 15 16 eqtrdi φnormprojAu2=1
18 6 17 eqtrid φSA=1