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	$⊢ (T \in HrmOp \land {norm}_{op} (T) \in ℝ) \to T \leq_{op} ({norm}_{op} (T) \cdot_{op} I_{op})$

Proof

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

Metamath Proof Explorer

Theorem leopnmid

Proof