Theorem jpi

Description: The function S , that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a Jauch-Piron state. Remark in Mayet p. 370. (See strlem3a for the proof that S is a state.) (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
	jp.3	|- B e. CH
Assertion	jpi	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( ( ( S ` A ) = 1 /\ ( S ` B ) = 1 ) <-> ( S ` ( A i^i B ) ) = 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		jp.3	|- B e. CH
4		elin	|- ( u e. ( A i^i B ) <-> ( u e. A /\ u e. B ) )
5	1 2	jplem2	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. A <-> ( S ` A ) = 1 ) )
6	1 3	jplem2	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. B <-> ( S ` B ) = 1 ) )
7	5 6	anbi12d	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( ( u e. A /\ u e. B ) <-> ( ( S ` A ) = 1 /\ ( S ` B ) = 1 ) ) )
8	4 7	syl5bb	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. ( A i^i B ) <-> ( ( S ` A ) = 1 /\ ( S ` B ) = 1 ) ) )
9	2 3	chincli	|- ( A i^i B ) e. CH
10	1 9	jplem2	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. ( A i^i B ) <-> ( S ` ( A i^i B ) ) = 1 ) )
11	8 10	bitr3d	|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( ( ( S ` A ) = 1 /\ ( S ` B ) = 1 ) <-> ( S ` ( A i^i B ) ) = 1 ) )