Metamath Proof Explorer


Theorem strlem6

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 strlem6 φ ¬ S A = 1 S B = 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 2 3 4 strlem4 φ S A = 1
6 1 2 3 4 strlem3 φ S States
7 stcl S States B C S B
8 6 4 7 mpisyl φ S B
9 1 2 3 4 strlem5 φ S B < 1
10 8 9 ltned φ S B 1
11 10 neneqd φ ¬ S B = 1
12 5 11 jcnd φ ¬ S A = 1 S B = 1