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 e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
	strlem3.2	|- ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) )
	strlem3.3	|- A e. CH
	strlem3.4	|- B e. CH
Assertion	strlem6	|- ( ph -> -. ( ( S ` A ) = 1 -> ( S ` B ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		strlem3.1	|- S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
2		strlem3.2	|- ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) )
3		strlem3.3	|- A e. CH
4		strlem3.4	|- B e. CH
5	1 2 3 4	strlem4	|- ( ph -> ( S ` A ) = 1 )
6	1 2 3 4	strlem3	|- ( ph -> S e. States )
7		stcl	|- ( S e. States -> ( B e. CH -> ( S ` B ) e. RR ) )
8	6 4 7	mpisyl	|- ( ph -> ( S ` B ) e. RR )
9	1 2 3 4	strlem5	|- ( ph -> ( S ` B ) < 1 )
10	8 9	ltned	|- ( ph -> ( S ` B ) =/= 1 )
11	10	neneqd	|- ( ph -> -. ( S ` B ) = 1 )
12	5 11	jcnd	|- ( ph -> -. ( ( S ` A ) = 1 -> ( S ` B ) = 1 ) )