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 \in C_{ℋ} ⟼ {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2})$
	jp.2	$⊢ A \in C_{ℋ}$
	jp.3	$⊢ B \in C_{ℋ}$
Assertion	jpi	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to ((S (A) = 1 \land S (B) = 1) \leftrightarrow S (A \cap B) = 1)$

Proof

Step	Hyp	Ref	Expression
1		jp.1	$⊢ S = (x \in C_{ℋ} ⟼ {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2})$
2		jp.2	$⊢ A \in C_{ℋ}$
3		jp.3	$⊢ B \in C_{ℋ}$
4		elin	$⊢ u \in (A \cap B) \leftrightarrow (u \in A \land u \in B)$
5	1 2	jplem2	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to (u \in A \leftrightarrow S (A) = 1)$
6	1 3	jplem2	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to (u \in B \leftrightarrow S (B) = 1)$
7	5 6	anbi12d	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to ((u \in A \land u \in B) \leftrightarrow (S (A) = 1 \land S (B) = 1))$
8	4 7	bitrid	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to (u \in (A \cap B) \leftrightarrow (S (A) = 1 \land S (B) = 1))$
9	2 3	chincli	$⊢ A \cap B \in C_{ℋ}$
10	1 9	jplem2	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to (u \in (A \cap B) \leftrightarrow S (A \cap B) = 1)$
11	8 10	bitr3d	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to ((S (A) = 1 \land S (B) = 1) \leftrightarrow S (A \cap B) = 1)$

Metamath Proof Explorer

Theorem jpi

Proof