Metamath Proof Explorer


Theorem nmophmi

Description: The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmophm.1 T BndLinOp
Assertion nmophmi A norm op A · op T = A norm op T

Proof

Step Hyp Ref Expression
1 nmophm.1 T BndLinOp
2 bdopf T BndLinOp T :
3 1 2 ax-mp T :
4 homval A T : x A · op T x = A T x
5 3 4 mp3an2 A x A · op T x = A T x
6 5 fveq2d A x norm A · op T x = norm A T x
7 3 ffvelrni x T x
8 norm-iii A T x norm A T x = A norm T x
9 7 8 sylan2 A x norm A T x = A norm T x
10 6 9 eqtrd A x norm A · op T x = A norm T x
11 10 adantr A x norm x 1 norm A · op T x = A norm T x
12 normcl T x norm T x
13 7 12 syl x norm T x
14 13 ad2antlr A x norm x 1 norm T x
15 abscl A A
16 absge0 A 0 A
17 15 16 jca A A 0 A
18 17 ad2antrr A x norm x 1 A 0 A
19 nmoplb T : x norm x 1 norm T x norm op T
20 3 19 mp3an1 x norm x 1 norm T x norm op T
21 20 adantll A x norm x 1 norm T x norm op T
22 nmopre T BndLinOp norm op T
23 1 22 ax-mp norm op T
24 lemul2a norm T x norm op T A 0 A norm T x norm op T A norm T x A norm op T
25 23 24 mp3anl2 norm T x A 0 A norm T x norm op T A norm T x A norm op T
26 14 18 21 25 syl21anc A x norm x 1 A norm T x A norm op T
27 11 26 eqbrtrd A x norm x 1 norm A · op T x A norm op T
28 27 ex A x norm x 1 norm A · op T x A norm op T
29 28 ralrimiva A x norm x 1 norm A · op T x A norm op T
30 homulcl A T : A · op T :
31 3 30 mpan2 A A · op T :
32 remulcl A norm op T A norm op T
33 15 23 32 sylancl A A norm op T
34 33 rexrd A A norm op T *
35 nmopub A · op T : A norm op T * norm op A · op T A norm op T x norm x 1 norm A · op T x A norm op T
36 31 34 35 syl2anc A norm op A · op T A norm op T x norm x 1 norm A · op T x A norm op T
37 29 36 mpbird A norm op A · op T A norm op T
38 fveq2 A = 0 A = 0
39 abs0 0 = 0
40 38 39 syl6eq A = 0 A = 0
41 40 oveq1d A = 0 A norm op T = 0 norm op T
42 23 recni norm op T
43 42 mul02i 0 norm op T = 0
44 41 43 syl6eq A = 0 A norm op T = 0
45 44 adantl A A = 0 A norm op T = 0
46 nmopge0 A · op T : 0 norm op A · op T
47 31 46 syl A 0 norm op A · op T
48 47 adantr A A = 0 0 norm op A · op T
49 45 48 eqbrtrd A A = 0 A norm op T norm op A · op T
50 nmoplb A · op T : x norm x 1 norm A · op T x norm op A · op T
51 31 50 syl3an1 A x norm x 1 norm A · op T x norm op A · op T
52 51 3expa A x norm x 1 norm A · op T x norm op A · op T
53 11 52 eqbrtrrd A x norm x 1 A norm T x norm op A · op T
54 53 adantllr A A 0 x norm x 1 A norm T x norm op A · op T
55 13 adantl A A 0 x norm T x
56 nmopxr A · op T : norm op A · op T *
57 31 56 syl A norm op A · op T *
58 nmopgtmnf A · op T : −∞ < norm op A · op T
59 31 58 syl A −∞ < norm op A · op T
60 xrre norm op A · op T * A norm op T −∞ < norm op A · op T norm op A · op T A norm op T norm op A · op T
61 57 33 59 37 60 syl22anc A norm op A · op T
62 61 ad2antrr A A 0 x norm op A · op T
63 15 ad2antrr A A 0 x A
64 absgt0 A A 0 0 < A
65 64 biimpa A A 0 0 < A
66 65 adantr A A 0 x 0 < A
67 lemuldiv2 norm T x norm op A · op T A 0 < A A norm T x norm op A · op T norm T x norm op A · op T A
68 55 62 63 66 67 syl112anc A A 0 x A norm T x norm op A · op T norm T x norm op A · op T A
69 68 adantr A A 0 x norm x 1 A norm T x norm op A · op T norm T x norm op A · op T A
70 54 69 mpbid A A 0 x norm x 1 norm T x norm op A · op T A
71 70 ex A A 0 x norm x 1 norm T x norm op A · op T A
72 71 ralrimiva A A 0 x norm x 1 norm T x norm op A · op T A
73 61 adantr A A 0 norm op A · op T
74 15 adantr A A 0 A
75 abs00 A A = 0 A = 0
76 75 necon3bid A A 0 A 0
77 76 biimpar A A 0 A 0
78 73 74 77 redivcld A A 0 norm op A · op T A
79 78 rexrd A A 0 norm op A · op T A *
80 nmopub T : norm op A · op T A * norm op T norm op A · op T A x norm x 1 norm T x norm op A · op T A
81 3 79 80 sylancr A A 0 norm op T norm op A · op T A x norm x 1 norm T x norm op A · op T A
82 72 81 mpbird A A 0 norm op T norm op A · op T A
83 23 a1i A A 0 norm op T
84 lemuldiv2 norm op T norm op A · op T A 0 < A A norm op T norm op A · op T norm op T norm op A · op T A
85 83 73 74 65 84 syl112anc A A 0 A norm op T norm op A · op T norm op T norm op A · op T A
86 82 85 mpbird A A 0 A norm op T norm op A · op T
87 49 86 pm2.61dane A A norm op T norm op A · op T
88 61 33 letri3d A norm op A · op T = A norm op T norm op A · op T A norm op T A norm op T norm op A · op T
89 37 87 88 mpbir2and A norm op A · op T = A norm op T