sto2i

Description: The state of the orthocomplement. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	sto1.1	$⊢ A \in C_{ℋ}$
	Assertion	sto2i	$⊢ S \in States \to S (⊥ (A)) = 1 - S (A)$

Step	Hyp	Ref	Expression
1		sto1.1	$⊢ A \in C_{ℋ}$
2	1	sto1i	$⊢ S \in States \to S (A) + S (⊥ (A)) = 1$
3		stcl	$⊢ S \in States \to (A \in C_{ℋ} \to S (A) \in ℝ)$
4	1 3	mpi	$⊢ S \in States \to S (A) \in ℝ$
5	4	recnd	$⊢ S \in States \to S (A) \in ℂ$
6	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
7		stcl	$⊢ S \in States \to (⊥ (A) \in C_{ℋ} \to S (⊥ (A)) \in ℝ)$
8	6 7	mpi	$⊢ S \in States \to S (⊥ (A)) \in ℝ$
9	8	recnd	$⊢ S \in States \to S (⊥ (A)) \in ℂ$
10		ax-1cn	$⊢ 1 \in ℂ$
11		subadd	$⊢ (1 \in ℂ \land S (A) \in ℂ \land S (⊥ (A)) \in ℂ) \to (1 - S (A) = S (⊥ (A)) \leftrightarrow S (A) + S (⊥ (A)) = 1)$
12	10 11	mp3an1	$⊢ (S (A) \in ℂ \land S (⊥ (A)) \in ℂ) \to (1 - S (A) = S (⊥ (A)) \leftrightarrow S (A) + S (⊥ (A)) = 1)$
13	5 9 12	syl2anc	$⊢ S \in States \to (1 - S (A) = S (⊥ (A)) \leftrightarrow S (A) + S (⊥ (A)) = 1)$
14	2 13	mpbird	$⊢ S \in States \to 1 - S (A) = S (⊥ (A))$
15	14	eqcomd	$⊢ S \in States \to S (⊥ (A)) = 1 - S (A)$

Metamath Proof Explorer