HomeTheorem List (p. 328 of 512)
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. 328 of 512) | < 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-31525) |
Hilbert Space Explorer
(31526-33048) |
Users' Mathboxes
(33049-51158) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nmoptrii 32701 | 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 32702 | 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 32703 | 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 32704 | 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 32705 | The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ BndLinOp & ⊢ 𝑇 ∈ BndLinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp | ||
| Theorem | nmoptri2i 32706 | 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 32707 | 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 32708 | 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 32709 | 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 32710 | 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 32711 | 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 32712 | The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴)) | ||
| Theorem | brabn 32713 | The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ) | ||
| Theorem | rnbra 32714 | 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 32715 | 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 32716 | A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ (LinFn ∩ ContFn)) | ||
| Theorem | cnvbraval 32717* | Value of the converse of the bra function. Based on the Riesz Lemma riesz4 32671, 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 32718 | Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) ∈ ℋ) | ||
| Theorem | cnvbrabra 32719 | 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 32720 | 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 32721* | 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 32722 | Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ (LinFn ∩ ContFn)) → (◡bra‘(𝐴 ·fn 𝑇)) = ((∗‘𝐴) ·ℎ (◡bra‘𝑇))) | ||
| Theorem | kbass1 32723 | 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 32724 | 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 32725 | Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = (⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ ) ∣ 𝐷⟩. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶))‘𝐷)) | ||
| Theorem | kbass4 32726 | Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = ⟨𝐴 ∣ ( ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((bra‘𝐴)‘(((bra‘𝐶)‘𝐷) ·ℎ 𝐵))) | ||
| Theorem | kbass5 32727 | Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = (( ∣ 𝐴⟩⟨𝐵 ∣ ) ∣ 𝐶⟩)⟨𝐷 ∣. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (((𝐴 ketbra 𝐵)‘𝐶) ketbra 𝐷)) | ||
| Theorem | kbass6 32728 | Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = ∣ 𝐴⟩(⟨𝐵 ∣ ( ∣ 𝐶⟩⟨𝐷 ∣ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (𝐴 ketbra (◡bra‘((bra‘𝐵) ∘ (𝐶 ketbra 𝐷))))) | ||
| Theorem | leopg 32729* | 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 32730* | 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 32731* | 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 32732 | 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 32733* | 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 32734 | The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → 𝑇 ≤op 𝑇) | ||
| Theorem | leoprf 32735 | The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → 𝑇 ≤op 𝑇) | ||
| Theorem | leopsq 32736 | The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → 0hop ≤op (𝑇 ∘ 𝑇)) | ||
| Theorem | 0leop 32737 | 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 32738 | 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 32739 | 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 32740 | 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 32741 | 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 32742 | 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 32743 | 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 32744 | 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 32745 | 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 32746 | 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 32747* | 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 32748* | 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 32749* | 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 32750* | 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 32751* | 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 32752* | 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 32753 | A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ HrmOp | ||
| Theorem | pjlnopi 32754 | A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ LinOp | ||
| Theorem | pjnmopi 32755 | 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 32756 | A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) ∈ BndLinOp | ||
| Theorem | pjhmop 32757 | A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) ∈ HrmOp) | ||
| Theorem | hmopidmchi 32758 | 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 32759 | 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 32758 shows.) (Contributed by NM, 22-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ HrmOp & ⊢ (𝑇 ∘ 𝑇) = 𝑇 ⇒ ⊢ 𝑇 = (projℎ‘ran 𝑇) | ||
| Theorem | hmopidmch 32760 | 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 32761 | 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 32762 | 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 32763 | 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 32764 | 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 32765 | Composition of projections. (Contributed by NM, 16-Aug-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) = ((projℎ‘𝐺)‘((projℎ‘𝐻)‘𝐴))) | ||
| Theorem | pjcocli 32766 | Closure of composition of projections. (Contributed by NM, 29-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ∈ 𝐺) | ||
| Theorem | pjcohcli 32767 | Closure of composition of projections. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ∈ ℋ) | ||
| Theorem | pjadjcoi 32768 | 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 32769 | Functionality of composition of projections. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) Fn ℋ | ||
| Theorem | pjss1coi 32770 | 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 32771 | 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 32772 | 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 32773 | 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 32774 | 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 32775* | 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 32776 | 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 32777 | 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 32778 | 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 32779* | 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 32780* | 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 32779). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (∀𝑥 ∈ ℋ 0 ≤ ((((projℎ‘𝐻) −op (projℎ‘𝐺))‘𝑥) ·ih 𝑥) ↔ ((projℎ‘𝐺) “ ℋ) ⊆ ((projℎ‘𝐻) “ ℋ)) | ||
| Theorem | pjssdif2i 32781 | The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 32779). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) −op (projℎ‘𝐺)) = (projℎ‘(𝐻 ∩ (⊥‘𝐺)))) | ||
| Theorem | pjssdif1i 32782 | 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 32779). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) −op (projℎ‘𝐺)) ∈ ran projℎ) | ||
| Theorem | pjimai 32783 | 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 32784 | 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 32785 | 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 32786 | 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 32787 | 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 32788 | 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 32789 | Definition of projection operator in [Hughes] p. 47, except that we do not need linearity to be explicit by virtue of hmoplin 32549. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ ran projℎ ↔ (𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇)) | ||
| Theorem | pjhmopidm 32790 | 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 32791 | 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 32792 | 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 32793 | A projector is a positive operator. (Contributed by NM, 27-Sep-2008.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ ran projℎ → 0hop ≤op 𝑇) | ||
| Theorem | pjadj2 32794 | 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 32795 | 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 32796 | 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 32797* | 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 32798 | 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 32799 | 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 32800 | 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ℎ‘𝐻)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |