P. 306 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30501-30600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pjcohcli 30501	Closure of composition of projections. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ∈ ℋ)
Theorem	pjadjcoi 30502	Adjoint of composition of projections. Special case of Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ·ih 𝐵) = (𝐴 ·ih (((projℎ‘𝐻) ∘ (projℎ‘𝐺))‘𝐵)))
Theorem	pjcofni 30503	Functionality of composition of projections. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) Fn ℋ
Theorem	pjss1coi 30504	Subset relationship for projections. Theorem 4.5(i)<->(iii) of [Beran] p. 112. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) ∘ (projℎ‘𝐺)) = (projℎ‘𝐺))
Theorem	pjss2coi 30505	Subset relationship for projections. Theorem 4.5(i)<->(ii) of [Beran] p. 112. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = (projℎ‘𝐺))
Theorem	pjssmi 30506	Projection meet property. Remark in [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (𝐻 ⊆ 𝐺 → (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴)))
Theorem	pjssge0i 30507	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 30508	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 30509*	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 30510	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 30511	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 30512	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 30513*	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 30514*	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 30513). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (∀𝑥 ∈ ℋ 0 ≤ ((((projℎ‘𝐻) −op (projℎ‘𝐺))‘𝑥) ·ih 𝑥) ↔ ((projℎ‘𝐺) “ ℋ) ⊆ ((projℎ‘𝐻) “ ℋ))
Theorem	pjssdif2i 30515	The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 30513). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) −op (projℎ‘𝐺)) = (projℎ‘(𝐻 ∩ (⊥‘𝐺))))
Theorem	pjssdif1i 30516	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 30513). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) −op (projℎ‘𝐺)) ∈ ran projℎ)
Theorem	pjimai 30517	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 30518	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 30519	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 30520	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 30521	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 30522	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 30523	Definition of projection operator in [Hughes] p. 47, except that we do not need linearity to be explicit by virtue of hmoplin 30283. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝑇 ∈ ran projℎ ↔ (𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇))
Theorem	pjhmopidm 30524	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 30525	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 30526	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 30527	A projector is a positive operator. (Contributed by NM, 27-Sep-2008.) (New usage is discouraged.)
⊢ (𝑇 ∈ ran projℎ → 0hop ≤op 𝑇)
Theorem	pjadj2 30528	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 30529	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 30530	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 30531*	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 30532	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 30533	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 30534	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 30535	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 30536	Lemma for projection commutation theorem. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 𝐶ℋ 𝐻 → ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = (projℎ‘(𝐺 ∩ 𝐻)))
Theorem	pjclem2 30537	Lemma for projection commutation theorem. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 𝐶ℋ 𝐻 → ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = ((projℎ‘𝐻) ∘ (projℎ‘𝐺)))
Theorem	pjclem3 30538	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 30539	Lemma for projection commutation theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (𝐺 ∩ 𝐻) → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) = 𝐴)
Theorem	pjclem4 30540	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 30541	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 30542	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 30543	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 30544	Closure of composition of projection and Hilbert space operator. (Contributed by NM, 3-Dec-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐻) ∘ 𝑇)‘𝐴) ∈ 𝐻)
Theorem	pjadj2coi 30545	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 30546	Closure of double composition of projections. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻))‘𝐴) ∈ 𝐹)
Theorem	pj3lem1 30547	Lemma for projection triplet theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ((𝐹 ∩ 𝐺) ∩ 𝐻) → ((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻))‘𝐴) = 𝐴)
Theorem	pj3si 30548	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 30549	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 30550	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 30551	Theorem S-14 of Watanabe, p. 486. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (normℎ‘(((projℎ‘𝐻) ∘ (projℎ‘𝐺))‘𝐴)) ≤ (normℎ‘((projℎ‘𝐺)‘𝐴)))
19.7  States on a Hilbert lattice and Godowski's equation
19.7.1  States on a Hilbert lattice
Definition	df-st 30552*	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 30553*	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 30554*	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 30555*	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 30556	[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 30557	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 30558	Closure of the value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → (𝑆‘𝐴) ∈ ℋ)
Theorem	hst1a 30559	Unit value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ (𝑆 ∈ CHStates → (normℎ‘(𝑆‘ ℋ)) = 1)
Theorem	hstel2 30560	Properties of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵))) → (((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵))))
Theorem	hstorth 30561	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 30562	Orthogonal sum property of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵))) → (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵)))
Theorem	hstoc 30563	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 30564	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 30565	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 30566	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 30567	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 30568	The norm of a Hilbert-space-valued state equals one iff the state value equals the state value of the lattice unit. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ((normℎ‘(𝑆‘𝐴)) = 1 ↔ (𝑆‘𝐴) = (𝑆‘ ℋ)))
Theorem	hst0h 30569	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 30570	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 30571	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 30572	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 30573	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.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ((𝑆‘𝐴) ·ih (𝑆‘ ℋ)) = 0) → (𝑆‘𝐴) = 0ℎ)
Theorem	hst0 30574	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 30575	The value of a state at the full Hilbert space. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝑆‘ ℋ) = 1)
Theorem	stj 30576	The value of a state on a join. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐴 ⊆ (⊥‘𝐵)) → (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) + (𝑆‘𝐵))))
Theorem	sto1i 30577	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 30578	The state of the orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝑆‘(⊥‘𝐴)) = (1 − (𝑆‘𝐴)))
Theorem	stge1i 30579	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 30580	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 30581	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → (𝑆‘𝐴) ≤ (𝑆‘𝐵)))
Theorem	stlesi 30582	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → ((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1)))
Theorem	stji1i 30583	Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝑆‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) = ((𝑆‘(⊥‘𝐴)) + (𝑆‘(𝐴 ∩ 𝐵))))
Theorem	stm1i 30584	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐴) = 1))
Theorem	stm1ri 30585	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐵) = 1))
Theorem	stm1addi 30586	Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → ((𝑆‘𝐴) + (𝑆‘𝐵)) = 2))
Theorem	staddi 30587	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 30588	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 30589	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 30590	The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝑆‘0ℋ) = 0)
Theorem	strlem1 30591*	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 30592*	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 30593*	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 30594*	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 30595*	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 30596*	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 30597*	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 30598*	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 30599*	Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ States ((𝑓‘𝐴) = 1 → (𝑓‘𝐵) = 1) ↔ 𝐴 ⊆ 𝐵)
Theorem	hstrlem2 30600*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    ⇒   ⊢ (𝐶 ∈ Cℋ → (𝑆‘𝐶) = ((projℎ‘𝐶)‘𝑢))