P. 322 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32101-32200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lnopeq0lem1 32101	Lemma for lnopeq0i 32103. Apply the generalized polarization identity polid2i 31253 to the quadratic form ((𝑇‘𝑥), 𝑥). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih (𝐴 +ℎ 𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵)) ·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i ·ℎ 𝐵))) ·ih (𝐴 +ℎ (i ·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i ·ℎ 𝐵))) ·ih (𝐴 −ℎ (i ·ℎ 𝐵)))))) / 4)
Theorem	lnopeq0lem2 32102	Lemma for lnopeq0i 32103. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih (𝐴 +ℎ 𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵)) ·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i ·ℎ 𝐵))) ·ih (𝐴 +ℎ (i ·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i ·ℎ 𝐵))) ·ih (𝐴 −ℎ (i ·ℎ 𝐵)))))) / 4))
Theorem	lnopeq0i 32103*	A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 31924 for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form (𝑇‘𝑥) ·ih 𝑥). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ (∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ 𝑇 = 0hop )
Theorem	lnopeqi 32104*	Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑈 ∈ LinOp    ⇒   ⊢ (∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑥) = ((𝑈‘𝑥) ·ih 𝑥) ↔ 𝑇 = 𝑈)
Theorem	lnopeq 32105*	Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinOp ∧ 𝑈 ∈ LinOp) → (∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑥) = ((𝑈‘𝑥) ·ih 𝑥) ↔ 𝑇 = 𝑈))
Theorem	lnopunilem1 32106*	Lemma for lnopunii 32108. (Contributed by NM, 14-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·ih 𝐵)))
Theorem	lnopunilem2 32107*	Lemma for lnopunii 32108. (Contributed by NM, 12-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵)
Theorem	lnopunii 32108*	If a linear operator (whose range is ℋ) is idempotent in the norm, the operator is unitary. Similar to theorem in [AkhiezerGlazman] p. 73. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇: ℋ–onto→ ℋ    &   ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)    ⇒   ⊢ 𝑇 ∈ UniOp
Theorem	elunop2 32109*	An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in [AkhiezerGlazman] p. 73, and its converse. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp ↔ (𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)))
Theorem	nmopun 32110	Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (normop‘𝑇) = 1)
Theorem	unopbd 32111	A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp)
Theorem	lnophmlem1 32112*	Lemma for lnophmi 32114. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ    ⇒   ⊢ (𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ
Theorem	lnophmlem2 32113*	Lemma for lnophmi 32114. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ    ⇒   ⊢ (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵)
Theorem	lnophmi 32114*	A linear operator is Hermitian if 𝑥 ·ih (𝑇‘𝑥) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ    ⇒   ⊢ 𝑇 ∈ HrmOp
Theorem	lnophm 32115*	A linear operator is Hermitian if 𝑥 ·ih (𝑇‘𝑥) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ) → 𝑇 ∈ HrmOp)
Theorem	hmops 32116	The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp)
Theorem	hmopm 32117	The scalar product of a Hermitian operator with a real is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) → (𝐴 ·op 𝑇) ∈ HrmOp)
Theorem	hmopd 32118	The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 −op 𝑈) ∈ HrmOp)
Theorem	hmopco 32119	The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp)
Theorem	nmbdoplbi 32120	A lower bound for the norm of a bounded linear operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝐴 ∈ ℋ → (normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴)))
Theorem	nmbdoplb 32121	A lower bound for the norm of a bounded linear Hilbert space operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ BndLinOp ∧ 𝐴 ∈ ℋ) → (normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴)))
Theorem	nmcexi 32122*	Lemma for nmcopexi 32123 and nmcfnexi 32147. The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by Mario Carneiro, 17-Nov-2013.) (Proof shortened by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)    &   ⊢ (𝑆‘𝑇) = sup({𝑚 ∣ ∃𝑥 ∈ ℋ ((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, < )    &   ⊢ (𝑥 ∈ ℋ → (𝑁‘(𝑇‘𝑥)) ∈ ℝ)    &   ⊢ (𝑁‘(𝑇‘0ℎ)) = 0    &   ⊢ (((𝑦 / 2) ∈ ℝ+ ∧ 𝑥 ∈ ℋ) → ((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ 𝑥))))    ⇒   ⊢ (𝑆‘𝑇) ∈ ℝ
Theorem	nmcopexi 32123	The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 5-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    ⇒   ⊢ (normop‘𝑇) ∈ ℝ
Theorem	nmcoplbi 32124	A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    ⇒   ⊢ (𝐴 ∈ ℋ → (normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴)))
Theorem	nmcopex 32125	The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp) → (normop‘𝑇) ∈ ℝ)
Theorem	nmcoplb 32126	A lower bound for the norm of a continuous linear Hilbert space operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ∧ 𝐴 ∈ ℋ) → (normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴)))
Theorem	nmophmi 32127	The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝐴 ∈ ℂ → (normop‘(𝐴 ·op 𝑇)) = ((abs‘𝐴) · (normop‘𝑇)))
Theorem	bdophmi 32128	The scalar product of a bounded linear operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝐴 ∈ ℂ → (𝐴 ·op 𝑇) ∈ BndLinOp)
Theorem	lnconi 32129*	Lemma for lnopconi 32130 and lnfnconi 32151. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ 𝐶 → 𝑆 ∈ ℝ)    &   ⊢ ((𝑇 ∈ 𝐶 ∧ 𝑦 ∈ ℋ) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 · (normℎ‘𝑦)))    &   ⊢ (𝑇 ∈ 𝐶 ↔ ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧))    &   ⊢ (𝑦 ∈ ℋ → (𝑁‘(𝑇‘𝑦)) ∈ ℝ)    &   ⊢ ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘(𝑤 −ℎ 𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥)))    ⇒   ⊢ (𝑇 ∈ 𝐶 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦)))
Theorem	lnopconi 32130*	A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ (𝑇 ∈ ContOp ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (normℎ‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦)))
Theorem	lnopcon 32131*	A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (normℎ‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦))))
Theorem	lnopcnbd 32132	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp))
Theorem	lncnopbd 32133	A continuous linear operator is a bounded linear operator. This theorem justifies our use of "bounded linear" as an interchangeable condition for "continuous linear" used in some textbook proofs. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinOp ∩ ContOp) ↔ 𝑇 ∈ BndLinOp)
Theorem	lncnbd 32134	A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ (LinOp ∩ ContOp) = BndLinOp
Theorem	lnopcnre 32135	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ (normop‘𝑇) ∈ ℝ))
Theorem	lnfnli 32136	Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶)))
Theorem	lnfnfi 32137	A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ 𝑇: ℋ⟶ℂ
Theorem	lnfn0i 32138	The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ (𝑇‘0ℎ) = 0
Theorem	lnfnaddi 32139	Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵)))
Theorem	lnfnmuli 32140	Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵)))
Theorem	lnfnaddmuli 32141	Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) + (𝐴 · (𝑇‘𝐶))))
Theorem	lnfnsubi 32142	Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) − (𝑇‘𝐵)))
Theorem	lnfn0 32143	The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → (𝑇‘0ℎ) = 0)
Theorem	lnfnmul 32144	Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵)))
Theorem	nmbdfnlbi 32145	A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ)    ⇒   ⊢ (𝐴 ∈ ℋ → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) · (normℎ‘𝐴)))
Theorem	nmbdfnlb 32146	A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ ∧ 𝐴 ∈ ℋ) → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) · (normℎ‘𝐴)))
Theorem	nmcfnexi 32147	The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    &   ⊢ 𝑇 ∈ ContFn    ⇒   ⊢ (normfn‘𝑇) ∈ ℝ
Theorem	nmcfnlbi 32148	A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    &   ⊢ 𝑇 ∈ ContFn    ⇒   ⊢ (𝐴 ∈ ℋ → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) · (normℎ‘𝐴)))
Theorem	nmcfnex 32149	The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn) → (normfn‘𝑇) ∈ ℝ)
Theorem	nmcfnlb 32150	A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ∧ 𝐴 ∈ ℋ) → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) · (normℎ‘𝐴)))
Theorem	lnfnconi 32151*	A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ (𝑇 ∈ ContFn ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (abs‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦)))
Theorem	lnfncon 32152*	A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → (𝑇 ∈ ContFn ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (abs‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦))))
Theorem	lnfncnbd 32153	A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → (𝑇 ∈ ContFn ↔ (normfn‘𝑇) ∈ ℝ))
Theorem	imaelshi 32154	The image of a subspace under a linear operator is a subspace. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝐴 ∈ Sℋ    ⇒   ⊢ (𝑇 “ 𝐴) ∈ Sℋ
Theorem	rnelshi 32155	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 32156	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 32157	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ℋ
20.6.11  Riesz lemma
Theorem	riesz3i 32158*	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 32159*	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 32160*	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 32162 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤))
Theorem	riesz1 32161*	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 32162. For the continuous linear functional version, see riesz3i 32158 and riesz4 32160. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → ((normfn‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)))
Theorem	riesz2 32162*	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 32161. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))
20.6.12  Adjoints (cont.)
Theorem	cnlnadjlem1 32163*	Lemma for cnlnadji 32172 (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 32164*	Lemma for cnlnadji 32172. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    ⇒   ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
Theorem	cnlnadjlem3 32165*	Lemma for cnlnadji 32172. By riesz4 32160, 𝐵 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 32166*	Lemma for cnlnadji 32172. 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 32167*	Lemma for cnlnadji 32172. 𝐹 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 32168*	Lemma for cnlnadji 32172. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ LinOp
Theorem	cnlnadjlem7 32169*	Lemma for cnlnadji 32172. 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 32170*	Lemma for cnlnadji 32172. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ ContOp
Theorem	cnlnadjlem9 32171*	Lemma for cnlnadji 32172. 𝐹 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 32172*	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 32173*	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 32174*	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 32175*	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 32176	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 32177	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ BndLinOp ⊆ dom adjℎ
Theorem	bdopadj 32178	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ)
Theorem	adjbdln 32179	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 32180	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 32181	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 32182	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 32183	Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
⊢ dom adjℎ ⊆ LinOp
Theorem	nmopadjlei 32184	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 32185	Lemma for nmopadji 32186. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘(adjℎ‘𝑇)) ≤ (normop‘𝑇)
Theorem	nmopadji 32186	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 32187	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 32188	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 32189	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 32190	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 32191	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 32192	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 32193	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 32194	The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp
Theorem	nmoptri2i 32195	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 32196	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 32197	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 32198	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 32199	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 )
20.6.13  Quantum computation error bound theorem
Theorem	unierri 32200	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 𝑇)))