Theorem nmopleid

Description: 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.)

	Ref	Expression
Assertion	nmopleid	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ∧ 𝑇 ≠ 0hop ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ≤op Iop )

Proof

Step	Hyp	Ref	Expression
1		hmoplin	⊢ ( 𝑇 ∈ HrmOp → 𝑇 ∈ LinOp )
2		nmlnopne0	⊢ ( 𝑇 ∈ LinOp → ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 𝑇 ≠ 0hop ) )
3	2	biimpar	⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ≠ 0hop ) → ( normop ‘ 𝑇 ) ≠ 0 )
4	1 3	sylan	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑇 ≠ 0hop ) → ( normop ‘ 𝑇 ) ≠ 0 )
5	4	adantlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑇 ≠ 0hop ) → ( normop ‘ 𝑇 ) ≠ 0 )
6		rereccl	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ )
7	6	adantll	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ )
8		simpll	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 𝑇 ∈ HrmOp )
9		idhmop	⊢ Iop ∈ HrmOp
10		hmopm	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ Iop ∈ HrmOp ) → ( ( normop ‘ 𝑇 ) ·op Iop ) ∈ HrmOp )
11	9 10	mpan2	⊢ ( ( normop ‘ 𝑇 ) ∈ ℝ → ( ( normop ‘ 𝑇 ) ·op Iop ) ∈ HrmOp )
12	11	ad2antlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normop ‘ 𝑇 ) ·op Iop ) ∈ HrmOp )
13		simplr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( normop ‘ 𝑇 ) ∈ ℝ )
14		hmopf	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
15		nmopgt0	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 0 < ( normop ‘ 𝑇 ) ) )
16	15	biimpa	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 0 < ( normop ‘ 𝑇 ) )
17	14 16	sylan	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 0 < ( normop ‘ 𝑇 ) )
18	17	adantlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 0 < ( normop ‘ 𝑇 ) )
19	13 18	recgt0d	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 0 < ( 1 / ( normop ‘ 𝑇 ) ) )
20		0re	⊢ 0 ∈ ℝ
21		ltle	⊢ ( ( 0 ∈ ℝ ∧ ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ ) → ( 0 < ( 1 / ( normop ‘ 𝑇 ) ) → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) ) )
22	20 6 21	sylancr	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( 0 < ( 1 / ( normop ‘ 𝑇 ) ) → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) ) )
23	22	adantll	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( 0 < ( 1 / ( normop ‘ 𝑇 ) ) → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) ) )
24	19 23	mpd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) )
25		leopnmid	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) → 𝑇 ≤op ( ( normop ‘ 𝑇 ) ·op Iop ) )
26	25	adantr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 𝑇 ≤op ( ( normop ‘ 𝑇 ) ·op Iop ) )
27		leopmul2i	⊢ ( ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ ( ( normop ‘ 𝑇 ) ·op Iop ) ∈ HrmOp ) ∧ ( 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) ∧ 𝑇 ≤op ( ( normop ‘ 𝑇 ) ·op Iop ) ) ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ≤op ( ( 1 / ( normop ‘ 𝑇 ) ) ·op ( ( normop ‘ 𝑇 ) ·op Iop ) ) )
28	7 8 12 24 26 27	syl32anc	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ≤op ( ( 1 / ( normop ‘ 𝑇 ) ) ·op ( ( normop ‘ 𝑇 ) ·op Iop ) ) )
29		recn	⊢ ( ( normop ‘ 𝑇 ) ∈ ℝ → ( normop ‘ 𝑇 ) ∈ ℂ )
30		reccl	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ )
31		simpl	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( normop ‘ 𝑇 ) ∈ ℂ )
32		hoif	⊢ Iop : ℋ –1-1-onto→ ℋ
33		f1of	⊢ ( Iop : ℋ –1-1-onto→ ℋ → Iop : ℋ ⟶ ℋ )
34	32 33	ax-mp	⊢ Iop : ℋ ⟶ ℋ
35		homulass	⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ∈ ℂ ∧ Iop : ℋ ⟶ ℋ ) → ( ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normop ‘ 𝑇 ) ) ·op Iop ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·op ( ( normop ‘ 𝑇 ) ·op Iop ) ) )
36	34 35	mp3an3	⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ∈ ℂ ) → ( ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normop ‘ 𝑇 ) ) ·op Iop ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·op ( ( normop ‘ 𝑇 ) ·op Iop ) ) )
37	30 31 36	syl2anc	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normop ‘ 𝑇 ) ) ·op Iop ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·op ( ( normop ‘ 𝑇 ) ·op Iop ) ) )
38		recid2	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normop ‘ 𝑇 ) ) = 1 )
39	38	oveq1d	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normop ‘ 𝑇 ) ) ·op Iop ) = ( 1 ·op Iop ) )
40	37 39	eqtr3d	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op ( ( normop ‘ 𝑇 ) ·op Iop ) ) = ( 1 ·op Iop ) )
41		homulid2	⊢ ( Iop : ℋ ⟶ ℋ → ( 1 ·op Iop ) = Iop )
42	34 41	ax-mp	⊢ ( 1 ·op Iop ) = Iop
43	40 42	syl6eq	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op ( ( normop ‘ 𝑇 ) ·op Iop ) ) = Iop )
44	29 43	sylan	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op ( ( normop ‘ 𝑇 ) ·op Iop ) ) = Iop )
45	44	adantll	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op ( ( normop ‘ 𝑇 ) ·op Iop ) ) = Iop )
46	28 45	breqtrd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ≤op Iop )
47	5 46	syldan	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑇 ≠ 0hop ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ≤op Iop )
48	47	3impa	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ∧ 𝑇 ≠ 0hop ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ≤op Iop )