Theorem leopnmid

Description: A bounded Hermitian operator is less than or equal to its norm times the identity operator. (Contributed by NM, 11-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	leopnmid	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) → 𝑇 ≤op ( ( normop ‘ 𝑇 ) ·op Iop ) )

Proof

Step	Hyp	Ref	Expression
1		hmopre	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
2	1	adantlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
3	1	recnd	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℂ )
4	3	abscld	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ∈ ℝ )
5	4	adantlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ∈ ℝ )
6		idhmop	⊢ Iop ∈ HrmOp
7		hmopm	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ Iop ∈ HrmOp ) → ( ( normop ‘ 𝑇 ) ·op Iop ) ∈ HrmOp )
8	6 7	mpan2	⊢ ( ( normop ‘ 𝑇 ) ∈ ℝ → ( ( normop ‘ 𝑇 ) ·op Iop ) ∈ HrmOp )
9		hmopre	⊢ ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
10	8 9	sylan	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 𝑥 ∈ ℋ ) → ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
11	10	adantll	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
12	1	leabsd	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )
13	12	adantlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )
14		hmopf	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
15		ffvelcdm	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
16		normcl	⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
17	15 16	syl	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
18	14 17	sylan	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
19	18	adantlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
20		normcl	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℝ )
21	20	adantl	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ 𝑥 ) ∈ ℝ )
22	19 21	remulcld	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) ∈ ℝ )
23	14 15	sylan	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
24		bcs	⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ≤ ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) )
25	23 24	sylancom	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ≤ ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) )
26	25	adantlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ≤ ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) )
27		remulcl	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normℎ ‘ 𝑥 ) ∈ ℝ ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) ∈ ℝ )
28	20 27	sylan2	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 𝑥 ∈ ℋ ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) ∈ ℝ )
29	28	adantll	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) ∈ ℝ )
30		normge0	⊢ ( 𝑥 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝑥 ) )
31	20 30	jca	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝑥 ) ) )
32	31	adantl	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝑥 ) ) )
33		hmoplin	⊢ ( 𝑇 ∈ HrmOp → 𝑇 ∈ LinOp )
34		elbdop2	⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) )
35	34	biimpri	⊢ ( ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) → 𝑇 ∈ BndLinOp )
36	33 35	sylan	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) → 𝑇 ∈ BndLinOp )
37		nmbdoplb	⊢ ( ( 𝑇 ∈ BndLinOp ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) )
38	36 37	sylan	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) )
39		lemul1a	⊢ ( ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) ∈ ℝ ∧ ( ( normℎ ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝑥 ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) )
40	19 29 32 38 39	syl31anc	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) )
41		recn	⊢ ( ( normop ‘ 𝑇 ) ∈ ℝ → ( normop ‘ 𝑇 ) ∈ ℂ )
42	41	ad2antlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( normop ‘ 𝑇 ) ∈ ℂ )
43	21	recnd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ 𝑥 ) ∈ ℂ )
44	42 43 43	mulassd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) = ( ( normop ‘ 𝑇 ) · ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑥 ) ) ) )
45		simpr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → 𝑥 ∈ ℋ )
46		ax-his3	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) ·ℎ 𝑥 ) ·ih 𝑥 ) = ( ( normop ‘ 𝑇 ) · ( 𝑥 ·ih 𝑥 ) ) )
47	42 45 45 46	syl3anc	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) ·ℎ 𝑥 ) ·ih 𝑥 ) = ( ( normop ‘ 𝑇 ) · ( 𝑥 ·ih 𝑥 ) ) )
48	20	recnd	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℂ )
49	48	sqvald	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) ↑ 2 ) = ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑥 ) ) )
50		normsq	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) ↑ 2 ) = ( 𝑥 ·ih 𝑥 ) )
51	49 50	eqtr3d	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑥 ) ) = ( 𝑥 ·ih 𝑥 ) )
52	51	oveq2d	⊢ ( 𝑥 ∈ ℋ → ( ( normop ‘ 𝑇 ) · ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑥 ) ) ) = ( ( normop ‘ 𝑇 ) · ( 𝑥 ·ih 𝑥 ) ) )
53	52	adantl	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( normop ‘ 𝑇 ) · ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑥 ) ) ) = ( ( normop ‘ 𝑇 ) · ( 𝑥 ·ih 𝑥 ) ) )
54	47 53	eqtr4d	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) ·ℎ 𝑥 ) ·ih 𝑥 ) = ( ( normop ‘ 𝑇 ) · ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑥 ) ) ) )
55	44 54	eqtr4d	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) = ( ( ( normop ‘ 𝑇 ) ·ℎ 𝑥 ) ·ih 𝑥 ) )
56		hoif	⊢ Iop : ℋ –1-1-onto→ ℋ
57		f1of	⊢ ( Iop : ℋ –1-1-onto→ ℋ → Iop : ℋ ⟶ ℋ )
58	56 57	mp1i	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → Iop : ℋ ⟶ ℋ )
59		homval	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ Iop : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) = ( ( normop ‘ 𝑇 ) ·ℎ ( Iop ‘ 𝑥 ) ) )
60	42 58 45 59	syl3anc	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) = ( ( normop ‘ 𝑇 ) ·ℎ ( Iop ‘ 𝑥 ) ) )
61		hoival	⊢ ( 𝑥 ∈ ℋ → ( Iop ‘ 𝑥 ) = 𝑥 )
62	61	oveq2d	⊢ ( 𝑥 ∈ ℋ → ( ( normop ‘ 𝑇 ) ·ℎ ( Iop ‘ 𝑥 ) ) = ( ( normop ‘ 𝑇 ) ·ℎ 𝑥 ) )
63	62	adantl	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( normop ‘ 𝑇 ) ·ℎ ( Iop ‘ 𝑥 ) ) = ( ( normop ‘ 𝑇 ) ·ℎ 𝑥 ) )
64	60 63	eqtrd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) = ( ( normop ‘ 𝑇 ) ·ℎ 𝑥 ) )
65	64	oveq1d	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( normop ‘ 𝑇 ) ·ℎ 𝑥 ) ·ih 𝑥 ) )
66	55 65	eqtr4d	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) = ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) )
67	40 66	breqtrd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) ≤ ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) )
68	5 22 11 26 67	letrd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ≤ ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) )
69	2 5 11 13 68	letrd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) )
70	69	ralrimiva	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) → ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) )
71		leop2	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( ( normop ‘ 𝑇 ) ·op Iop ) ∈ HrmOp ) → ( 𝑇 ≤op ( ( normop ‘ 𝑇 ) ·op Iop ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
72	8 71	sylan2	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) → ( 𝑇 ≤op ( ( normop ‘ 𝑇 ) ·op Iop ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( ( ( normop ‘ 𝑇 ) ·op Iop ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
73	70 72	mpbird	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) → 𝑇 ≤op ( ( normop ‘ 𝑇 ) ·op Iop ) )