Theorem leopnmidt 9982

Description: A bounded Hermitian operator is less than or equal to its norm times the identity operator.

Assertion

Ref	Expression
leopnmidt	|- ((T e. HrmOp /\ (normop` T) e. RR) -> T <_op ((normop` T) .op Iop ))

Proof of Theorem leopnmidt

Step	Hyp	Ref	Expression
1		hmopret 9763	. . . . 5 |- ((T e. HrmOp /\ x e. H~) -> ((T` x) .ih x) e. RR)
2	1	adantlr 393	. . . 4 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> ((T` x) .ih x) e. RR)
3	1	recnd 5287	. . . . . 6 |- ((T e. HrmOp /\ x e. H~) -> ((T` x) .ih x) e. CC)
4		absclt 6768	. . . . . 6 |- (((T` x) .ih x) e. CC -> (abs` ((T` x) .ih x)) e. RR)
5	3, 4	syl 10	. . . . 5 |- ((T e. HrmOp /\ x e. H~) -> (abs` ((T` x) .ih x)) e. RR)
6	5	adantlr 393	. . . 4 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (abs` ((T` x) .ih x)) e. RR)
7		hmopret 9763	. . . . . 6 |- ((((normop` T) .op Iop ) e. HrmOp /\ x e. H~) -> ((((normop` T) .op Iop )` x) .ih x) e. RR)
8		idhmop 9822	. . . . . . 7 |- Iop e. HrmOp
9		hmopmt 9861	. . . . . . 7 |- (((normop` T) e. RR /\ Iop e. HrmOp) -> ((normop` T) .op Iop ) e. HrmOp)
10	8, 9	mpan2 694	. . . . . 6 |- ((normop` T) e. RR -> ((normop` T) .op Iop ) e. HrmOp)
11	7, 10	sylan 448	. . . . 5 |- (((normop` T) e. RR /\ x e. H~) -> ((((normop` T) .op Iop )` x) .ih x) e. RR)
12	11	adantll 392	. . . 4 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> ((((normop` T) .op Iop )` x) .ih x) e. RR)
13		leabst 6799	. . . . . 6 |- (((T` x) .ih x) e. RR -> ((T` x) .ih x) <_ (abs` ((T` x) .ih x)))
14	1, 13	syl 10	. . . . 5 |- ((T e. HrmOp /\ x e. H~) -> ((T` x) .ih x) <_ (abs` ((T` x) .ih x)))
15	14	adantlr 393	. . . 4 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> ((T` x) .ih x) <_ (abs` ((T` x) .ih x)))
16		axmulrcl 5246	. . . . . 6 |- (((normh` (T` x)) e. RR /\ (normh` x) e. RR) -> ((normh` (T` x)) x. (normh` x)) e. RR)
17		ffvelrn 3799	. . . . . . . . 9 |- ((T:H~-->H~ /\ x e. H~) -> (T` x) e. H~)
18		normclt 8912	. . . . . . . . 9 |- ((T` x) e. H~ -> (normh` (T` x)) e. RR)
19	17, 18	syl 10	. . . . . . . 8 |- ((T:H~-->H~ /\ x e. H~) -> (normh` (T` x)) e. RR)
20		hmopft 9718	. . . . . . . 8 |- (T e. HrmOp -> T:H~-->H~)
21	19, 20	sylan 448	. . . . . . 7 |- ((T e. HrmOp /\ x e. H~) -> (normh` (T` x)) e. RR)
22	21	adantlr 393	. . . . . 6 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (normh` (T` x)) e. RR)
23		normclt 8912	. . . . . . 7 |- (x e. H~ -> (normh` x) e. RR)
24	23	adantl 388	. . . . . 6 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (normh` x) e. RR)
25	16, 22, 24	sylanc 471	. . . . 5 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> ((normh` (T` x)) x. (normh` x)) e. RR)
26		bcst 8969	. . . . . . 7 |- (((T` x) e. H~ /\ x e. H~) -> (abs` ((T` x) .ih x)) <_ ((normh` (T` x)) x. (normh` x)))
27	17, 20	sylan 448	. . . . . . 7 |- ((T e. HrmOp /\ x e. H~) -> (T` x) e. H~)
28		pm3.27 323	. . . . . . 7 |- ((T e. HrmOp /\ x e. H~) -> x e. H~)
29	26, 27, 28	sylanc 471	. . . . . 6 |- ((T e. HrmOp /\ x e. H~) -> (abs` ((T` x) .ih x)) <_ ((normh` (T` x)) x. (normh` x)))
30	29	adantlr 393	. . . . 5 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (abs` ((T` x) .ih x)) <_ ((normh` (T` x)) x. (normh` x)))
31		lemul1itOLD 5794	. . . . . . 7 |- ((((normh` (T` x)) e. RR /\ ((normop` T) x. (normh` x)) e. RR /\ (normh` x) e. RR) /\ (0 <_ (normh` x) /\ (normh` (T` x)) <_ ((normop` T) x. (normh` x)))) -> ((normh` (T` x)) x. (normh` x)) <_ (((normop` T) x. (normh` x)) x. (normh` x)))
32		axmulrcl 5246	. . . . . . . . 9 |- (((normop` T) e. RR /\ (normh` x) e. RR) -> ((normop` T) x. (normh` x)) e. RR)
33		pm3.27 323	. . . . . . . . 9 |- ((T e. HrmOp /\ (normop` T) e. RR) -> (normop` T) e. RR)
34	32, 33, 23	syl2an 454	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> ((normop` T) x. (normh` x)) e. RR)
35	22, 34, 24	3jca 817	. . . . . . 7 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> ((normh` (T` x)) e. RR /\ ((normop` T) x. (normh` x)) e. RR /\ (normh` x) e. RR))
36		normge0t 8913	. . . . . . . . 9 |- (x e. H~ -> 0 <_ (normh` x))
37	36	adantl 388	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> 0 <_ (normh` x))
38		nmbdoplbt 9865	. . . . . . . . 9 |- ((T e. BndLinOp /\ x e. H~) -> (normh` (T` x)) <_ ((normop` T) x. (normh` x)))
39		elbdop2t 9715	. . . . . . . . . . 11 |- (T e. BndLinOp <-> (T e. LinOp /\ (normop` T) e. RR))
40	39	biimpr 152	. . . . . . . . . 10 |- ((T e. LinOp /\ (normop` T) e. RR) -> T e. BndLinOp)
41		hmoplint 9782	. . . . . . . . . 10 |- (T e. HrmOp -> T e. LinOp)
42	40, 41	sylan 448	. . . . . . . . 9 |- ((T e. HrmOp /\ (normop` T) e. RR) -> T e. BndLinOp)
43	38, 42	sylan 448	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (normh` (T` x)) <_ ((normop` T) x. (normh` x)))
44	37, 43	jca 288	. . . . . . 7 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (0 <_ (normh` x) /\ (normh` (T` x)) <_ ((normop` T) x. (normh` x))))
45	31, 35, 44	sylanc 471	. . . . . 6 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> ((normh` (T` x)) x. (normh` x)) <_ (((normop` T) x. (normh` x)) x. (normh` x)))
46	23	recnd 5287	. . . . . . . . . . . 12 |- (x e. H~ -> (normh` x) e. CC)
47		sqvalt 6540	. . . . . . . . . . . 12 |- ((normh` x) e. CC -> ((normh` x)^2) = ((normh` x) x. (normh` x)))
48	46, 47	syl 10	. . . . . . . . . . 11 |- (x e. H~ -> ((normh` x)^2) = ((normh` x) x. (normh` x)))
49		normsqt 8922	. . . . . . . . . . 11 |- (x e. H~ -> ((normh` x)^2) = (x .ih x))
50	48, 49	eqtr3d 1501	. . . . . . . . . 10 |- (x e. H~ -> ((normh` x) x. (normh` x)) = (x .ih x))
51	50	opreq2d 3961	. . . . . . . . 9 |- (x e. H~ -> ((normop` T) x. ((normh` x) x. (normh` x))) = ((normop` T) x. (x .ih x)))
52	51	adantl 388	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> ((normop` T) x. ((normh` x) x. (normh` x))) = ((normop` T) x. (x .ih x)))
53		axmulass 5250	. . . . . . . . 9 |- (((normop` T) e. CC /\ (normh` x) e. CC /\ (normh` x) e. CC) -> (((normop` T) x. (normh` x)) x. (normh` x)) = ((normop` T) x. ((normh` x) x. (normh` x))))
54		recnt 5285	. . . . . . . . . 10 |- ((normop` T) e. RR -> (normop` T) e. CC)
55	54	ad2antlr 405	. . . . . . . . 9 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (normop` T) e. CC)
56	24	recnd 5287	. . . . . . . . 9 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (normh` x) e. CC)
57	53, 55, 56, 56	syl3anc 856	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (((normop` T) x. (normh` x)) x. (normh` x)) = ((normop` T) x. ((normh` x) x. (normh` x))))
58		ax-his3 8872	. . . . . . . . 9 |- (((normop` T) e. CC /\ x e. H~ /\ x e. H~) -> (((normop` T) .h x) .ih x) = ((normop` T) x. (x .ih x)))
59		pm3.27 323	. . . . . . . . 9 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> x e. H~)
60	58, 55, 59, 59	syl3anc 856	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (((normop` T) .h x