Theorem nmopco 10023

Description: Upper bound for the norm of the composition of two bounded linear operators.

Hypotheses

Ref	Expression
nmoptri.1	|- S e. BndLinOp
nmoptri.2	|- T e. BndLinOp

Assertion

Ref	Expression
nmopco	|- (normop` (S o. T)) <_ ((normop` S) x. (normop` T))

Proof of Theorem nmopco

Step	Hyp	Ref	Expression
1		nmoptri.1	. . . . 5 |- S e. BndLinOp
2		bdoplnt 9783	. . . . 5 |- (S e. BndLinOp -> S e. LinOp)
3	1, 2	ax-mp 7	. . . 4 |- S e. LinOp
4		nmoptri.2	. . . . 5 |- T e. BndLinOp
5		bdoplnt 9783	. . . . 5 |- (T e. BndLinOp -> T e. LinOp)
6	4, 5	ax-mp 7	. . . 4 |- T e. LinOp
7	3, 6	lnopco 9923	. . 3 |- (S o. T) e. LinOp
8	7	lnopf 9888	. 2 |- (S o. T):H~-->H~
9		nmopret 9792	. . . . 5 |- (S e. BndLinOp -> (normop` S) e. RR)
10	1, 9	ax-mp 7	. . . 4 |- (normop` S) e. RR
11		nmopret 9792	. . . . 5 |- (T e. BndLinOp -> (normop` T) e. RR)
12	4, 11	ax-mp 7	. . . 4 |- (normop` T) e. RR
13	10, 12	remulcl 5347	. . 3 |- ((normop` S) x. (normop` T)) e. RR
14		rexrt 5511	. . 3 |- (((normop` S) x. (normop` T)) e. RR -> ((normop` S) x. (normop` T)) e. RR*)
15	13, 14	ax-mp 7	. 2 |- ((normop` S) x. (normop` T)) e. RR*
16		0re 5452	. . . . . . . . 9 |- 0 e. RR
17	16	leid 5622	. . . . . . . 8 |- 0 <_ 0
18	17	a1i 8	. . . . . . 7 |- (((normop` T) = 0 /\ x e. H~) -> 0 <_ 0)
19		fveq1 3729	. . . . . . . . . 10 |- ((S o. T) = 0hop -> ((S o. T)` x) = (0hop` x))
20	19	fveq2d 3734	. . . . . . . . 9 |- ((S o. T) = 0hop -> (normh` ((S o. T)` x)) = (normh` (0hop` x)))
21		ho0valt 9671	. . . . . . . . . . 11 |- (x e. H~ -> (0hop` x) = 0h)
22	21	fveq2d 3734	. . . . . . . . . 10 |- (x e. H~ -> (normh` (0hop` x)) = (normh` 0h))
23		norm0 8990	. . . . . . . . . 10 |- (normh` 0h) = 0
24	22, 23	syl6eq 1526	. . . . . . . . 9 |- (x e. H~ -> (normh` (0hop` x)) = 0)
25	20, 24	sylan9eq 1530	. . . . . . . 8 |- (((S o. T) = 0hop /\ x e. H~) -> (normh` ((S o. T)` x)) = 0)
26	3, 6	lnopco0 9924	. . . . . . . . 9 |- ((normop` T) = 0 -> (normop` (S o. T)) = 0)
27	7	nmlnop0HIL 9916	. . . . . . . . 9 |- ((normop` (S o. T)) = 0 <-> (S o. T) = 0hop)
28	26, 27	sylib 198	. . . . . . . 8 |- ((normop` T) = 0 -> (S o. T) = 0hop)
29	25, 28	sylan 450	. . . . . . 7 |- (((normop` T) = 0 /\ x e. H~) -> (normh` ((S o. T)` x)) = 0)
30		opreq2 3975	. . . . . . . . 9 |- ((normop` T) = 0 -> ((normop` S) x. (normop` T)) = ((normop` S) x. 0))
31	10	recn 5326	. . . . . . . . . 10 |- (normop` S) e. CC
32	31	mul01 5443	. . . . . . . . 9 |- ((normop` S) x. 0) = 0
33	30, 32	syl6eq 1526	. . . . . . . 8 |- ((normop` T) = 0 -> ((normop` S) x. (normop` T)) = 0)
34	33	adantr 391	. . . . . . 7 |- (((normop` T) = 0 /\ x e. H~) -> ((normop` S) x. (normop` T)) = 0)
35	18, 29, 34	3brtr4d 2650	. . . . . 6 |- (((normop` T) = 0 /\ x e. H~) -> (normh` ((S o. T)` x)) <_ ((normop` S) x. (normop` T)))
36	35	adantrr 397	. . . . 5 |- (((normop` T) = 0 /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` ((S o. T)` x)) <_ ((normop` S) x. (normop` T)))
37		norm-iiit 9002	. . . . . . . . . . 11 |- (((1 / (normop` T)) e. CC /\ ((S o. T)` x) e. H~) -> (normh` ((1 / (normop` T)) .h ((S o. T)` x))) = ((abs` (1 / (normop` T))) x. (normh` ((S o. T)` x))))
38	12	recn 5326	. . . . . . . . . . . 12 |- (normop` T) e. CC
39	38	recclz 5726	. . . . . . . . . . 11 |- ((normop` T) =/= 0 -> (1 / (normop` T)) e. CC)
40	8	ffvelrni 3821	. . . . . . . . . . 11 |- (x e. H~ -> ((S o. T)` x) e. H~)
41	37, 39, 40	syl2an 456	. . . . . . . . . 10 |- (((normop` T) =/= 0 /\ x e. H~) -> (normh` ((1 / (normop` T)) .h ((S o. T)` x))) = ((abs` (1 / (normop` T))) x. (normh` ((S o. T)` x))))
42	3	lnopmul 9891	. . . . . . . . . . . . 13 |- (((1 / (normop` T)) e. CC /\ (T` x) e. H~) -> (S` ((1 / (normop` T)) .h (T` x))) = ((1 / (normop` T)) .h (S` (T` x))))
43		bdopft 9784	. . . . . . . . . . . . . . 15 |- (T e. BndLinOp -> T:H~-->H~)
44	4, 43	ax-mp 7	. . . . . . . . . . . . . 14 |- T:H~-->H~
45	44	ffvelrni 3821	. . . . . . . . . . . . 13 |- (x e. H~ -> (T` x) e. H~)
46	42, 39, 45	syl2an 456	. . . . . . . . . . . 12 |- (((normop` T) =/= 0 /\ x e. H~) -> (S` ((1 / (normop` T)) .h (T` x))) = ((1 / (normop` T)) .h (S` (T` x))))
47		bdopft 9784	. . . . . . . . . . . . . . . 16 |- (S e. BndLinOp -> S:H~-->H~)
48	1, 47	ax-mp 7	. . . . . . . . . . . . . . 15 |- S:H~-->H~
49	48, 44	hoco 9685	. . . . . . . . . . . . . 14 |- (x e. H~ -> ((S o. T)` x) = (S` (T` x)))
50	49	opreq2d 3982	. . . . . . . . . . . . 13 |- (x e. H~ -> ((1 / (normop` T)) .h ((S o. T)` x)) = ((1 / (normop` T)) .h (S` (T` x))))
51	50	adantl 390	. . . . . . . . . . . 12 |- (((normop` T) =/= 0 /\ x e. H~) -> ((1 / (normop` T)) .h ((S o. T)` x)) = ((1 / (normop` T)) .h (S` (T` x))))
52	46, 51	eqtr4d 1513	. . . . . . . . . . 11 |- (((normop` T) =/= 0 /\ x e. H~) -> (S` ((1 / (normop` T)) .h (T` x))) = ((1 / (normop` T)) .h ((S o. T)` x)))
53	52	fveq2d 3734	. . . . . . . . . 10 |- (((normop` T) =/= 0 /\ x e. H~) -> (normh` (S` ((1 / (normop` T)) .h (T` x)))) = (normh` ((1 / (normop` T)) .h ((S o. T)` x))))
54		divrec2t 5747	. . . . . . . . . . . . . 14 |- (((normh` ((S o. T)` x)) e. CC /\ (normop` T) e. CC /\ (normop` T) =/= 0) -> ((normh` ((S o. T)` x)) / (normop` T)) = ((1 / (normop` T)) x. (normh` ((S o. T)` x))))
55	38, 54	mp3an2 906	. . . . . . . . . . . . 13 |- (((normh` ((S o. T)` x)) e. CC /\ (normop` T) =/= 0) -> ((normh` ((S o. T)` x)) / (normop` T)) = ((1 / (normop` T)) x. (normh` ((S o. T)` x))))
56		normclt 8986	. . . . . . . . . . . . . . 15 |- (((S o. T)` x) e. H~ -> (normh` ((S o. T)` x)) e. RR)
57	40, 56	syl 10	. . . . . . . . . . . . . 14 |- (x e. H~ -> (normh` ((S o. T)` x)) e. RR)
58	57	recnd 5327	. . . . . . . . . . . . 13 |- (x e. H~ -> (normh` ((S o. T)` x)) e. CC)
59	55, 58	sylan 450	. . . . . . . . . . . 12 |- ((x e. H~ /\ (normop` T) =/= 0) -> ((normh` ((S o. T)` x)) / (normop` T)) = ((1 / (normop` T)) x. (normh` ((S o. T)` x))))
60	59	ancoms 438	. . . . . . . . . . 11 |- (((normop` T) =/= 0 /\ x e. H~) -> ((normh` ((S o. T)` x)) / (normop` T)) = ((1 / (normop` T)) x. (normh` ((S o. T)` x))))
61		absidt 6862	. . . . . . . . . . . . . 14 |- (((1 / (normop` T)) e. RR /\ 0 <_ (1 / (normop` T))) -> (abs` (1 / (normop` T))) = (1 / (normop` T)))
62	12	rerecclz 5804	. . . . . . . . . . . . . 14 |- ((normop` T) =/= 0 -> (1 / (normop` T)) e. RR)
63		ltlet 5532	. . . . . . . . . . . . . . . 16 |- ((0 e. RR /\ (1 / (normop` T)) e. RR) -> (0 < (1 / (normop` T)) -> 0 <_ (1 / (normop` T))))
64	16, 63	mpan 697	. . . . . . . . . . . . . . 15 |- ((1 / (normop` T)) e. RR -> (0 < (1 / (normop` T)) -> 0 <_ (1 / (normop` T))))
65		nmopgt0t 9831	. . . . . . . . . . . . . . . . 17 |- (T:H~-->H~ -> ((normop` T) =/= 0 <-> 0 < (normop` T)))
66	44, 65	ax-mp 7	. . . . . . . . . . . . . . . 16 |- ((normop` T) =/= 0 <-> 0 < (normop` T))
67	12	recgt0 5864	. . . . . . . . . . . . . . . 16 |- (0 < (normop` T) -> 0 < (1 / (normop` T)))
68	66, 67	sylbi 199	. . . . . . . . . . . . . . 15 |- ((normop` T) =/= 0 -> 0 < (1 / (normop` T)))
69	64, 62, 68	sylc 68	. . . . . . . . . . . . . 14 |- ((normop` T) =/= 0 -> 0 <_ (1 / (normop` T)))
70	61, 62, 69	sylanc 473	. . . . . . . . . . . . 13 |- ((normop` T) =/= 0 -> (abs` (1 / (normop` T))) = (1 / (normop` T)))
71	70	adantr 391	. . . . . . . . . . . 12 |- (((normop` T) =/= 0 /\ x e. H~) -> (abs` (1 / (normop` T))) = (1 / (normop` T)))
72	71	opreq1d 3981	. . . . . . . . . . 11 |- (((normop` T) =/= 0 /\ x e. H~)