HomeTheorem List (p. 311 of 473)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 311 of 473) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-29860) |
Hilbert Space Explorer
(29861-31383) |
Users' Mathboxes
(31384-47242) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rnelshi 31001 | The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ran 𝑇 ∈ Sℋ | ||
| Theorem | nlelshi 31002 | The null space of a linear functional is a subspace. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn ⇒ ⊢ (null‘𝑇) ∈ Sℋ | ||
| Theorem | nlelchi 31003 | The null space of a continuous linear functional is a closed subspace. Remark 3.8 of [Beran] p. 103. (Contributed by NM, 11-Feb-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn & ⊢ 𝑇 ∈ ContFn ⇒ ⊢ (null‘𝑇) ∈ Cℋ | ||
| Theorem | riesz3i 31004* | A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn & ⊢ 𝑇 ∈ ContFn ⇒ ⊢ ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) | ||
| Theorem | riesz4i 31005* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn & ⊢ 𝑇 ∈ ContFn ⇒ ⊢ ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) | ||
| Theorem | riesz4 31006* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 31008 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) | ||
| Theorem | riesz1 31007* | Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 2, see riesz2 31008. For the continuous linear functional version, see riesz3i 31004 and riesz4 31006. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinFn → ((normfn‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))) | ||
| Theorem | riesz2 31008* | Part 2 of the Riesz representation theorem for bounded linear functionals. The value of a bounded linear functional corresponds to a unique inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 1, see riesz1 31007. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)) | ||
| Theorem | cnlnadjlem1 31009* | Lemma for cnlnadji 31018 (Theorem 3.10 of [Beran] p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional 𝐺. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) ⇒ ⊢ (𝐴 ∈ ℋ → (𝐺‘𝐴) = ((𝑇‘𝐴) ·ih 𝑦)) | ||
| Theorem | cnlnadjlem2 31010* | Lemma for cnlnadji 31018. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) ⇒ ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn)) | ||
| Theorem | cnlnadjlem3 31011* | Lemma for cnlnadji 31018. By riesz4 31006, 𝐵 is the unique vector such that (𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) for all 𝑣. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ⇒ ⊢ (𝑦 ∈ ℋ → 𝐵 ∈ ℋ) | ||
| Theorem | cnlnadjlem4 31012* | Lemma for cnlnadji 31018. The values of auxiliary function 𝐹 are vectors. (Contributed by NM, 17-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ (𝐴 ∈ ℋ → (𝐹‘𝐴) ∈ ℋ) | ||
| Theorem | cnlnadjlem5 31013* | Lemma for cnlnadji 31018. 𝐹 is an adjoint of 𝑇 (later, we will show it is unique). (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇‘𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹‘𝐴))) | ||
| Theorem | cnlnadjlem6 31014* | Lemma for cnlnadji 31018. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ 𝐹 ∈ LinOp | ||
| Theorem | cnlnadjlem7 31015* | Lemma for cnlnadji 31018. Helper lemma to show that 𝐹 is continuous. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ (𝐴 ∈ ℋ → (normℎ‘(𝐹‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴))) | ||
| Theorem | cnlnadjlem8 31016* | Lemma for cnlnadji 31018. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ 𝐹 ∈ ContOp | ||
| Theorem | cnlnadjlem9 31017* | Lemma for cnlnadji 31018. 𝐹 provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑧 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑧) = (𝑥 ·ih (𝑡‘𝑧)) | ||
| Theorem | cnlnadji 31018* | Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp ⇒ ⊢ ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦)) | ||
| Theorem | cnlnadjeui 31019* | Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp ⇒ ⊢ ∃!𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦)) | ||
| Theorem | cnlnadjeu 31020* | Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinOp ∩ ContOp) → ∃!𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦))) | ||
| Theorem | cnlnadj 31021* | Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinOp ∩ ContOp) → ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦))) | ||
| Theorem | cnlnssadj 31022 | Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ (LinOp ∩ ContOp) ⊆ dom adjℎ | ||
| Theorem | bdopssadj 31023 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ BndLinOp ⊆ dom adjℎ | ||
| Theorem | bdopadj 31024 | Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ) | ||
| Theorem | adjbdln 31025 | The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp → (adjℎ‘𝑇) ∈ BndLinOp) | ||
| Theorem | adjbdlnb 31026 | An operator is bounded and linear iff its adjoint is. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp ↔ (adjℎ‘𝑇) ∈ BndLinOp) | ||
| Theorem | adjbd1o 31027 | The mapping of adjoints of bounded linear operators is one-to-one onto. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.) |
| ⊢ (adjℎ ↾ BndLinOp):BndLinOp–1-1-onto→BndLinOp | ||
| Theorem | adjlnop 31028 | The adjoint of an operator is linear. Proposition 1 of [AkhiezerGlazman] p. 80. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) ∈ LinOp) | ||
| Theorem | adjsslnop 31029 | Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
| ⊢ dom adjℎ ⊆ LinOp | ||
| Theorem | nmopadjlei 31030 | Property of the norm of an adjoint. Part of proof of Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝐴 ∈ ℋ → (normℎ‘((adjℎ‘𝑇)‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴))) | ||
| Theorem | nmopadjlem 31031 | Lemma for nmopadji 31032. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(adjℎ‘𝑇)) ≤ (normop‘𝑇) | ||
| Theorem | nmopadji 31032 | Property of the norm of an adjoint. Theorem 3.11(v) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(adjℎ‘𝑇)) = (normop‘𝑇) | ||
| Theorem | adjeq0 31033 | An operator is zero iff its adjoint is zero. Theorem 3.11(i) of [Beran] p. 106. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 = 0hop ↔ (adjℎ‘𝑇) = 0hop ) | ||
| Theorem | adjmul 31034 | The adjoint of the scalar product of an operator. Theorem 3.11(ii) of [Beran] p. 106. (Contributed by NM, 21-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom adjℎ) → (adjℎ‘(𝐴 ·op 𝑇)) = ((∗‘𝐴) ·op (adjℎ‘𝑇))) | ||
| Theorem | adjadd 31035 | The adjoint of the sum of two operators. Theorem 3.11(iii) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ) → (adjℎ‘(𝑆 +op 𝑇)) = ((adjℎ‘𝑆) +op (adjℎ‘𝑇))) | ||
| Theorem | nmoptrii 31036 | Triangle inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(𝑆 +op 𝑇)) ≤ ((normop‘𝑆) + (normop‘𝑇)) | ||
| Theorem | nmopcoi 31037 | Upper bound for the norm of the composition of two bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(𝑆 ∘ 𝑇)) ≤ ((normop‘𝑆) · (normop‘𝑇)) | ||
| Theorem | bdophsi 31038 | The sum of two bounded linear operators is a bounded linear operator. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 +op 𝑇) ∈ BndLinOp | ||
| Theorem | bdophdi 31039 | The difference between two bounded linear operators is bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 −op 𝑇) ∈ BndLinOp | ||
| Theorem | bdopcoi 31040 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp | ||
| Theorem | nmoptri2i 31041 | Triangle-type inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ ((normop‘𝑆) − (normop‘𝑇)) ≤ (normop‘(𝑆 +op 𝑇)) | ||
| Theorem | adjcoi 31042 | The adjoint of a composition of bounded linear operators. Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (adjℎ‘(𝑆 ∘ 𝑇)) = ((adjℎ‘𝑇) ∘ (adjℎ‘𝑆)) | ||
| Theorem | nmopcoadji 31043 | The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘((adjℎ‘𝑇) ∘ 𝑇)) = ((normop‘𝑇)↑2) | ||
| Theorem | nmopcoadj2i 31044 | The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (normop‘(𝑇 ∘ (adjℎ‘𝑇))) = ((normop‘𝑇)↑2) | ||
| Theorem | nmopcoadj0i 31045 | An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ ((𝑇 ∘ (adjℎ‘𝑇)) = 0hop ↔ 𝑇 = 0hop ) | ||
| Theorem | unierri 31046 | If we approximate a chain of unitary transformations (quantum computer gates) 𝐹, 𝐺 by other unitary transformations 𝑆, 𝑇, the error increases at most additively. Equation 4.73 of [NielsenChuang] p. 195. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝐹 ∈ UniOp & ⊢ 𝐺 ∈ UniOp & ⊢ 𝑆 ∈ UniOp & ⊢ 𝑇 ∈ UniOp ⇒ ⊢ (normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ≤ ((normop‘(𝐹 −op 𝑆)) + (normop‘(𝐺 −op 𝑇))) | ||
| Theorem | branmfn 31047 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴)) | ||
| Theorem | brabn 31048 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ) | ||
| Theorem | rnbra 31049 | The set of bras equals the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ ran bra = (LinFn ∩ ContFn) | ||
| Theorem | bra11 31050 | The bra function maps vectors one-to-one onto the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ bra: ℋ–1-1-onto→(LinFn ∩ ContFn) | ||
| Theorem | bracnln 31051 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ (LinFn ∩ ContFn)) | ||
| Theorem | cnvbraval 31052* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 31006, this very important theorem not only justifies the Dirac bra-ket notation, but allows to extract a unique vector from any continuous linear functional from which the functional can be recovered; i.e. a single vector can "store" all of the information contained in any entire continuous linear functional (mapping from ℋ to ℂ). (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) = (℩𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))) | ||
| Theorem | cnvbracl 31053 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) ∈ ℋ) | ||
| Theorem | cnvbrabra 31054 | The converse bra of the bra of a vector is the vector itself. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (◡bra‘(bra‘𝐴)) = 𝐴) | ||
| Theorem | bracnvbra 31055 | The bra of the converse bra of a continuous linear functional. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (bra‘(◡bra‘𝑇)) = 𝑇) | ||
| Theorem | bracnlnval 31056* | The vector that a continuous linear functional is the bra of. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → 𝑇 = (bra‘(℩𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)))) | ||
| Theorem | cnvbramul 31057 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ (LinFn ∩ ContFn)) → (◡bra‘(𝐴 ·fn 𝑇)) = ((∗‘𝐴) ·ℎ (◡bra‘𝑇))) | ||
| Theorem | kbass1 31058 | Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ ) ∣ 𝐶⟩ = ∣ 𝐴⟩(⟨𝐵 ∣ 𝐶⟩), i.e., the juxtaposition of an outer product with a ket equals a bra juxtaposed with an inner product. Since ⟨𝐵 ∣ 𝐶⟩ is a complex number, it is the first argument in the inner product ·ℎ that it is mapped to, although in Dirac notation it is placed after the ket. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ketbra 𝐵)‘𝐶) = (((bra‘𝐵)‘𝐶) ·ℎ 𝐴)) | ||
| Theorem | kbass2 31059 | Dirac bra-ket associative law (⟨𝐴 ∣ 𝐵⟩)⟨𝐶 ∣ = ⟨𝐴 ∣ ( ∣ 𝐵⟩⟨𝐶 ∣ ), i.e., the juxtaposition of an inner product with a bra equals a ket juxtaposed with an outer product. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶)) = ((bra‘𝐴) ∘ (𝐵 ketbra 𝐶))) | ||
| Theorem | kbass3 31060 | Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = (⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ ) ∣ 𝐷⟩. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶))‘𝐷)) | ||
| Theorem | kbass4 31061 | Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = ⟨𝐴 ∣ ( ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((bra‘𝐴)‘(((bra‘𝐶)‘𝐷) ·ℎ 𝐵))) | ||
| Theorem | kbass5 31062 | Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = (( ∣ 𝐴⟩⟨𝐵 ∣ ) ∣ 𝐶⟩)⟨𝐷 ∣. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (((𝐴 ketbra 𝐵)‘𝐶) ketbra 𝐷)) | ||
| Theorem | kbass6 31063 | Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = ∣ 𝐴⟩(⟨𝐵 ∣ ( ∣ 𝐶⟩⟨𝐷 ∣ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (𝐴 ketbra (◡bra‘((bra‘𝐵) ∘ (𝐶 ketbra 𝐷))))) | ||
| Theorem | leopg 31064* | Ordering relation for positive operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐵) → (𝑇 ≤op 𝑈 ↔ ((𝑈 −op 𝑇) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑈 −op 𝑇)‘𝑥) ·ih 𝑥)))) | ||
| Theorem | leop 31065* | Ordering relation for operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ≤op 𝑈 ↔ ∀𝑥 ∈ ℋ 0 ≤ (((𝑈 −op 𝑇)‘𝑥) ·ih 𝑥))) | ||
| Theorem | leop2 31066* | Ordering relation for operators. Definition of operator ordering in [Young] p. 141. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ≤op 𝑈 ↔ ∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑥) ≤ ((𝑈‘𝑥) ·ih 𝑥))) | ||
| Theorem | leop3 31067 | Operator ordering in terms of a positive operator. Definition of operator ordering in [Retherford] p. 49. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ≤op 𝑈 ↔ 0hop ≤op (𝑈 −op 𝑇))) | ||
| Theorem | leoppos 31068* | Binary relation defining a positive operator. Definition VI.1 of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → ( 0hop ≤op 𝑇 ↔ ∀𝑥 ∈ ℋ 0 ≤ ((𝑇‘𝑥) ·ih 𝑥))) | ||
| Theorem | leoprf2 31069 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → 𝑇 ≤op 𝑇) | ||
| Theorem | leoprf 31070 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → 𝑇 ≤op 𝑇) | ||
| Theorem | leopsq 31071 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → 0hop ≤op (𝑇 ∘ 𝑇)) | ||
| Theorem | 0leop 31072 | The zero operator is a positive operator. (The literature calls it "positive", even though in some sense it is really "nonnegative".) Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ 0hop ≤op 0hop | ||
| Theorem | idleop 31073 | The identity operator is a positive operator. Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ 0hop ≤op Iop | ||
| Theorem | leopadd 31074 | The sum of two positive operators is positive. Exercise 1(i) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ ( 0hop ≤op 𝑇 ∧ 0hop ≤op 𝑈)) → 0hop ≤op (𝑇 +op 𝑈)) | ||
| Theorem | leopmuli 31075 | The scalar product of a nonnegative real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) ∧ (0 ≤ 𝐴 ∧ 0hop ≤op 𝑇)) → 0hop ≤op (𝐴 ·op 𝑇)) | ||
| Theorem | leopmul 31076 | The scalar product of a positive real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴) → ( 0hop ≤op 𝑇 ↔ 0hop ≤op (𝐴 ·op 𝑇))) | ||
| Theorem | leopmul2i 31077 | Scalar product applied to operator ordering. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (0 ≤ 𝐴 ∧ 𝑇 ≤op 𝑈)) → (𝐴 ·op 𝑇) ≤op (𝐴 ·op 𝑈)) | ||
| Theorem | leoptri 31078 | The positive operator ordering relation satisfies trichotomy. Exercise 1(iii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → ((𝑇 ≤op 𝑈 ∧ 𝑈 ≤op 𝑇) ↔ 𝑇 = 𝑈)) | ||
| Theorem | leoptr 31079 | The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (((𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑆 ≤op 𝑇 ∧ 𝑇 ≤op 𝑈)) → 𝑆 ≤op 𝑈) | ||
| Theorem | leopnmid 31080 | A bounded Hermitian operator is less than or equal to its norm times the identity operator. (Contributed by NM, 11-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ (normop‘𝑇) ∈ ℝ) → 𝑇 ≤op ((normop‘𝑇) ·op Iop )) | ||
| Theorem | nmopleid 31081 | A nonzero, bounded Hermitian operator divided by its norm is less than or equal to the identity operator. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ (normop‘𝑇) ∈ ℝ ∧ 𝑇 ≠ 0hop ) → ((1 / (normop‘𝑇)) ·op 𝑇) ≤op Iop ) | ||
| Theorem | opsqrlem1 31082* | Lemma for opsqri . (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ (normop‘𝑇) ∈ ℝ & ⊢ 0hop ≤op 𝑇 & ⊢ 𝑅 = ((1 / (normop‘𝑇)) ·op 𝑇) & ⊢ (𝑇 ≠ 0hop → ∃𝑢 ∈ HrmOp ( 0hop ≤op 𝑢 ∧ (𝑢 ∘ 𝑢) = 𝑅)) ⇒ ⊢ (𝑇 ≠ 0hop → ∃𝑣 ∈ HrmOp ( 0hop ≤op 𝑣 ∧ (𝑣 ∘ 𝑣) = 𝑇)) | ||
| Theorem | opsqrlem2 31083* | Lemma for opsqri . 𝐹‘𝑁 is the recursive function An (starting at n=1 instead of 0) of Theorem 9.4-2 of [Kreyszig] p. 476. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) ⇒ ⊢ (𝐹‘1) = 0hop | ||
| Theorem | opsqrlem3 31084* | Lemma for opsqri . (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) ⇒ ⊢ ((𝐺 ∈ HrmOp ∧ 𝐻 ∈ HrmOp) → (𝐺𝑆𝐻) = (𝐺 +op ((1 / 2) ·op (𝑇 −op (𝐺 ∘ 𝐺))))) | ||
| Theorem | opsqrlem4 31085* | Lemma for opsqri . (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) ⇒ ⊢ 𝐹:ℕ⟶HrmOp | ||
| Theorem | opsqrlem5 31086* | Lemma for opsqri . (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) ⇒ ⊢ (𝑁 ∈ ℕ → (𝐹‘(𝑁 + 1)) = ((𝐹‘𝑁) +op ((1 / 2) ·op (𝑇 −op ((𝐹‘𝑁) ∘ (𝐹‘𝑁)))))) | ||
| Theorem | opsqrlem6 31087* | Lemma for opsqri . (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥))))) & ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop })) & ⊢ 𝑇 ≤op Iop ⇒ ⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) ≤op Iop ) | ||
| Theorem | pjhmopi 31088 | A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ HrmOp | ||
| Theorem | pjlnopi 31089 | A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ LinOp | ||
| Theorem | pjnmopi 31090 | The operator norm of a projector on a nonzero closed subspace is one. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐻 ≠ 0ℋ → (normop‘(projℎ‘𝐻)) = 1) | ||
| Theorem | pjbdlni 31091 | A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ BndLinOp | ||
| Theorem | pjhmop 31092 | A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) ∈ HrmOp) | ||
| Theorem | hmopidmchi 31093 | An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64. (Contributed by NM, 21-Apr-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ (𝑇 ∘ 𝑇) = 𝑇 ⇒ ⊢ ran 𝑇 ∈ Cℋ | ||
| Theorem | hmopidmpji 31094 | An idempotent Hermitian operator is a projection operator. Theorem 26.4 of [Halmos] p. 44. (Halmos seems to omit the proof that 𝐻 is a closed subspace, which is not trivial as hmopidmchi 31093 shows.) (Contributed by NM, 22-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ (𝑇 ∘ 𝑇) = 𝑇 ⇒ ⊢ 𝑇 = (projℎ‘ran 𝑇) | ||
| Theorem | hmopidmch 31095 | An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇) → ran 𝑇 ∈ Cℋ ) | ||
| Theorem | hmopidmpj 31096 | An idempotent Hermitian operator is a projection operator. Theorem 26.4 of [Halmos] p. 44. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇) → 𝑇 = (projℎ‘ran 𝑇)) | ||
| Theorem | pjsdii 31097 | Distributive law for Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((projℎ‘𝐻) ∘ (𝑆 +op 𝑇)) = (((projℎ‘𝐻) ∘ 𝑆) +op ((projℎ‘𝐻) ∘ 𝑇)) | ||
| Theorem | pjddii 31098 | Distributive law for Hilbert space operator difference. (Contributed by NM, 24-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((projℎ‘𝐻) ∘ (𝑆 −op 𝑇)) = (((projℎ‘𝐻) ∘ 𝑆) −op ((projℎ‘𝐻) ∘ 𝑇)) | ||
| Theorem | pjsdi2i 31099 | Chained distributive law for Hilbert space operator difference. (Contributed by NM, 30-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 ∘ (𝑆 +op 𝑇)) = ((𝑅 ∘ 𝑆) +op (𝑅 ∘ 𝑇)) → (((projℎ‘𝐻) ∘ 𝑅) ∘ (𝑆 +op 𝑇)) = ((((projℎ‘𝐻) ∘ 𝑅) ∘ 𝑆) +op (((projℎ‘𝐻) ∘ 𝑅) ∘ 𝑇))) | ||
| Theorem | pjcoi 31100 | Composition of projections. (Contributed by NM, 16-Aug-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) = ((projℎ‘𝐺)‘((projℎ‘𝐻)‘𝐴))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |