Theorem hstrlem5

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	hstrlem5	|- ( ph -> ( 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	hstrlem2	|- ( B e. CH -> ( S ` B ) = ( ( projh ` B ) ` u ) )
6	5	fveq2d	|- ( B e. CH -> ( normh ` ( S ` B ) ) = ( normh ` ( ( projh ` B ) ` u ) ) )
7	4 6	ax-mp	|- ( normh ` ( S ` B ) ) = ( normh ` ( ( projh ` B ) ` u ) )
8		eldif	|- ( u e. ( A \ B ) <-> ( u e. A /\ -. u e. B ) )
9	3	cheli	|- ( u e. A -> u e. ~H )
10		pjnel	|- ( ( B e. CH /\ u e. ~H ) -> ( -. u e. B <-> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) ) )
11	4 10	mpan	|- ( u e. ~H -> ( -. u e. B <-> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) ) )
12	11	biimpa	|- ( ( u e. ~H /\ -. u e. B ) -> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) )
13	9 12	sylan	|- ( ( u e. A /\ -. u e. B ) -> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) )
14	8 13	sylbi	|- ( u e. ( A \ B ) -> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) )
15		breq2	|- ( ( normh ` u ) = 1 -> ( ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) <-> ( normh ` ( ( projh ` B ) ` u ) ) < 1 ) )
16	14 15	imbitrid	|- ( ( normh ` u ) = 1 -> ( u e. ( A \ B ) -> ( normh ` ( ( projh ` B ) ` u ) ) < 1 ) )
17	16	impcom	|- ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( normh ` ( ( projh ` B ) ` u ) ) < 1 )
18	7 17	eqbrtrid	|- ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( normh ` ( S ` B ) ) < 1 )
19	2 18	sylbi	|- ( ph -> ( normh ` ( S ` B ) ) < 1 )