sto1i

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

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

Step	Hyp	Ref	Expression
1		sto1.1	$⊢ A \in C_{ℋ}$
2	1	chjoi	$⊢ A \lor_{ℋ} ⊥ (A) = ℋ$
3	2	fveq2i	$⊢ S (A \lor_{ℋ} ⊥ (A)) = S (ℋ)$
4	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
5	1 4	pm3.2i	$⊢ (A \in C_{ℋ} \land ⊥ (A) \in C_{ℋ})$
6	1	chshii	$⊢ A \in S_{ℋ}$
7		shococss	$⊢ A \in S_{ℋ} \to A \subseteq ⊥ (⊥ (A))$
8	6 7	ax-mp	$⊢ A \subseteq ⊥ (⊥ (A))$
9		stj	$⊢ S \in States \to (((A \in C_{ℋ} \land ⊥ (A) \in C_{ℋ}) \land A \subseteq ⊥ (⊥ (A))) \to S (A \lor_{ℋ} ⊥ (A)) = S (A) + S (⊥ (A)))$
10	5 8 9	mp2ani	$⊢ S \in States \to S (A \lor_{ℋ} ⊥ (A)) = S (A) + S (⊥ (A))$
11		sthil	$⊢ S \in States \to S (ℋ) = 1$
12	3 10 11	3eqtr3a	$⊢ S \in States \to S (A) + S (⊥ (A)) = 1$

Metamath Proof Explorer