P. 318 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31701-31800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pjssge0i 31701	Theorem 4.5(iv)->(v) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) → 0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴)))
Theorem	pjdifnormi 31702	Theorem 4.5(v)<->(vi) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴) ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘((projℎ‘𝐺)‘𝐴))))
Theorem	pjnormssi 31703*	Theorem 4.5(i)<->(vi) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ 𝐻 ↔ ∀𝑥 ∈ ℋ (normℎ‘((projℎ‘𝐺)‘𝑥)) ≤ (normℎ‘((projℎ‘𝐻)‘𝑥)))
Theorem	pjorthcoi 31704	Composition of projections of orthogonal subspaces. Part (i)->(iia) of Theorem 27.4 of [Halmos] p. 45. (Contributed by NM, 6-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ (⊥‘𝐻) → ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = 0hop )
Theorem	pjscji 31705	The projection of orthogonal subspaces is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ (⊥‘𝐻) → (projℎ‘(𝐺 ∨ℋ 𝐻)) = ((projℎ‘𝐺) +op (projℎ‘𝐻)))
Theorem	pjssumi 31706	The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ (⊥‘𝐻) → (projℎ‘(𝐺 +ℋ 𝐻)) = ((projℎ‘𝐺) +op (projℎ‘𝐻)))
Theorem	pjssposi 31707*	Projector ordering can be expressed by the subset relationship between their projection subspaces. (i)<->(iii) of Theorem 29.2 of [Halmos] p. 48. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (∀𝑥 ∈ ℋ 0 ≤ ((((projℎ‘𝐻) −op (projℎ‘𝐺))‘𝑥) ·ih 𝑥) ↔ 𝐺 ⊆ 𝐻)
Theorem	pjordi 31708*	The definition of projector ordering in [Halmos] p. 42 is equivalent to the definition of projector ordering in [Beran] p. 110. (We will usually express projector ordering with the even simpler equivalent 𝐺 ⊆ 𝐻; see pjssposi 31707). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (∀𝑥 ∈ ℋ 0 ≤ ((((projℎ‘𝐻) −op (projℎ‘𝐺))‘𝑥) ·ih 𝑥) ↔ ((projℎ‘𝐺) “ ℋ) ⊆ ((projℎ‘𝐻) “ ℋ))
Theorem	pjssdif2i 31709	The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 31707). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) −op (projℎ‘𝐺)) = (projℎ‘(𝐻 ∩ (⊥‘𝐺))))
Theorem	pjssdif1i 31710	A necessary and sufficient condition for the difference between two projectors to be a projector. Part 1 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 31707). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) −op (projℎ‘𝐺)) ∈ ran projℎ)
Theorem	pjimai 31711	The image of a projection. Lemma 5 in Daniel Lehmann, "A presentation of Quantum Logic based on an and then connective", https://doi.org/10.48550/arXiv.quant-ph/0701113. (Contributed by NM, 20-Jan-2007.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐵) “ 𝐴) = ((𝐴 +ℋ (⊥‘𝐵)) ∩ 𝐵)
Theorem	pjidmcoi 31712	A projection is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐻) ∘ (projℎ‘𝐻)) = (projℎ‘𝐻)
Theorem	pjoccoi 31713	Composition of projections of a subspace and its orthocomplement. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐻) ∘ (projℎ‘(⊥‘𝐻))) = 0hop
Theorem	pjtoi 31714	Subspace sum of projection and projection of orthocomplement. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐻) +op (projℎ‘(⊥‘𝐻))) = (projℎ‘ ℋ)
Theorem	pjoci 31715	Projection of orthocomplement. First part of Theorem 27.3 of [Halmos] p. 45. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘ ℋ) −op (projℎ‘𝐻)) = (projℎ‘(⊥‘𝐻))
Theorem	pjidmco 31716	A projection operator is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → ((projℎ‘𝐻) ∘ (projℎ‘𝐻)) = (projℎ‘𝐻))
Theorem	dfpjop 31717	Definition of projection operator in [Hughes] p. 47, except that we do not need linearity to be explicit by virtue of hmoplin 31477. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝑇 ∈ ran projℎ ↔ (𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇))
Theorem	pjhmopidm 31718	Two ways to express the set of all projection operators. (Contributed by NM, 24-Apr-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ ran projℎ = {𝑡 ∈ HrmOp ∣ (𝑡 ∘ 𝑡) = 𝑡}
Theorem	elpjidm 31719	A projection operator is idempotent. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ ran projℎ → (𝑇 ∘ 𝑇) = 𝑇)
Theorem	elpjhmop 31720	A projection operator is Hermitian. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ ran projℎ → 𝑇 ∈ HrmOp)
Theorem	0leopj 31721	A projector is a positive operator. (Contributed by NM, 27-Sep-2008.) (New usage is discouraged.)
⊢ (𝑇 ∈ ran projℎ → 0hop ≤op 𝑇)
Theorem	pjadj2 31722	A projector is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ ran projℎ → (adjℎ‘𝑇) = 𝑇)
Theorem	pjadj3 31723	A projector is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (adjℎ‘(projℎ‘𝐻)) = (projℎ‘𝐻))
Theorem	elpjch 31724	Reconstruction of the subspace of a projection operator. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ ran projℎ → (ran 𝑇 ∈ Cℋ ∧ 𝑇 = (projℎ‘ran 𝑇)))
Theorem	elpjrn 31725*	Reconstruction of the subspace of a projection operator. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝑇 ∈ ran projℎ → ran 𝑇 = {𝑥 ∈ ℋ ∣ (𝑇‘𝑥) = 𝑥})
Theorem	pjinvari 31726	A closed subspace 𝐻 with projection 𝑇 is invariant under an operator 𝑆 iff 𝑆𝑇 = 𝑇𝑆𝑇. Theorem 27.1 of [Halmos] p. 45. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝑇 = (projℎ‘𝐻)    ⇒   ⊢ ((𝑆 ∘ 𝑇): ℋ⟶𝐻 ↔ (𝑆 ∘ 𝑇) = (𝑇 ∘ (𝑆 ∘ 𝑇)))
Theorem	pjin1i 31727	Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘(𝐺 ∩ 𝐻)) = ((projℎ‘𝐺) ∘ (projℎ‘(𝐺 ∩ 𝐻)))
Theorem	pjin2i 31728	Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((projℎ‘𝐺) = ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) ∧ (projℎ‘𝐻) = ((projℎ‘𝐻) ∘ (projℎ‘𝐺))) ↔ (projℎ‘𝐺) = (projℎ‘𝐻))
Theorem	pjin3i 31729	Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((projℎ‘𝐹) = ((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∧ (projℎ‘𝐹) = ((projℎ‘𝐹) ∘ (projℎ‘𝐻))) ↔ (projℎ‘𝐹) = ((projℎ‘𝐹) ∘ (projℎ‘(𝐺 ∩ 𝐻))))
Theorem	pjclem1 31730	Lemma for projection commutation theorem. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 𝐶ℋ 𝐻 → ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = (projℎ‘(𝐺 ∩ 𝐻)))
Theorem	pjclem2 31731	Lemma for projection commutation theorem. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 𝐶ℋ 𝐻 → ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = ((projℎ‘𝐻) ∘ (projℎ‘𝐺)))
Theorem	pjclem3 31732	Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = ((projℎ‘𝐻) ∘ (projℎ‘𝐺)) → ((projℎ‘𝐺) ∘ (projℎ‘(⊥‘𝐻))) = ((projℎ‘(⊥‘𝐻)) ∘ (projℎ‘𝐺)))
Theorem	pjclem4a 31733	Lemma for projection commutation theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (𝐺 ∩ 𝐻) → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) = 𝐴)
Theorem	pjclem4 31734	Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = ((projℎ‘𝐻) ∘ (projℎ‘𝐺)) → ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = (projℎ‘(𝐺 ∩ 𝐻)))
Theorem	pjci 31735	Two subspaces commute iff their projections commute. Lemma 4 of [Kalmbach] p. 67. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 𝐶ℋ 𝐻 ↔ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = ((projℎ‘𝐻) ∘ (projℎ‘𝐺)))
Theorem	pjcmul1i 31736	A necessary and sufficient condition for the product of two projectors to be a projector is that the projectors commute. Part 1 of Theorem 1 of [AkhiezerGlazman] p. 65. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = ((projℎ‘𝐻) ∘ (projℎ‘𝐺)) ↔ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) ∈ ran projℎ)
Theorem	pjcmul2i 31737	The projection subspace of the difference between two projectors. Part 2 of Theorem 1 of [AkhiezerGlazman] p. 65. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = ((projℎ‘𝐻) ∘ (projℎ‘𝐺)) ↔ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = (projℎ‘(𝐺 ∩ 𝐻)))
Theorem	pjcohocli 31738	Closure of composition of projection and Hilbert space operator. (Contributed by NM, 3-Dec-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐻) ∘ 𝑇)‘𝐴) ∈ 𝐻)
Theorem	pjadj2coi 31739	Adjoint of double composition of projections. Generalization of special case of Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻))‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((((projℎ‘𝐻) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐹))‘𝐵)))
Theorem	pj2cocli 31740	Closure of double composition of projections. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻))‘𝐴) ∈ 𝐹)
Theorem	pj3lem1 31741	Lemma for projection triplet theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ((𝐹 ∩ 𝐺) ∩ 𝐻) → ((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻))‘𝐴) = 𝐴)
Theorem	pj3si 31742	Stronger projection triplet theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻)) = (((projℎ‘𝐻) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐹)) ∧ ran (((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻)) ⊆ 𝐺) → (((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻)) = (projℎ‘((𝐹 ∩ 𝐺) ∩ 𝐻)))
Theorem	pj3i 31743	Projection triplet theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻)) = (((projℎ‘𝐻) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐹)) ∧ (((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻)) = (((projℎ‘𝐺) ∘ (projℎ‘𝐹)) ∘ (projℎ‘𝐻))) → (((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻)) = (projℎ‘((𝐹 ∩ 𝐺) ∩ 𝐻)))
Theorem	pj3cor1i 31744	Projection triplet corollary. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻)) = (((projℎ‘𝐻) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐹)) ∧ (((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻)) = (((projℎ‘𝐺) ∘ (projℎ‘𝐹)) ∘ (projℎ‘𝐻))) → (((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻)) = (((projℎ‘𝐻) ∘ (projℎ‘𝐹)) ∘ (projℎ‘𝐺)))
Theorem	pjs14i 31745	Theorem S-14 of Watanabe, p. 486. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (normℎ‘(((projℎ‘𝐻) ∘ (projℎ‘𝐺))‘𝐴)) ≤ (normℎ‘((projℎ‘𝐺)‘𝐴)))
20.7  States on a Hilbert lattice and Godowski's equation
20.7.1  States on a Hilbert lattice
Definition	df-st 31746*	Define the set of states on a Hilbert lattice. Definition of [Kalmbach] p. 266. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ States = {𝑓 ∈ ((0[,]1) ↑m Cℋ ) ∣ ((𝑓‘ ℋ) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦))))}
Definition	df-hst 31747*	Define the set of complex Hilbert-space-valued states on a Hilbert lattice. Definition of CH-states in [Mayet3] p. 9. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ CHStates = {𝑓 ∈ ( ℋ ↑m Cℋ ) ∣ ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))}
Theorem	isst 31748*	Property of a state. (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝑆 ∈ States ↔ (𝑆: Cℋ ⟶(0[,]1) ∧ (𝑆‘ ℋ) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦)))))
Theorem	ishst 31749*	Property of a complex Hilbert-space-valued state. Definition of CH-states in [Mayet3] p. 9. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ (𝑆 ∈ CHStates ↔ (𝑆: Cℋ ⟶ ℋ ∧ (normℎ‘(𝑆‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑆‘𝑥) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))))))
Theorem	sticl 31750	[0, 1] closure of the value of a state. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝐴 ∈ Cℋ → (𝑆‘𝐴) ∈ (0[,]1)))
Theorem	stcl 31751	Real closure of the value of a state. (Contributed by NM, 24-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝐴 ∈ Cℋ → (𝑆‘𝐴) ∈ ℝ))
Theorem	hstcl 31752	Closure of the value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → (𝑆‘𝐴) ∈ ℋ)
Theorem	hst1a 31753	Unit value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ (𝑆 ∈ CHStates → (normℎ‘(𝑆‘ ℋ)) = 1)
Theorem	hstel2 31754	Properties of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵))) → (((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵))))
Theorem	hstorth 31755	Orthogonality property of a Hilbert-space-valued state. This is a key feature distinguishing it from a real-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵))) → ((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0)
Theorem	hstosum 31756	Orthogonal sum property of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵))) → (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵)))
Theorem	hstoc 31757	Sum of a Hilbert-space-valued state of a lattice element and its orthocomplement. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ((𝑆‘𝐴) +ℎ (𝑆‘(⊥‘𝐴))) = (𝑆‘ ℋ))
Theorem	hstnmoc 31758	Sum of norms of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → (((normℎ‘(𝑆‘𝐴))↑2) + ((normℎ‘(𝑆‘(⊥‘𝐴)))↑2)) = 1)
Theorem	stge0 31759	The value of a state is nonnegative. (Contributed by NM, 24-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝐴 ∈ Cℋ → 0 ≤ (𝑆‘𝐴)))
Theorem	stle1 31760	The value of a state is less than or equal to one. (Contributed by NM, 24-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝐴 ∈ Cℋ → (𝑆‘𝐴) ≤ 1))
Theorem	hstle1 31761	The norm of the value of a Hilbert-space-valued state is less than or equal to one. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → (normℎ‘(𝑆‘𝐴)) ≤ 1)
Theorem	hst1h 31762	The norm of a Hilbert-space-valued state equals one iff the state value equals the state value of the lattice one. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ((normℎ‘(𝑆‘𝐴)) = 1 ↔ (𝑆‘𝐴) = (𝑆‘ ℋ)))
Theorem	hst0h 31763	The norm of a Hilbert-space-valued state equals zero iff the state value equals zero. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ((normℎ‘(𝑆‘𝐴)) = 0 ↔ (𝑆‘𝐴) = 0ℎ))
Theorem	hstpyth 31764	Pythagorean property of a Hilbert-space-valued state for orthogonal vectors 𝐴 and 𝐵. (Contributed by NM, 26-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵))) → ((normℎ‘(𝑆‘(𝐴 ∨ℋ 𝐵)))↑2) = (((normℎ‘(𝑆‘𝐴))↑2) + ((normℎ‘(𝑆‘𝐵))↑2)))
Theorem	hstle 31765	Ordering property of a Hilbert-space-valued state. (Contributed by NM, 26-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵)) → (normℎ‘(𝑆‘𝐴)) ≤ (normℎ‘(𝑆‘𝐵)))
Theorem	hstles 31766	Ordering property of a Hilbert-space-valued state. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵)) → ((normℎ‘(𝑆‘𝐴)) = 1 → (normℎ‘(𝑆‘𝐵)) = 1))
Theorem	hstoh 31767	A Hilbert-space-valued state orthogonal to the state of the lattice one is zero. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ((𝑆‘𝐴) ·ih (𝑆‘ ℋ)) = 0) → (𝑆‘𝐴) = 0ℎ)
Theorem	hst0 31768	A Hilbert-space-valued state is zero at the zero subspace. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ (𝑆 ∈ CHStates → (𝑆‘0ℋ) = 0ℎ)
Theorem	sthil 31769	The value of a state at the full Hilbert space. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝑆‘ ℋ) = 1)
Theorem	stj 31770	The value of a state on a join. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐴 ⊆ (⊥‘𝐵)) → (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) + (𝑆‘𝐵))))
Theorem	sto1i 31771	The state of a subspace plus the state of its orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘𝐴) + (𝑆‘(⊥‘𝐴))) = 1)
Theorem	sto2i 31772	The state of the orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝑆‘(⊥‘𝐴)) = (1 − (𝑆‘𝐴)))
Theorem	stge1i 31773	If a state is greater than or equal to 1, it is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (1 ≤ (𝑆‘𝐴) ↔ (𝑆‘𝐴) = 1))
Theorem	stle0i 31774	If a state is less than or equal to 0, it is 0. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘𝐴) ≤ 0 ↔ (𝑆‘𝐴) = 0))
Theorem	stlei 31775	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → (𝑆‘𝐴) ≤ (𝑆‘𝐵)))
Theorem	stlesi 31776	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → ((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1)))
Theorem	stji1i 31777	Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝑆‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) = ((𝑆‘(⊥‘𝐴)) + (𝑆‘(𝐴 ∩ 𝐵))))
Theorem	stm1i 31778	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐴) = 1))
Theorem	stm1ri 31779	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐵) = 1))
Theorem	stm1addi 31780	Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → ((𝑆‘𝐴) + (𝑆‘𝐵)) = 2))
Theorem	staddi 31781	If the sum of 2 states is 2, then each state is 1. (Contributed by NM, 12-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (((𝑆‘𝐴) + (𝑆‘𝐵)) = 2 → (𝑆‘𝐴) = 1))
Theorem	stm1add3i 31782	Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘((𝐴 ∩ 𝐵) ∩ 𝐶)) = 1 → (((𝑆‘𝐴) + (𝑆‘𝐵)) + (𝑆‘𝐶)) = 3))
Theorem	stadd3i 31783	If the sum of 3 states is 3, then each state is 1. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((((𝑆‘𝐴) + (𝑆‘𝐵)) + (𝑆‘𝐶)) = 3 → (𝑆‘𝐴) = 1))
Theorem	st0 31784	The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝑆‘0ℋ) = 0)
Theorem	strlem1 31785*	Lemma for strong state theorem: if closed subspace 𝐴 is not contained in 𝐵, there is a unit vector 𝑢 in their difference. (Contributed by NM, 25-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (¬ 𝐴 ⊆ 𝐵 → ∃𝑢 ∈ (𝐴 ∖ 𝐵)(normℎ‘𝑢) = 1)
Theorem	strlem2 31786*	Lemma for strong state theorem. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    ⇒   ⊢ (𝐶 ∈ Cℋ → (𝑆‘𝐶) = ((normℎ‘((projℎ‘𝐶)‘𝑢))↑2))
Theorem	strlem3a 31787*	Lemma for strong state theorem: the function 𝑆, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    ⇒   ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → 𝑆 ∈ States)
Theorem	strlem3 31788*	Lemma for strong state theorem: the function 𝑆, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. This lemma restates the hypotheses in a more convenient form to work with. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → 𝑆 ∈ States)
Theorem	strlem4 31789*	Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → (𝑆‘𝐴) = 1)
Theorem	strlem5 31790*	Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → (𝑆‘𝐵) < 1)
Theorem	strlem6 31791*	Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → ¬ ((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1))
Theorem	stri 31792*	Strong state theorem. The states on a Hilbert lattice define an ordering. Remark in [Mayet] p. 370. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ States ((𝑓‘𝐴) = 1 → (𝑓‘𝐵) = 1) → 𝐴 ⊆ 𝐵)
Theorem	strb 31793*	Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ States ((𝑓‘𝐴) = 1 → (𝑓‘𝐵) = 1) ↔ 𝐴 ⊆ 𝐵)
Theorem	hstrlem2 31794*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    ⇒   ⊢ (𝐶 ∈ Cℋ → (𝑆‘𝐶) = ((projℎ‘𝐶)‘𝑢))
Theorem	hstrlem3a 31795*	Lemma for strong set of CH states theorem: the function 𝑆, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    ⇒   ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → 𝑆 ∈ CHStates)
Theorem	hstrlem3 31796*	Lemma for strong set of CH states theorem: the function 𝑆, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. This lemma restates the hypotheses in a more convenient form to work with. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → 𝑆 ∈ CHStates)
Theorem	hstrlem4 31797*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → (normℎ‘(𝑆‘𝐴)) = 1)
Theorem	hstrlem5 31798*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → (normℎ‘(𝑆‘𝐵)) < 1)
Theorem	hstrlem6 31799*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → ¬ ((normℎ‘(𝑆‘𝐴)) = 1 → (normℎ‘(𝑆‘𝐵)) = 1))
Theorem	hstri 31800*	Hilbert space admits a strong set of Hilbert-space-valued states (CH-states). Theorem in [Mayet3] p. 10. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ CHStates ((normℎ‘(𝑓‘𝐴)) = 1 → (normℎ‘(𝑓‘𝐵)) = 1) → 𝐴 ⊆ 𝐵)