Theorem jplem2

Description: Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001) (New usage is discouraged.)

	Ref	Expression
Hypotheses	jp.1	|- S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
	jp.2	|- A e. CH
Assertion	jplem2	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. A <-> ( S ` A ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		jp.1	|- S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
2		jp.2	|- A e. CH
3	2	jplem1	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. A <-> ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = 1 ) )
4	1	strlem2	|- ( A e. CH -> ( S ` A ) = ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) )
5	2 4	ax-mp	|- ( S ` A ) = ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 )
6	5	eqeq1i	|- ( ( S ` A ) = 1 <-> ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = 1 )
7	3 6	bitr4di	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. A <-> ( S ` A ) = 1 ) )