HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem nmophm 9876
Description: The norm of the scalar product of a bounded linear operator.
Hypothesis
Ref Expression
nmophm.1 |- T e. BndLinOp
Assertion
Ref Expression
nmophm |- (A e. CC -> (normop` (A .op T)) = ((abs` A) x. (normop` T)))
Proof of Theorem nmophm
StepHypRef Expression
1 nmopubt 9749 . . . 4 |- (((A .op T):H~-->H~ /\ ((abs` A) x. (normop` T)) e. RR* /\ A.x e. H~ ((normh` x) <_ 1 -> (normh` ((A .op T)` x)) <_ ((abs` A) x. (normop` T)))) -> (normop` (A .op T)) <_ ((abs` A) x. (normop` T)))
2 nmophm.1 . . . . . 6 |- T e. BndLinOp
3 bdopft 9706 . . . . . 6 |- (T e. BndLinOp -> T:H~-->H~)
42, 3ax-mp 7 . . . . 5 |- T:H~-->H~
5 homulclt 9602 . . . . 5 |- ((A e. CC /\ T:H~-->H~) -> (A .op T):H~-->H~)
64, 5mpan2 694 . . . 4 |- (A e. CC -> (A .op T):H~-->H~)
7 absclt 6768 . . . . . 6 |- (A e. CC -> (abs` A) e. RR)
8 nmopret 9714 . . . . . . . 8 |- (T e. BndLinOp -> (normop` T) e. RR)
92, 8ax-mp 7 . . . . . . 7 |- (normop` T) e. RR
10 axmulrcl 5246 . . . . . . 7 |- (((abs` A) e. RR /\ (normop` T) e. RR) -> ((abs` A) x. (normop` T)) e. RR)
119, 10mpan2 694 . . . . . 6 |- ((abs` A) e. RR -> ((abs` A) x. (normop` T)) e. RR)
127, 11syl 10 . . . . 5 |- (A e. CC -> ((abs` A) x. (normop` T)) e. RR)
13 rexrt 5471 . . . . 5 |- (((abs` A) x. (normop` T)) e. RR -> ((abs` A) x. (normop` T)) e. RR*)
1412, 13syl 10 . . . 4 |- (A e. CC -> ((abs` A) x. (normop` T)) e. RR*)
15 homvalt 9435 . . . . . . . . . . 11 |- ((A e. CC /\ T:H~-->H~ /\ x e. H~) -> ((A .op T)` x) = (A .h (T` x)))
164, 15mp3an2 901 . . . . . . . . . 10 |- ((A e. CC /\ x e. H~) -> ((A .op T)` x) = (A .h (T` x)))
1716fveq2d 3713 . . . . . . . . 9 |- ((A e. CC /\ x e. H~) -> (normh` ((A .op T)` x)) = (normh` (A .h (T` x))))
18 norm-iiit 8928 . . . . . . . . . 10 |- ((A e. CC /\ (T` x) e. H~) -> (normh` (A .h (T` x))) = ((abs` A) x. (normh` (T` x))))
194ffvelrni 3800 . . . . . . . . . 10 |- (x e. H~ -> (T` x) e. H~)
2018, 19sylan2 451 . . . . . . . . 9 |- ((A e. CC /\ x e. H~) -> (normh` (A .h (T` x))) = ((abs` A) x. (normh` (T` x))))
2117, 20eqtrd 1499 . . . . . . . 8 |- ((A e. CC /\ x e. H~) -> (normh` ((A .op T)` x)) = ((abs` A) x. (normh` (T` x))))
2221adantr 389 . . . . . . 7 |- (((A e. CC /\ x e. H~) /\ (normh` x) <_ 1) -> (normh` ((A .op T)` x)) = ((abs` A) x. (normh` (T` x))))
23 lemul2itOLD 5796 . . . . . . . 8 |- ((((normh` (T` x)) e. RR /\ (normop` T) e. RR /\ (abs` A) e. RR) /\ (0 <_ (abs` A) /\ (normh` (T` x)) <_ (normop` T))) -> ((abs` A) x. (normh` (T` x))) <_ ((abs` A) x. (normop` T)))
24 normclt 8912 . . . . . . . . . . . 12 |- ((T` x) e. H~ -> (normh` (T` x)) e. RR)
2519, 24syl 10 . . . . . . . . . . 11 |- (x e. H~ -> (normh` (T` x)) e. RR)
2625adantl 388 . . . . . . . . . 10 |- ((A e. CC /\ x e. H~) -> (normh` (T` x)) e. RR)
279a1i 8 . . . . . . . . . 10 |- ((A e. CC /\ x e. H~) -> (normop` T) e. RR)
287adantr 389 . . . . . . . . . 10 |- ((A e. CC /\ x e. H~) -> (abs` A) e. RR)
2926, 27, 283jca 817 . . . . . . . . 9 |- ((A e. CC /\ x e. H~) -> ((normh` (T` x)) e. RR /\ (normop` T) e. RR /\ (abs` A) e. RR))
3029adantr 389 . . . . . . . 8 |- (((A e. CC /\ x e. H~) /\ (normh` x) <_ 1) -> ((normh` (T` x)) e. RR /\ (normop` T) e. RR /\ (abs` A) e. RR))
31 absge0t 6789 . . . . . . . . . 10 |- (A e. CC -> 0 <_ (abs` A))
32 nmoplbt 9748 . . . . . . . . . . 11 |- ((T:H~-->H~ /\ x e. H~ /\ (normh` x) <_ 1) -> (normh` (T` x)) <_ (normop` T))
334, 32mp3an1 900 . . . . . . . . . 10 |- ((x e. H~ /\ (normh` x) <_ 1) -> (normh` (T` x)) <_ (normop` T))
3431, 33anim12i 333 . . . . . . . . 9 |- ((A e. CC /\ (x e. H~ /\ (normh` x) <_ 1)) -> (0 <_ (abs` A) /\ (normh` (T` x)) <_ (normop` T)))
3534anassrs 441 . . . . . . . 8 |- (((A e. CC /\ x e. H~) /\ (normh` x) <_ 1) -> (0 <_ (abs` A) /\ (normh` (T` x)) <_ (normop` T)))
3623, 30, 35sylanc 471 . . . . . . 7 |- (((A e. CC /\ x e. H~) /\ (normh` x) <_ 1) -> ((abs` A) x. (normh` (T` x))) <_ ((abs` A) x. (normop` T)))
3722, 36eqbrtrd 2625 . . . . . 6 |- (((A e. CC /\ x e. H~) /\ (normh` x) <_ 1) -> (normh` ((A .op T)` x)) <_ ((abs` A) x. (normop` T)))
3837ex 373 . . . . 5 |- ((A e. CC /\ x e. H~) -> ((normh` x) <_ 1 -> (normh` ((A .op T)` x)) <_ ((abs` A) x. (normop` T))))
3938r19.21aiva 1706 . . . 4 |- (A e. CC -> A.x e. H~ ((normh` x) <_ 1 -> (normh` ((A .op T)` x)) <_ ((abs` A) x. (normop` T))))
401, 6, 14, 39syl3anc 856 . . 3 |- (A e. CC -> (normop` (A .op T)) <_ ((abs` A) x. (normop` T)))
41 fveq2 3709 . . . . . . . . 9 |- (A = 0 -> (abs` A) = (abs` 0))
42 abs0 6814 . . . . . . . . 9 |- (abs` 0) = 0
4341, 42syl6eq 1515 . . . . . . . 8 |- (A = 0 -> (abs` A) = 0)
4443opreq1d 3960 . . . . . . 7 |- (A = 0 -> ((abs` A) x. (normop` T)) = (0 x. (normop` T)))
459recn 5286 . . . . . . . 8 |- (normop` T) e. CC
4645mul02 5404 . . . . . . 7 |- (0 x. (normop` T)) = 0
4744, 46syl6eq 1515 . . . . . 6 |- (A = 0 -> ((abs` A) x. (normop` T)) = 0)
4847adantl 388 . . . . 5 |- ((A e. CC /\ A = 0) -> ((abs` A) x. (normop` T)) = 0)
49 nmopge0t 9751 . . . . . . 7 |- ((A .op T):H~-->H~ -> 0 <_ (normop` (A .op T)))
506, 49syl 10 . . . . . 6 |- (A e. CC -> 0 <_ (normop` (A .op T)))
5150adantr 389 . . . . 5 |- ((A e. CC /\ A = 0) -> 0 <_ (normop` (A .op T)))
5248, 51eqbrtrd 2625 . . . 4 |- ((A e. CC /\ A = 0) -> ((abs` A) x. (normop` T)) <_ (normop` (A .op T)))
53 nmopubt 9749 . . . . . . . 8 |- ((T:H~-->H~ /\ ((normop` (A .op T)) / (abs` A)) e. RR* /\ A.x e. H~ ((normh` x) <_ 1 -> (normh` (T` x)) <_ ((normop` (A .op T)) / (abs` A)))) -> (normop` T) <_ ((normop` (A .op T)) / (abs` A)))
544, 53mp3an1 900 . . . . . . 7 |- ((((normop` (A .op T)) / (abs` A)) e. RR* /\ A.x e. H~ ((normh` x) <_ 1 -> (normh` (T` x)) <_ ((normop` (A .op T)) / (abs` A)))) -> (normop` T) <_ ((normop` (A .op T)) / (abs` A)))
55 redivclt 5756 . . . . . . . . 9 |- (((normop` (A .op T)) e. RR /\ (abs` A) e. RR /\ (abs` A) =/= 0) -> ((normop` (A .op T)) / (abs` A)) e. RR)
56 xrret 5542 . . . . . . . . . . 11 |- ((((normop` (A .op T)) e. RR* /\ ((abs` A) x. (normop` T)) e. RR) /\ ( -oo < (normop` (A .op T)) /\ (normop` (A .op T)) <_ ((abs` A) x. (normop` T)))) -> (normop` (A .op T)) e. RR)
57 nmopxrt 9710 . . . . . . . . . . . 12 |- ((A .op T):H~-->H~ -> (normop` (A .op T)) e. RR*)
586, 57syl 10 . . . . . . . . . . 11 |- (A e. CC -> (normop` (A .op T)) e. RR*)
59 nmopgtmnf 9712 . . . . . . . . . . . 12 |- ((A .op T):H~-->H~ -> -oo < (normop` (A .op T)))
606, 59syl 10 . . . . . . . . . . 11 |- (A e. CC -> -oo < (normop` (A .op T)))
6156, 58, 12, 60, 40syl2anc 472 . . . . . . . . . 10 |- (A e. CC -> (normop`