Theorem leopnmidt 10071

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 9847	. . . . 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 5315	. . . . . 6 |- ((T e. HrmOp /\ x e. H~) -> ((T` x) .ih x) e. CC)
4		absclt 6833	. . . . . 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 9847	. . . . . 6 |- ((((normop` T) .op Iop ) e. HrmOp /\ x e. H~) -> ((((normop` T) .op Iop )` x) .ih x) e. RR)
8		idhmop 9906	. . . . . . 7 |- Iop e. HrmOp
9		hmopmt 9946	. . . . . . 7 |- (((normop` T) e. RR /\ Iop e. HrmOp) -> ((normop` T) .op Iop ) e. HrmOp)
10	8, 9	mpan2 696	. . . . . 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 6864	. . . . . 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 5274	. . . . . 6 |- (((normh` (T` x)) e. RR /\ (normh` x) e. RR) -> ((normh` (T` x)) x. (normh` x)) e. RR)
17		ffvelrn 3814	. . . . . . . . 9 |- ((T:H~-->H~ /\ x e. H~) -> (T` x) e. H~)
18		normclt 8991	. . . . . . . . 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 9801	. . . . . . . 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 8991	. . . . . . 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	17, 20	sylan 448	. . . . . . 7 |- ((T e. HrmOp /\ x e. H~) -> (T` x) e. H~)
27		bcst 9048	. . . . . . 7 |- (((T` x) e. H~ /\ x e. H~) -> (abs` ((T` x) .ih x)) <_ ((normh` (T` x)) x. (normh` x)))
28	26, 27	sylancom 475	. . . . . 6 |- ((T e. HrmOp /\ x e. H~) -> (abs` ((T` x) .ih x)) <_ ((normh` (T` x)) x. (normh` x)))
29	28	adantlr 393	. . . . 5 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (abs` ((T` x) .ih x)) <_ ((normh` (T` x)) x. (normh` x)))
30		lemul1itOLD 5838	. . . . . . 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)))
31		axmulrcl 5274	. . . . . . . . 9 |- (((normop` T) e. RR /\ (normh` x) e. RR) -> ((normop` T) x. (normh` x)) e. RR)
32		pm3.27 323	. . . . . . . . 9 |- ((T e. HrmOp /\ (normop` T) e. RR) -> (normop` T) e. RR)
33	31, 32, 23	syl2an 454	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> ((normop` T) x. (normh` x)) e. RR)
34	22, 33, 24	3jca 819	. . . . . . 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))
35		normge0t 8992	. . . . . . . . 9 |- (x e. H~ -> 0 <_ (normh` x))
36	35	adantl 388	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> 0 <_ (normh` x))
37		nmbdoplbt 9950	. . . . . . . . 9 |- ((T e. BndLinOp /\ x e. H~) -> (normh` (T` x)) <_ ((normop` T) x. (normh` x)))
38		elbdop2t 9798	. . . . . . . . . . 11 |- (T e. BndLinOp <-> (T e. LinOp /\ (normop` T) e. RR))
39	38	biimpr 152	. . . . . . . . . 10 |- ((T e. LinOp /\ (normop` T) e. RR) -> T e. BndLinOp)
40		hmoplint 9866	. . . . . . . . . 10 |- (T e. HrmOp -> T e. LinOp)
41	39, 40	sylan 448	. . . . . . . . 9 |- ((T e. HrmOp /\ (normop` T) e. RR) -> T e. BndLinOp)
42	37, 41	sylan 448	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (normh` (T` x)) <_ ((normop` T) x. (normh` x)))
43	36, 42	jca 288	. . . . . . 7 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (0 <_ (normh` x) /\ (normh` (T` x)) <_ ((normop` T) x. (normh` x))))
44	30, 34, 43	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)))
45	23	recnd 5315	. . . . . . . . . . . 12 |- (x e. H~ -> (normh` x) e. CC)
46		sqvalt 6609	. . . . . . . . . . . 12 |- ((normh` x) e. CC -> ((normh` x)^2) = ((normh` x) x. (normh` x)))
47	45, 46	syl 10	. . . . . . . . . . 11 |- (x e. H~ -> ((normh` x)^2) = ((normh` x) x. (normh` x)))
48		normsqt 9001	. . . . . . . . . . 11 |- (x e. H~ -> ((normh` x)^2) = (x .ih x))
49	47, 48	eqtr3d 1509	. . . . . . . . . 10 |- (x e. H~ -> ((normh` x) x. (normh` x)) = (x .ih x))
50	49	opreq2d 3976	. . . . . . . . 9 |- (x e. H~ -> ((normop` T) x. ((normh` x) x. (normh` x))) = ((normop` T) x. (x .ih x)))
51	50	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)))
52		axmulass 5278	. . . . . . . . 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))))
53		recnt 5313	. . . . . . . . . 10 |- ((normop` T) e. RR -> (normop` T) e. CC)
54	53	ad2antlr 405	. . . . . . . . 9 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (normop` T) e. CC)
55	24	recnd 5315	. . . . . . . . 9 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (normh` x) e. CC)
56	52, 54, 55, 55	syl3anc 858	. . . . . . . 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))))
57		ax-his3 8951	. . . . . . . . 9 |- (((normop` T) e. CC /\ x e. H~ /\ x e. H~) -> (((normop` T) .h x) .ih x) = ((normop` T) x. (x .ih x)))
58		pm3.27 323	. . . . . . . . 9 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> x e. H~)
59	57, 54, 58, 58	syl3anc 858	. . . . . . . 8 |- (((T e. HrmOp /\ (normop` T) e. RR) /\ x e. H~) -> (((normop` T) .h x) .ih x) = ((normop` T) x. (x .ih x)))
60	51, 56, 59