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 ‘ 𝑇 )