hstoh

Description: A Hilbert-space-valued state orthogonal to the state of the lattice unit is zero. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hstoh	$⊢ (S \in CHStates \land A \in C_{ℋ} \land S (A) \cdot_{ih} S (ℋ) = 0) \to S (A) = 0_{ℎ}$

Proof

Step	Hyp	Ref	Expression
1		hstcl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A) \in ℋ$
2		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
3		hstcl	$⊢ (S \in CHStates \land ⊥ (A) \in C_{ℋ}) \to S (⊥ (A)) \in ℋ$
4	2 3	sylan2	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (⊥ (A)) \in ℋ$
5		his7	$⊢ (S (A) \in ℋ \land S (A) \in ℋ \land S (⊥ (A)) \in ℋ) \to S (A) \cdot_{ih} (S (A) +_{ℎ} S (⊥ (A))) = (S (A) \cdot_{ih} S (A)) + (S (A) \cdot_{ih} S (⊥ (A)))$
6	1 1 4 5	syl3anc	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A) \cdot_{ih} (S (A) +_{ℎ} S (⊥ (A))) = (S (A) \cdot_{ih} S (A)) + (S (A) \cdot_{ih} S (⊥ (A)))$
7		normsq	$⊢ S (A) \in ℋ \to {{norm}_{ℎ} (S (A))}^{2} = S (A) \cdot_{ih} S (A)$
8	1 7	syl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} = S (A) \cdot_{ih} S (A)$
9	8	eqcomd	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A) \cdot_{ih} S (A) = {{norm}_{ℎ} (S (A))}^{2}$
10		ococ	$⊢ A \in C_{ℋ} \to ⊥ (⊥ (A)) = A$
11		eqimss2	$⊢ ⊥ (⊥ (A)) = A \to A \subseteq ⊥ (⊥ (A))$
12	10 11	syl	$⊢ A \in C_{ℋ} \to A \subseteq ⊥ (⊥ (A))$
13	2 12	jca	$⊢ A \in C_{ℋ} \to (⊥ (A) \in C_{ℋ} \land A \subseteq ⊥ (⊥ (A)))$
14	13	adantl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to (⊥ (A) \in C_{ℋ} \land A \subseteq ⊥ (⊥ (A)))$
15		hstorth	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (⊥ (A) \in C_{ℋ} \land A \subseteq ⊥ (⊥ (A)))) \to S (A) \cdot_{ih} S (⊥ (A)) = 0$
16	14 15	mpdan	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A) \cdot_{ih} S (⊥ (A)) = 0$
17	9 16	oveq12d	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to (S (A) \cdot_{ih} S (A)) + (S (A) \cdot_{ih} S (⊥ (A))) = {{norm}_{ℎ} (S (A))}^{2} + 0$
18		normcl	$⊢ S (A) \in ℋ \to {norm}_{ℎ} (S (A)) \in ℝ$
19	1 18	syl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {norm}_{ℎ} (S (A)) \in ℝ$
20	19	resqcld	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} \in ℝ$
21	20	recnd	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} \in ℂ$
22	21	addid1d	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} + 0 = {{norm}_{ℎ} (S (A))}^{2}$
23	6 17 22	3eqtrrd	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} = S (A) \cdot_{ih} (S (A) +_{ℎ} S (⊥ (A)))$
24		hstoc	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A) +_{ℎ} S (⊥ (A)) = S (ℋ)$
25	24	oveq2d	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A) \cdot_{ih} (S (A) +_{ℎ} S (⊥ (A))) = S (A) \cdot_{ih} S (ℋ)$
26	23 25	eqtrd	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} = S (A) \cdot_{ih} S (ℋ)$
27		id	$⊢ S (A) \cdot_{ih} S (ℋ) = 0 \to S (A) \cdot_{ih} S (ℋ) = 0$
28	26 27	sylan9eq	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land S (A) \cdot_{ih} S (ℋ) = 0) \to {{norm}_{ℎ} (S (A))}^{2} = 0$
29	28	3impa	$⊢ (S \in CHStates \land A \in C_{ℋ} \land S (A) \cdot_{ih} S (ℋ) = 0) \to {{norm}_{ℎ} (S (A))}^{2} = 0$
30	19	recnd	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {norm}_{ℎ} (S (A)) \in ℂ$
31		sqeq0	$⊢ {norm}_{ℎ} (S (A)) \in ℂ \to ({{norm}_{ℎ} (S (A))}^{2} = 0 \leftrightarrow {norm}_{ℎ} (S (A)) = 0)$
32	30 31	syl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to ({{norm}_{ℎ} (S (A))}^{2} = 0 \leftrightarrow {norm}_{ℎ} (S (A)) = 0)$
33	32	3adant3	$⊢ (S \in CHStates \land A \in C_{ℋ} \land S (A) \cdot_{ih} S (ℋ) = 0) \to ({{norm}_{ℎ} (S (A))}^{2} = 0 \leftrightarrow {norm}_{ℎ} (S (A)) = 0)$
34	29 33	mpbid	$⊢ (S \in CHStates \land A \in C_{ℋ} \land S (A) \cdot_{ih} S (ℋ) = 0) \to {norm}_{ℎ} (S (A)) = 0$
35		hst0h	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to ({norm}_{ℎ} (S (A)) = 0 \leftrightarrow S (A) = 0_{ℎ})$
36	35	3adant3	$⊢ (S \in CHStates \land A \in C_{ℋ} \land S (A) \cdot_{ih} S (ℋ) = 0) \to ({norm}_{ℎ} (S (A)) = 0 \leftrightarrow S (A) = 0_{ℎ})$
37	34 36	mpbid	$⊢ (S \in CHStates \land A \in C_{ℋ} \land S (A) \cdot_{ih} S (ℋ) = 0) \to S (A) = 0_{ℎ}$

Metamath Proof Explorer

Theorem hstoh

Proof