Metamath Proof Explorer

Theorem nmopnegi

Description: Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi , the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopneg.1 ⊢ T : ℋ ⟶ ℋ
Assertion nmopnegi ⊢ norm op ⁡ -1 · op T = norm op ⁡ T

Proof

Step Hyp Ref Expression
1 nmopneg.1 ⊢ T : ℋ ⟶ ℋ
2 neg1cn ⊢ − 1 ∈ ℂ
3 homval ⊢ − 1 ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → -1 · op T ⁡ y = -1 ⋅ ℎ T ⁡ y
4 2 1 3 mp3an12 ⊢ y ∈ ℋ → -1 · op T ⁡ y = -1 ⋅ ℎ T ⁡ y
5 4 fveq2d ⊢ y ∈ ℋ → norm ℎ ⁡ -1 · op T ⁡ y = norm ℎ ⁡ -1 ⋅ ℎ T ⁡ y
6 1 ffvelrni ⊢ y ∈ ℋ → T ⁡ y ∈ ℋ
7 normneg ⊢ T ⁡ y ∈ ℋ → norm ℎ ⁡ -1 ⋅ ℎ T ⁡ y = norm ℎ ⁡ T ⁡ y
8 6 7 syl ⊢ y ∈ ℋ → norm ℎ ⁡ -1 ⋅ ℎ T ⁡ y = norm ℎ ⁡ T ⁡ y
9 5 8 eqtrd ⊢ y ∈ ℋ → norm ℎ ⁡ -1 · op T ⁡ y = norm ℎ ⁡ T ⁡ y
10 9 eqeq2d ⊢ y ∈ ℋ → x = norm ℎ ⁡ -1 · op T ⁡ y ↔ x = norm ℎ ⁡ T ⁡ y
11 10 anbi2d ⊢ y ∈ ℋ → norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ -1 · op T ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y
12 11 rexbiia ⊢ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ -1 · op T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y
13 12 abbii ⊢ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ -1 · op T ⁡ y = x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y
14 13 supeq1i ⊢ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ -1 · op T ⁡ y ℝ * < = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
15 homulcl ⊢ − 1 ∈ ℂ ∧ T : ℋ ⟶ ℋ → -1 · op T : ℋ ⟶ ℋ
16 2 1 15 mp2an ⊢ -1 · op T : ℋ ⟶ ℋ
17 nmopval ⊢ -1 · op T : ℋ ⟶ ℋ → norm op ⁡ -1 · op T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ -1 · op T ⁡ y ℝ * <
18 16 17 ax-mp ⊢ norm op ⁡ -1 · op T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ -1 · op T ⁡ y ℝ * <
19 nmopval ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
20 1 19 ax-mp ⊢ norm op ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
21 14 18 20 3eqtr4i ⊢ norm op ⁡ -1 · op T = norm op ⁡ T