Theorem hstrlem6

Description: Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hstrlem3.1	|- S = ( x e. CH |-> ( ( projh ` x ) ` u ) )
	hstrlem3.2	|- ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) )
	hstrlem3.3	|- A e. CH
	hstrlem3.4	|- B e. CH
Assertion	hstrlem6	|- ( ph -> -. ( ( normh ` ( S ` A ) ) = 1 -> ( normh ` ( S ` B ) ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		hstrlem3.1	|- S = ( x e. CH |-> ( ( projh ` x ) ` u ) )
2		hstrlem3.2	|- ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) )
3		hstrlem3.3	|- A e. CH
4		hstrlem3.4	|- B e. CH
5	1 2 3 4	hstrlem4	|- ( ph -> ( normh ` ( S ` A ) ) = 1 )
6	1 2 3 4	hstrlem3	|- ( ph -> S e. CHStates )
7		hstcl	|- ( ( S e. CHStates /\ B e. CH ) -> ( S ` B ) e. ~H )
8	6 4 7	sylancl	|- ( ph -> ( S ` B ) e. ~H )
9		normcl	|- ( ( S ` B ) e. ~H -> ( normh ` ( S ` B ) ) e. RR )
10	8 9	syl	|- ( ph -> ( normh ` ( S ` B ) ) e. RR )
11	1 2 3 4	hstrlem5	|- ( ph -> ( normh ` ( S ` B ) ) < 1 )
12	10 11	ltned	|- ( ph -> ( normh ` ( S ` B ) ) =/= 1 )
13	12	neneqd	|- ( ph -> -. ( normh ` ( S ` B ) ) = 1 )
14	5 13	jcnd	|- ( ph -> -. ( ( normh ` ( S ` A ) ) = 1 -> ( normh ` ( S ` B ) ) = 1 ) )