P. 317 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31601-31700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pjadjii 31601	A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (((projℎ‘𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((projℎ‘𝐻)‘𝐵))
Theorem	pjaddii 31602	Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵))
Theorem	pjinormii 31603	The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴) = ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2)
Theorem	pjmulii 31604	Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐶 ·ℎ 𝐴)) = (𝐶 ·ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjsubii 31605	Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵))
Theorem	pjsslem 31606	Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ ((projℎ‘(⊥‘𝐺))‘𝐴)) = (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjss2i 31607	Subset relationship for projections. Theorem 4.5(i)->(ii) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (𝐻 ⊆ 𝐺 → ((projℎ‘𝐻)‘((projℎ‘𝐺)‘𝐴)) = ((projℎ‘𝐻)‘𝐴))
Theorem	pjssmii 31608	Projection meet property. Remark in [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (𝐻 ⊆ 𝐺 → (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴))
Theorem	pjssge0ii 31609	Theorem 4.5(iv)->(v) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) → 0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴))
Theorem	pjdifnormii 31610	Theorem 4.5(v)<->(vi) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴) ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘((projℎ‘𝐺)‘𝐴)))
Theorem	pjcji 31611	The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (𝐻 ⊆ (⊥‘𝐺) → ((projℎ‘(𝐻 ∨ℋ 𝐺))‘𝐴) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴)))
Theorem	pjadji 31612	A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (((projℎ‘𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((projℎ‘𝐻)‘𝐵)))
Theorem	pjaddi 31613	Projection of vector sum is sum of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjinormi 31614	The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐻)‘𝐴) ·ih 𝐴) = ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2))
Theorem	pjsubi 31615	Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjmuli 31616	Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjige0i 31617	The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → 0 ≤ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴))
Theorem	pjige0 31618	The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → 0 ≤ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴))
Theorem	pjcjt2 31619	The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐺 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐻 ⊆ (⊥‘𝐺) → ((projℎ‘(𝐻 ∨ℋ 𝐺))‘𝐴) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴))))
Theorem	pj0i 31620	The projection of the zero vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐻)‘0ℎ) = 0ℎ
Theorem	pjch 31621	Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ ((projℎ‘𝐻)‘𝐴) = 𝐴))
Theorem	pjid 31622	The projection of a vector in the projection subspace is itself. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ 𝐻) → ((projℎ‘𝐻)‘𝐴) = 𝐴)
Theorem	pjvec 31623*	The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → 𝐻 = {𝑥 ∈ ℋ ∣ ((projℎ‘𝐻)‘𝑥) = 𝑥})
Theorem	pjocvec 31624*	The set of vectors belonging to the orthocomplemented subspace of a projection. Second part of Theorem 27.3 of [Halmos] p. 45. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (⊥‘𝐻) = {𝑥 ∈ ℋ ∣ ((projℎ‘𝐻)‘𝑥) = 0ℎ})
Theorem	pjocini 31625	Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘(𝐺 ∩ 𝐻)) → ((projℎ‘𝐺)‘𝐴) ∈ (⊥‘(𝐺 ∩ 𝐻)))
Theorem	pjini 31626	Membership of projection in an intersection. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (𝐺 ∩ 𝐻) → ((projℎ‘𝐺)‘𝐴) ∈ (𝐺 ∩ 𝐻))
Theorem	pjjsi 31627*	A sufficient condition for subspace join to be equal to subspace sum. (Contributed by NM, 29-May-2004.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ (∀𝑥 ∈ (𝐺 ∨ℋ 𝐻)((projℎ‘(⊥‘𝐺))‘𝑥) ∈ 𝐻 → (𝐺 ∨ℋ 𝐻) = (𝐺 +ℋ 𝐻))
Theorem	pjfni 31628	Functionality of a projection. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻) Fn ℋ
Theorem	pjrni 31629	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ran (projℎ‘𝐻) = 𝐻
Theorem	pjfoi 31630	A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻): ℋ–onto→𝐻
Theorem	pjfi 31631	The mapping of a projection. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻): ℋ⟶ ℋ
Theorem	pjvi 31632	The value of a projection in terms of components. (Contributed by NM, 28-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = 𝐴)
Theorem	pjhfo 31633	A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ–onto→𝐻)
Theorem	pjrn 31634	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → ran (projℎ‘𝐻) = 𝐻)
Theorem	pjhf 31635	The mapping of a projection. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ⟶ ℋ)
Theorem	pjfn 31636	Functionality of a projection. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) Fn ℋ)
Theorem	pjsumi 31637	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ℎ‘𝐺)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐴))))
Theorem	pj11i 31638	One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻)
Theorem	pjdsi 31639	Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 21-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ (𝐺 ∨ℋ 𝐻) ∧ 𝐺 ⊆ (⊥‘𝐻)) → 𝐴 = (((projℎ‘𝐺)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐴)))
Theorem	pjds3i 31640	Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((𝐴 ∈ ((𝐹 ∨ℋ 𝐺) ∨ℋ 𝐻) ∧ 𝐹 ⊆ (⊥‘𝐺)) ∧ (𝐹 ⊆ (⊥‘𝐻) ∧ 𝐺 ⊆ (⊥‘𝐻))) → 𝐴 = ((((projℎ‘𝐹)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴)) +ℎ ((projℎ‘𝐻)‘𝐴)))
Theorem	pj11 31641	One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ) → ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻))
Theorem	pjmfn 31642	Functionality of the projection function. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ projℎ Fn Cℋ
Theorem	pjmf1 31643	The projector function maps one-to-one into the set of Hilbert space operators. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ projℎ: Cℋ –1-1→( ℋ ↑m ℋ)
Theorem	pjoi0 31644	The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ (((𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) ∧ 𝐺 ⊆ (⊥‘𝐻)) → (((projℎ‘𝐺)‘𝐴) ·ih ((projℎ‘𝐻)‘𝐴)) = 0)
Theorem	pjoi0i 31645	The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (𝐺 ⊆ (⊥‘𝐻) → (((projℎ‘𝐺)‘𝐴) ·ih ((projℎ‘𝐻)‘𝐴)) = 0)
Theorem	pjopythi 31646	Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (𝐺 ⊆ (⊥‘𝐻) → ((normℎ‘(((projℎ‘𝐺)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐴)))↑2) = (((normℎ‘((projℎ‘𝐺)‘𝐴))↑2) + ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2)))
Theorem	pjopyth 31647	Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐺 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐻 ⊆ (⊥‘𝐺) → ((normℎ‘(((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴)))↑2) = (((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) + ((normℎ‘((projℎ‘𝐺)‘𝐴))↑2))))
Theorem	pjnormi 31648	The norm of the projection is less than or equal to the norm. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘𝐴)
Theorem	pjpythi 31649	Pythagorean theorem for projections. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((normℎ‘𝐴)↑2) = (((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) + ((normℎ‘((projℎ‘(⊥‘𝐻))‘𝐴))↑2))
Theorem	pjneli 31650	If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (¬ 𝐴 ∈ 𝐻 ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) < (normℎ‘𝐴))
Theorem	pjnorm 31651	The norm of the projection is less than or equal to the norm. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘𝐴))
Theorem	pjpyth 31652	Pythagorean theorem for projectors. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((normℎ‘𝐴)↑2) = (((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) + ((normℎ‘((projℎ‘(⊥‘𝐻))‘𝐴))↑2)))
Theorem	pjnel 31653	If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (¬ 𝐴 ∈ 𝐻 ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) < (normℎ‘𝐴)))
Theorem	pjnorm2 31654	A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch 31621 yield Theorem 26.3 of [Halmos] p. 44. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) = (normℎ‘𝐴)))
20.5.11  Mayet's equation E_3
Theorem	mayete3i 31655	Mayet's equation E3. Part of Theorem 4.1 of [Mayet3] p. 1223. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    &   ⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐴 ⊆ (⊥‘𝐶)    &   ⊢ 𝐴 ⊆ (⊥‘𝐹)    &   ⊢ 𝐶 ⊆ (⊥‘𝐹)    &   ⊢ 𝐴 ⊆ (⊥‘𝐵)    &   ⊢ 𝐶 ⊆ (⊥‘𝐷)    &   ⊢ 𝐹 ⊆ (⊥‘𝐺)    &   ⊢ 𝑋 = ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)    &   ⊢ 𝑌 = (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺))    &   ⊢ 𝑍 = ((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺)    ⇒   ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑍
Theorem	mayetes3i 31656	Mayet's equation E^*3, derived from E3. Solution, for n = 3, to open problem in Remark (b) after Theorem 7.1 of [Mayet3] p. 1240. (Contributed by NM, 10-May-2009.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    &   ⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝐴 ⊆ (⊥‘𝐶)    &   ⊢ 𝐴 ⊆ (⊥‘𝐹)    &   ⊢ 𝐶 ⊆ (⊥‘𝐹)    &   ⊢ 𝐴 ⊆ (⊥‘𝐵)    &   ⊢ 𝐶 ⊆ (⊥‘𝐷)    &   ⊢ 𝐹 ⊆ (⊥‘𝐺)    &   ⊢ 𝑅 ⊆ (⊥‘𝑋)    &   ⊢ 𝑋 = ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)    &   ⊢ 𝑌 = (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺))    &   ⊢ 𝑍 = ((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺)    ⇒   ⊢ ((𝑋 ∨ℋ 𝑅) ∩ 𝑌) ⊆ (𝑍 ∨ℋ 𝑅)
20.6  Operators on Hilbert spaces
20.6.1  Operator sum, difference, and scalar multiplication Note on operators. Unlike some authors, we use the term "operator" to mean any function from ℋ to ℋ. This is the definition of operator in [Hughes] p. 14, the definition of operator in [AkhiezerGlazman] p. 30, and the definition of operator in [Goldberg] p. 10. For Reed and Simon, an operator is linear (definition of operator in [ReedSimon] p. 2). For Halmos, an operator is bounded and linear (definition of operator in [Halmos] p. 35). For Kalmbach and Beran, an operator is continuous and linear (definition of operator in [Kalmbach] p. 353; definition of operator in [Beran] p. 99). Note that "bounded and linear" and "continuous and linear" are equivalent by lncnbd 31965.
Definition	df-hosum 31657*	Define the sum of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.)
⊢ +op = (𝑓 ∈ ( ℋ ↑m ℋ), 𝑔 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ ((𝑓‘𝑥) +ℎ (𝑔‘𝑥))))
Definition	df-homul 31658*	Define the scalar product with a Hilbert space operator. Definition of [Beran] p. 111. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
⊢ ·op = (𝑓 ∈ ℂ, 𝑔 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ (𝑓 ·ℎ (𝑔‘𝑥))))
Definition	df-hodif 31659*	Define the difference of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.)
⊢ −op = (𝑓 ∈ ( ℋ ↑m ℋ), 𝑔 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ ((𝑓‘𝑥) −ℎ (𝑔‘𝑥))))
Definition	df-hfsum 31660*	Define the sum of two Hilbert space functionals. Definition of [Beran] p. 111. Note that unlike some authors, we define a functional as any function from ℋ to ℂ, not just linear (or bounded linear) ones. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ +fn = (𝑓 ∈ (ℂ ↑m ℋ), 𝑔 ∈ (ℂ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ ((𝑓‘𝑥) + (𝑔‘𝑥))))
Definition	df-hfmul 31661*	Define the scalar product with a Hilbert space functional. Definition of [Beran] p. 111. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ ·fn = (𝑓 ∈ ℂ, 𝑔 ∈ (ℂ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ (𝑓 · (𝑔‘𝑥))))
Theorem	hosmval 31662*	Value of the sum of two Hilbert space operators. (Contributed by NM, 9-Nov-2000.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇) = (𝑥 ∈ ℋ ↦ ((𝑆‘𝑥) +ℎ (𝑇‘𝑥))))
Theorem	hommval 31663*	Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op 𝑇) = (𝑥 ∈ ℋ ↦ (𝐴 ·ℎ (𝑇‘𝑥))))
Theorem	hodmval 31664*	Value of the difference of two Hilbert space operators. (Contributed by NM, 9-Nov-2000.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇) = (𝑥 ∈ ℋ ↦ ((𝑆‘𝑥) −ℎ (𝑇‘𝑥))))
Theorem	hfsmval 31665*	Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ℂ ∧ 𝑇: ℋ⟶ℂ) → (𝑆 +fn 𝑇) = (𝑥 ∈ ℋ ↦ ((𝑆‘𝑥) + (𝑇‘𝑥))))
Theorem	hfmmval 31666*	Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ℂ) → (𝐴 ·fn 𝑇) = (𝑥 ∈ ℋ ↦ (𝐴 · (𝑇‘𝑥))))
Theorem	hosval 31667	Value of the sum of two Hilbert space operators. (Contributed by NM, 10-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℋ) → ((𝑆 +op 𝑇)‘𝐴) = ((𝑆‘𝐴) +ℎ (𝑇‘𝐴)))
Theorem	homval 31668	Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·op 𝑇)‘𝐵) = (𝐴 ·ℎ (𝑇‘𝐵)))
Theorem	hodval 31669	Value of the difference of two Hilbert space operators. (Contributed by NM, 10-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℋ) → ((𝑆 −op 𝑇)‘𝐴) = ((𝑆‘𝐴) −ℎ (𝑇‘𝐴)))
Theorem	hfsval 31670	Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ℂ ∧ 𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ ℋ) → ((𝑆 +fn 𝑇)‘𝐴) = ((𝑆‘𝐴) + (𝑇‘𝐴)))
Theorem	hfmval 31671	Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ℂ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·fn 𝑇)‘𝐵) = (𝐴 · (𝑇‘𝐵)))
Theorem	hoscl 31672	Closure of the sum of two Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝐴 ∈ ℋ) → ((𝑆 +op 𝑇)‘𝐴) ∈ ℋ)
Theorem	homcl 31673	Closure of the scalar product of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·op 𝑇)‘𝐵) ∈ ℋ)
Theorem	hodcl 31674	Closure of the difference of two Hilbert space operators. (Contributed by NM, 15-Nov-2002.) (New usage is discouraged.)
⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝐴 ∈ ℋ) → ((𝑆 −op 𝑇)‘𝐴) ∈ ℋ)
20.6.2  Zero and identity operators
Definition	df-h0op 31675	Define the Hilbert space zero operator. See df0op2 31679 for alternate definition. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ 0hop = (projℎ‘0ℋ)
Definition	df-iop 31676	Define the Hilbert space identity operator. See dfiop2 31680 for alternate definition. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
⊢ Iop = (projℎ‘ ℋ)
Theorem	ho0val 31677	Value of the zero Hilbert space operator (null projector). Remark in [Beran] p. 111. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ( 0hop ‘𝐴) = 0ℎ)
Theorem	ho0f 31678	Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 0hop : ℋ⟶ ℋ
Theorem	df0op2 31679	Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.)
⊢ 0hop = ( ℋ × 0ℋ)
Theorem	dfiop2 31680	Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.)
⊢ Iop = ( I ↾ ℋ)
Theorem	hoif 31681	Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.)
⊢ Iop : ℋ–1-1-onto→ ℋ
Theorem	hoival 31682	The value of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ( Iop ‘𝐴) = 𝐴)
Theorem	hoico1 31683	Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (𝑇 ∘ Iop ) = 𝑇)
Theorem	hoico2 31684	Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → ( Iop ∘ 𝑇) = 𝑇)
20.6.3  Operations on Hilbert space operators
Theorem	hoaddcl 31685	The sum of Hilbert space operators is an operator. (Contributed by NM, 21-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇): ℋ⟶ ℋ)
Theorem	homulcl 31686	The scalar product of a Hilbert space operator is an operator. (Contributed by NM, 21-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op 𝑇): ℋ⟶ ℋ)
Theorem	hoeq 31687*	Equality of Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑈‘𝑥) ↔ 𝑇 = 𝑈))
Theorem	hoeqi 31688*	Equality of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (∀𝑥 ∈ ℋ (𝑆‘𝑥) = (𝑇‘𝑥) ↔ 𝑆 = 𝑇)
Theorem	hoscli 31689	Closure of Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((𝑆 +op 𝑇)‘𝐴) ∈ ℋ)
Theorem	hodcli 31690	Closure of Hilbert space operator difference. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((𝑆 −op 𝑇)‘𝐴) ∈ ℋ)
Theorem	hocoi 31691	Composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝐴) = (𝑆‘(𝑇‘𝐴)))
Theorem	hococli 31692	Closure of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝐴) ∈ ℋ)
Theorem	hocofi 31693	Mapping of composition of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 ∘ 𝑇): ℋ⟶ ℋ
Theorem	hocofni 31694	Functionality of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 ∘ 𝑇) Fn ℋ
Theorem	hoaddcli 31695	Mapping of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 +op 𝑇): ℋ⟶ ℋ
Theorem	hosubcli 31696	Mapping of difference of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 −op 𝑇): ℋ⟶ ℋ
Theorem	hoaddfni 31697	Functionality of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 +op 𝑇) Fn ℋ
Theorem	hosubfni 31698	Functionality of difference of Hilbert space operators. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 −op 𝑇) Fn ℋ
Theorem	hoaddcomi 31699	Commutativity of sum of Hilbert space operators. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 +op 𝑇) = (𝑇 +op 𝑆)
Theorem	hosubcl 31700	Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇): ℋ⟶ ℋ)