This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion nmopnegi ( normop ‘ ( - 1 ·op 𝑇 ) ) = ( normop ‘ 𝑇 )

Proof

Step Hyp Ref Expression
1 nmopneg.1 ⊢ 𝑇 : ℋ ⟶ ℋ
2 neg1cn ⊢ - 1 ∈ ℂ
3 homval ⊢ ( ( - 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) = ( - 1 ·ℎ ( 𝑇 ‘ 𝑦 ) ) )
4 2 1 3 mp3an12 ⊢ ( 𝑦 ∈ ℋ → ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) = ( - 1 ·ℎ ( 𝑇 ‘ 𝑦 ) ) )
5 4 fveq2d ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) ) = ( normℎ ‘ ( - 1 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) )
6 1 ffvelcdmi ⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
7 normneg ⊢ ( ( 𝑇 ‘ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( - 1 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) )
8 6 7 syl ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( - 1 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) )
9 5 8 eqtrd ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) )
10 9 eqeq2d ⊢ ( 𝑦 ∈ ℋ → ( 𝑥 = ( normℎ ‘ ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) ) ↔ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
11 10 anbi2d ⊢ ( 𝑦 ∈ ℋ → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
12 11 rexbiia ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
13 12 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) ) ) } = { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) }
14 13 supeq1i ⊢ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) ) ) } , ℝ* , < ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < )
15 homulcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ )
16 2 1 15 mp2an ⊢ ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ
17 nmopval ⊢ ( ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ → ( normop ‘ ( - 1 ·op 𝑇 ) ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) ) ) } , ℝ* , < ) )
18 16 17 ax-mp ⊢ ( normop ‘ ( - 1 ·op 𝑇 ) ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( - 1 ·op 𝑇 ) ‘ 𝑦 ) ) ) } , ℝ* , < )
19 nmopval ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
20 1 19 ax-mp ⊢ ( normop ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < )
21 14 18 20 3eqtr4i ⊢ ( normop ‘ ( - 1 ·op 𝑇 ) ) = ( normop ‘ 𝑇 )