Metamath Proof Explorer

Theorem hstoc

Description: Sum of a Hilbert-space-valued state of a lattice element and its orthocomplement. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hstoc	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A) +_{ℎ} S (⊥ (A)) = S (ℋ)$

Proof

Step	Hyp	Ref	Expression
1		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
2	1	adantl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to ⊥ (A) \in C_{ℋ}$
3		chsh	$⊢ A \in C_{ℋ} \to A \in S_{ℋ}$
4		shococss	$⊢ A \in S_{ℋ} \to A \subseteq ⊥ (⊥ (A))$
5	3 4	syl	$⊢ A \in C_{ℋ} \to A \subseteq ⊥ (⊥ (A))$
6	5	adantl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to A \subseteq ⊥ (⊥ (A))$
7	2 6	jca	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to (⊥ (A) \in C_{ℋ} \land A \subseteq ⊥ (⊥ (A)))$
8		hstosum	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (⊥ (A) \in C_{ℋ} \land A \subseteq ⊥ (⊥ (A)))) \to S (A \lor_{ℋ} ⊥ (A)) = S (A) +_{ℎ} S (⊥ (A))$
9	7 8	mpdan	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A \lor_{ℋ} ⊥ (A)) = S (A) +_{ℎ} S (⊥ (A))$
10		chjo	$⊢ A \in C_{ℋ} \to A \lor_{ℋ} ⊥ (A) = ℋ$
11	10	fveq2d	$⊢ A \in C_{ℋ} \to S (A \lor_{ℋ} ⊥ (A)) = S (ℋ)$
12	11	adantl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A \lor_{ℋ} ⊥ (A)) = S (ℋ)$
13	9 12	eqtr3d	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A) +_{ℎ} S (⊥ (A)) = S (ℋ)$