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	⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
	jp.2	⊢ 𝐴 ∈ Cℋ
	jp.3	⊢ 𝐵 ∈ Cℋ
Assertion	jpi	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( ( ( 𝑆 ‘ 𝐴 ) = 1 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) ↔ ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		jp.1	⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
2		jp.2	⊢ 𝐴 ∈ Cℋ
3		jp.3	⊢ 𝐵 ∈ Cℋ
4		elin	⊢ ( 𝑢 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) )
5	1 2	jplem2	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ 𝐴 ↔ ( 𝑆 ‘ 𝐴 ) = 1 ) )
6	1 3	jplem2	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ 𝐵 ↔ ( 𝑆 ‘ 𝐵 ) = 1 ) )
7	5 6	anbi12d	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ↔ ( ( 𝑆 ‘ 𝐴 ) = 1 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) ) )
8	4 7	bitrid	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ( 𝑆 ‘ 𝐴 ) = 1 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) ) )
9	2 3	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
10	1 9	jplem2	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 ) )
11	8 10	bitr3d	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( ( ( 𝑆 ‘ 𝐴 ) = 1 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) ↔ ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 ) )